Behavioral Congruences and Verification of Graph Transformation Systems with Applications to Model Refactoring

dc.contributor.advisorEhrig, Hartmuten
dc.contributor.authorSalum Rangel, Guilhermeen
dc.contributor.grantorTechnische Universität Berlin, Fakultät IV - Elektrotechnik und Informatiken
dc.date.accepted2008-11-14
dc.date.accessioned2015-11-20T18:29:12Z
dc.date.available2008-11-25T12:00:00Z
dc.date.issued2008-11-25
dc.date.submitted2008-11-25
dc.description.abstractDas Konzept von Borrowed-Contexts eröffnete für Graphtransformationen die Möglichkeit eines externen ''Beobachters'', wobei Graphen (als Spezifikationen von Systemen) mit einer Umgebung kommunizieren können, um sich zu entwickeln. Dies führt zu offenen Systemen, in denen internes (nicht beobachtbares) und externes (beobachtbares) Verhalten unterschieden werden. Die beobachtbaren Interaktionen bilden ein Transitionssystem derart, dass Bisimilaritäten automatisch Kongruenzen sind. Das heißt, wenn ein Graph bisimilar zu einem anderen ist, können beide Graphen im Kontext eines größeren Graphen ohne Auswirkung auf das beobachtbare Verhalten ausgetauscht werden. Dieses Ergebnis ist sehr nützlich für Modell-Refactoring, weil ein Teil des Modells durch ein bisimilares Teil ersetzt werden kann. Das Hauptziel dieser Arbeit besteht darin, den Ansatz von Graphtransformationen mit Borrowed-Contexts weiter zu entwickeln und auch seine Eignung zur Analyse der Bewahrung des Verhaltens im Anwendungsgebiet Modell-Refactoring zu erforschen. Erstens erweitern wir den Borrowed-Context Ansatz auf Regeln mit negativen Anwendungsbedingungen, die oft in komplexen Spezifikationen verwendet werden. Dies bedeutet, dass eine Regel nur angewendet werden darf, wenn bestimmte Muster außerhalb einer linken Seite abwesend sind. Diese Erweiterung, die im Rahmen von Adhesiven Kategorien durchgeführt wird, erfordert auch eine Erweiterung der Label des Transitionssystems um negative Anwendungsbedingungen. Als wichtiges Ergebnis zeigen wir, dass die Bisimilarität immer noch eine Kongruenz ist, wenn Regeln negative Anwendungsbedingungen haben. Die Erfahrung zeigt, dass Bisimulationsbeweise langwierig und sehr fehleranfällig werden, wenn sie von Hand durchgeführt werden. Um dieses Problem zu lösen, haben wir einen bestehenden ''on-the-fly'' Bisimulations-Algorithmus um zusätzliche Prozeduren zur Mechanisierung der Überprüfung der Bisimilarität von Graphen im Rahmen des Borrowed Context Ansatzes definiert. Dieser Algorithmus bildet den Kern einer Werkzeugunterstützung für die Entwicklung von Techniken zur Verhaltensanalyse basierend auf Graphtransformationen mit Borrowed Contexts. Darauf aufbauend werden Techniken definiert, um die Verhaltensbewahrung im Anwendungsbereich Modell-Refactoring zu untersuchen. Verhaltensbewahrung ist immer ein wesentlicher Aspekt jeder Refactoring-Transformation. Eine Technik überprüft die Bisimilarität von Instanzen eines Metamodells in Bezug auf Regeln, die die operationelle Semantik des Metamodells beschreiben, wobei Bisimilarität Verhaltensbewahrung impliziert. Eine zweite Technik bezieht sich auf Verhaltensbewahrung von Refactoring-Regeln. Einer der Vorteile dieser Techniken ist, dass sie nicht an spezifische Metamodelle gebunden sind, sondern auf jedes Metamodell angewendet werden können, deren operationelle Semantik durch endliche Graphregeln beschrieben werden kann.de
dc.description.abstractThe concept of borrowed contexts has opened up graph transformations to the notion of an external ''observer'' where graphs (specifying systems) may interact with an environment in order to evolve. This leads to open systems in which a clear line delimits internal (non-observable) and external (observable) behavior. The observable interactions of a graph build up labeled transition systems such that bisimulations are automatically congruences, which means that whenever one graph is bisimilar to another, one can exchange them in a larger graph without effect on the observable behavior. This result turns out to be very useful for model refactoring, since one part of the model can be replaced by another bisimilar one. The main goal of this thesis is twofold, namely to further develop the borrowed context framework and to explore its suitability as an instrument to reason about behavior preservation in model refactoring. First we extend the borrowed context framework to handle rules with negative application conditions, which are often a required feature of nontrivial system specifications. That is, a rule may only be applied if certain patterns are absent in the vicinity of a left-hand side. This extension, which is carried out for adhesive categories, requires an enrichment of the transition labels which now do not only indicate the context that is provided by the observer, but also constrain further additional contexts that may (not) satisfy the negative application condition. We have shown that bisimilarity is still a congruence when rules have negative application conditions. Experience shows that bisimulation proofs easily become tedious tasks and very prone to error when done by hand. In order to overcome this problem we have extended an existing on-the-fly bisimulation checking algorithm to the borrowed context setting and defined additional procedures to mechanize the verification of graphs for bisimilarity. This algorithm forms the core of a tool support which will enable us to come up with behavior analysis tools based on the borrowed context machinery. Finally, techniques based on borrowed contexts are defined to check model refactorings for behavior preservation, which is always a crucial aspect of every refactoring transformation. One technique checks instances of a metamodel for bisimilarity w.r.t. to a set of productions defining the operational semantics of the metamodel. Bisimilarity implies preservation of behavior. A more elaborate technique shifts the behavior-preservation focus from instances of a metamodel to refactoring rules, where rules are checked for behavior preservation. One of the advantages of these techniques is that they are not tied up to specific metamodels, but rather can be applied to any metamodel whose operational semantics can be described by finite graph productions.en
dc.identifier.uriurn:nbn:de:kobv:83-opus-20807
dc.identifier.urihttps://depositonce.tu-berlin.de/handle/11303/2329
dc.identifier.urihttp://dx.doi.org/10.14279/depositonce-2032
dc.languageEnglishen
dc.language.isoenen
dc.rights.urihttps://creativecommons.org/licenses/by-sa/2.0/deen
dc.subject.ddc004 Datenverarbeitung; Informatiken
dc.subject.otherBisimulationde
dc.subject.otherBorrowed-Contextde
dc.subject.otherGraphtransformationde
dc.subject.otherModell-Refactoringde
dc.subject.otherVerhaltenskongruenzende
dc.subject.otherBehavioral Congruencesen
dc.subject.otherBisimulationen
dc.subject.otherBorrowed Contexten
dc.subject.otherGraph Transformationen
dc.subject.otherModel Refactoringen
dc.titleBehavioral Congruences and Verification of Graph Transformation Systems with Applications to Model Refactoringen
dc.title.translatedVerhaltenskongruenzen und Verifikation von Graphtransformationssystemen mit Anwendungen auf Modell-Refactoringde
dc.typeDoctoral Thesisen
dc.type.versionpublishedVersionen
tub.accessrights.dnbfree*
tub.affiliationFak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatikde
tub.affiliation.facultyFak. 4 Elektrotechnik und Informatikde
tub.affiliation.instituteInst. Softwaretechnik und Theoretische Informatikde
tub.identifier.opus32080
tub.identifier.opus41986
tub.publisher.universityorinstitutionTechnische Universität Berlinen

Files

Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
Dokument_36.pdf
Size:
3.4 MB
Format:
Adobe Portable Document Format

Collections