Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-2032
Main Title: Behavioral Congruences and Verification of Graph Transformation Systems with Applications to Model Refactoring
Translated Title: Verhaltenskongruenzen und Verifikation von Graphtransformationssystemen mit Anwendungen auf Modell-Refactoring
Author(s): Salum Rangel, Guilherme
Advisor(s): Ehrig, Hartmut
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Das 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.
The 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.
URI: urn:nbn:de:kobv:83-opus-20807
http://depositonce.tu-berlin.de/handle/11303/2329
http://dx.doi.org/10.14279/depositonce-2032
Exam Date: 14-Nov-2008
Issue Date: 25-Nov-2008
Date Available: 25-Nov-2008
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Bisimulation
Borrowed-Context
Graphtransformation
Modell-Refactoring
Verhaltenskongruenzen
Behavioral Congruences
Bisimulation
Borrowed Context
Graph Transformation
Model Refactoring
Creative Commons License: https://creativecommons.org/licenses/by-sa/2.0/de
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_36.pdf3.48 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.