Behavior and confluence analysis of M-adhesive transformation systems using M-functors

dc.contributor.advisorNestmann, Uwe
dc.contributor.authorMaximova, Maria
dc.contributor.grantorTechnische Universität Berlinen
dc.contributor.refereeNestmann, Uwe
dc.contributor.refereeKönig, Barbara
dc.contributor.refereePadberg, Julia
dc.contributor.refereeErmel, Claudia
dc.date.accepted2019-03-26
dc.date.accessioned2019-12-20T10:49:21Z
dc.date.available2019-12-20T10:49:21Z
dc.date.issued2019
dc.description.abstractFor 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.en
dc.description.abstractKomplexe 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.de
dc.identifier.urihttps://depositonce.tu-berlin.de/handle/11303/10521
dc.identifier.urihttp://dx.doi.org/10.14279/depositonce-9454
dc.language.isoenen
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subject.ddc006 Spezielle Computerverfahrende
dc.subject.othergraph transformationen
dc.subject.otherM-adhesive transformation systemen
dc.subject.otherconfluenceen
dc.subject.othertranslational verificationen
dc.subject.othercritical pair analysisen
dc.subject.otherGraphentransformationde
dc.subject.otherM-adhäsives Transformationssystemde
dc.subject.otherKonfluenzde
dc.subject.otherÜbersetzungsverifikationde
dc.subject.otherkritische Paaranalysede
dc.titleBehavior and confluence analysis of M-adhesive transformation systems using M-functorsen
dc.title.translatedVerhaltens- und Konfluenzanalyse von M-adhäsiven Transformationssystemen mittels M-Funktorende
dc.typeDoctoral Thesisen
dc.type.versionacceptedVersionen
tub.accessrights.dnbfreeen
tub.affiliationFak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik::FG Modelle und Theorie Verteilter Systemede
tub.affiliation.facultyFak. 4 Elektrotechnik und Informatikde
tub.affiliation.groupFG Modelle und Theorie Verteilter Systemede
tub.affiliation.instituteInst. Softwaretechnik und Theoretische Informatikde
tub.publisher.universityorinstitutionTechnische Universität Berlinen

Files

Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
maximova_maria.pdf
Size:
5.83 MB
Format:
Adobe Portable Document Format
Description:
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.9 KB
Format:
Item-specific license agreed upon to submission
Description:

Collections