Loading…
Certifying Rule-Based Models using Graph Transformation
Lambers, Leen
Viele Systeme zeigen regelhaftes Verhalten auf was sehr gut durch Graphtransformation modelliert werden kann. Diese Dissertation führt eine neue Graphtransformationstheorie für eine ausdruckskräftigere Variante von Graphtransformation als die bisherige ein. Sie erlaubt nicht nur positive Vor- und Nachbedingungen in Regeln, sondern auch negative Anwendungsbedingungen. Die bisherigen Analysetechniken werden erweitert für diese ausdruckskräftigere Variante. Diese Techniken ermöglichen unter anderem das statische Aufspüren von potentiellen Konflikten oder kausalen Abhängigkeiten zwischen Transformationen, und das Feststellen von lokaler Konfluenz im Falle eines Konflikts. Zu diesem Zweck wurde die Theorie der kritischen Paare erweitert. Es werden auch neuartige Analysetechniken eingeführt und die bisherigen werden teilweise effizienter gemacht. Eine der neuen Techniken ermöglicht zum Beispiel eine statische Prüfung der Anwendbarkeit bzw. Nicht-Anwendbarkeit von Regelsequenzen. Der Hauptteil der entwickelten Theorie in dieser Dissertation ist nicht nur auf Graphtransformationen anwendbar. Sie wird ausserdem formuliert im abstrakteren Rahmenwerk der adhesiven High-Level-Transformation. Somit können die Analysetechniken nicht nur auf Graphen, sondern auch auf andere komplexe Strukturen sowie z.B. Petrinetze und attributierte Graphen angewandt werden. Schliesslich wird eine allgemeine Vorgehensweise vorgeschlagen, die zur Zertifizierung einer Auswahl von Eigenschaften der regelbasierten Modelle führt. Die Zertifizierung, basierend auf Analysetechniken für Graphtransformation, wird illustriert am Fallbeispiel einer Fahrstulkontrolle. Ausserdem wird die aktuelle Werkzeugunterstützung in AGG, hinsichtlich der Zertifizierung von regelbasierten Modellen mittels Graphtransformation, vorgestellt.
Many systems exhibit rule-based behavior that can be modeled very well by means of graph transformation. In this thesis, a new graph transformation theory is introduced for a more expressive kind of graph transformation than the usual one. This kind of graph transformation not only allows positive pre- and post-conditions to be expressed in rules, but also allows so-called negative application conditions. Present analysis techniques are extended for this more expressive kind of graph transformation. These techniques allow, amongst other things, the static detection of potential conflicts and causal dependencies between transformations, and the detection of local confluence in cases of conflicts. For this purpose, the theory of critical pairs is extended. Moreover, new kinds of analysis techniques are introduced and present techniques are improved. One new technique enables, for example, the static analysis of applicability (resp. non-applicability) of rule sequences. The main part of the newly developed theory in this thesis does not only apply to graph transformation. In addition, it is formulated in the more abstract adhesive high-level-transformation framework. Consequently, the analysis techniques can be applied not only to graphs, but also to other complex structures such as, for example, Petri nets and attributed graphs. Finally, a general road map is presented leading to the certification of a selection of properties in rule-based models. The certification, based on graph transformation analysis techniques, is illustrated by a case study of an elevator control system. Moreover, the current tool support for certification of rule-based models using graph transformation provided by AGG is outlined.
