Loading…
Behavior and confluence analysis of M-adhesive transformation systems using M-functors
Maximova, Maria
For modeling dynamic systems, various graphical modeling formalisms exist. In particular, rule-based graph transformation formalisms have proven to be adequate, both to capture system behavior and system adaptations. For some graph transformation-based formalisms there already exist well-established tools, enabling modelers to analyze important semantical properties of considered transformation systems. Yet, there are many further adaptations and variants of such formalisms which, on the one hand, ease their application in certain contexts but, on the other hand, require new analysis techniques and tools. To avoid the implementation of further formalism-specific analysis tools for all these formalism variants, it would be helpful to develop and use a formal mapping of the considered formalisms to a kernel formalism for which analysis techniques and tools do already exist.
Therefore, in this thesis, for a broad class of transformation-based modeling formalisms, we have introduced a technique to relate two formalisms with respect to their semantical properties of interest. The provided connection enables the usage of the analysis methods and tools available for the target formalism also for the source formalism. As a class of considered formalisms we have chosen M-adhesive transformation systems based on M-adhesive categories, which share common technical properties and include many relevant notions used for the modeling of system behavior and adaptation. The investigated semantical properties include behavioral equivalence, (local) confluence, termination, functional behavior as well as parallel and sequential independence of transformations.
To establish the described formal relationship between different M-adhesive transformation systems, we have developed an abstract framework of M-functors. This framework is introduced first for transformation systems containing only rules without nested application conditions and is then extended to rules with nested application conditions. This extension is non-trivial concerning the technical aspects and is most important for transformation systems in practice.
The developed abstract framework is instantiated for two relevant modeling formalisms. We related both, hypergraph transformation systems and Petri net transformation systems with individual tokens with typed attributed graph transformation systems. The instantiation is executed by providing concrete M-functors from the M-adhesive category of the source transformation system to the M-adhesive category of the target transformation system and by verifying sufficient technical properties required by the developed theory for the involved categories and the constructed concrete M-functors. The common target transformation system of typed attributed graphs is a reasonable choice since, for example, the well-established tool AGG, purpose-built for typed attributed graph transformation systems, allows for modeling, simulation, and, in particular, critical pair analysis, which is the first step towards the confluence analysis.
Komplexe dynamische Systeme können unter Einsatz von graphischen Formalismen adäquat modelliert werden. Insbesondere regelbasierte Graphtransformationsformalismen werden erfolgreich eingesetzt, um sowohl das Systemverhalten als auch Systemveränderungen zu erfassen. Für einige Graphtransformationsformalismen wurden bereits Werkzeuge zur Analyse von semantischen Eigenschaften entwickelt. Weiterführende Entwicklungen von Graphtransformationsformalismen vereinfachen einerseits ihre Anwendung in verschiedenen Kontexten, erfordern jedoch andererseits neue Analysetechniken und Analysewerkzeuge. Um die Entwicklung von solchen zusätzlichen formalismusspezifischen Werkzeugen zu vermeiden, ist die Erforschung und Bereitstellung von formalen Abbildungen solcher Formalismen in einen Kernformalismus mit bereits existierender adäquater Werkzeugunterstützung hilfreich.
In dieser Arbeit haben wir für eine große Klasse von transformationsbasierten Modellierungsformalismen eine Technik entwickelt, um Instanzen von zwei Formalismen (einem Quell- und einem Zielformalismus) miteinander in Beziehung zu setzen. Diese Beziehung garantiert, dass bestimmte relevante semantische Eigenschaften der Instanz des Zielformalismus (wie Verhaltensäquivalenz, (lokale) Konfluenz, Terminierung, funktionales Verhalten sowie parallele und sequentielle Unabhängigkeit von Transformationen) auch von der Instanz des Quellformalismus erfüllt werden. Die entwickelte Technik ermöglicht somit den Einsatz der Analysewerkzeuge des Zielformalismus auch für Instanzen des Quellformalismus. Verhalten sowie parallele und sequentielle Unabhängigkeit von Transformationen. paralleler und sequentieller Unabhängigkeit von Transformationen nachgewiesen. Mit unserer entwickelten Technik setzen wir Formalismen aus der wohletablierten Klasse von M-adhäsiven Transformationssystemen in Beziehung, einer Klasse von Formalismen die zahlreiche relevante graphische Modellierungsformalismen umfasst. Diese Formalismen basieren auf M-adhäsiven Kategorien, die durch eine Liste von fundamentalen technischen Eigenschaften charakterisiert sind und relevante Begrifflichkeiten für die Modellierung und Analyse von Systemverhalten und Systemveränderungen bereitstellen.
Aus formaler Sicht stellen wir die Beziehung zwischen zwei M-adhäsiven Transformationssystemen mit Hilfe von sogenannten M-Funktoren her. Die hierfür benötigte Theorie entwickeln wir im ersten Schritt für Transformationssysteme ohne verschachtelten Anwendungsbedingungen und verallgemeinern diese nachfolgend für Transformationssysteme mit verschachtelten Anwendungsbedingungen. Der Erweiterungsschritt ist formal anspruchsvoll jedoch von großer praktischer Bedeutung, da die Verwendung von verschachtelten Anwendungsbedingungen die Ausdrucksmächtigkeit der Transformationssysteme erhöht und eine breite Verwendung bei der Modellierung findet.
Wir demonstrieren die Anwendbarkeit unseres auf der Ebene von M-adhäsiven Transformationssystemen entwickelten abstrakten Ansatzes durch seine Instanziierung für konkrete relevante Modellierungsformalismen. Wir setzen sowohl Hypergraphtransformationssysteme als auch Petri-Netz-Transformationssysteme mit individuellen Marken jeweils mit den entsprechenden getypten attributierten Graphtransformationssystemen in Beziehung. Für diese Instanziierung definieren wir zunächst jeweils einen konkreten M-Funktor zwischen der M-adhäsiven Kategorie des Quelltransformationssystems und der M-adhäsiven Kategorie des Zieltransformationssystems und verifizieren im Anschluss, dass der definierte M-Funktor in Verbindung mit den involvierten M-adhäsiven Kategorien die durch die Theorie vorgegebenen hinreichenden Bedingungen erfüllt.
