Certifying rule-based models using graph transformation [Elektronische Ressource] / vorgelegt von Leen Lambers

Sujets

• Informatik

Informations

• Publié par: technische_universitat_berlin
• Publié le: 01 janvier 2009
• Nombre de lectures: 9
• Langue: English
• Poids de l'ouvrage: 12 Mo

Extrait

Certifying Rule-Based Models
using Graph Transformation
vorgelegt von
Diplom-Mathematikerin
Leen Lambers
Fakultat¨ IV — Elektrotechnik und Informatik
der Technischen Universitat¨ Berlin
zur Erlangung des akademischen Grades
Doktor der Naturwissenschaften
Dr. rer. nat
genehmigte Dissertation
Promotionsausschuss:
Vorsitzende: Prof. Dr. Sabine Glesner
Berichter: Prof. Dr. Hartmut Ehrig Prof. Dr. Fernando Orejas
Berichterin: Prof. Dr. Gabriele Taentzer
Tag der wissenschaftlichen Aussprache: 30. Oktober 2009
Berlin 2010
D 83Abstract
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 transfor-
mation 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 allow, amongst
other things, the static detection of potential conflicts and causal dependencies between
transformations, and the of local confluence in cases of conflicts. For this pur-
pose, 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 exam-
ple, 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 transforma-
tion. 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. Fi-
nally, 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 sup-
port for certification of rule-based models using graph provided by AGG is
outlined.Zusammenfassung
Viele Systeme zeigen regelhaftes Verhalten auf was sehr gut durch Graphtransformation
modelliert werden kann. Diese Dissertation fuhrt¨ eine neue Graphtransformationstheorie
fur¨ eine ausdruckskraftigere¨ 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 fur¨ diese
ausdruckskraftigere¨ Variante. Diese Techniken ermoglichen¨ unter anderem das statische
Aufspuren¨ von potentiellen Konflikten oder kausalen Abhangigk¨ eiten zwischen Transfor-
mationen, und das Feststellen von lokaler Konfluenz im Falle eines Konflikts. Zu diesem
Zweck wurde die Theorie der kritischen Paare erweitert. Es werden auch neuartige Analy-
setechniken eingefuhrt¨ und die bisherigen werden teilweise effizienter gemacht. Eine der
¨ ¨neuen Techniken ermoglicht zum Beispiel eine statische Prufung der Anwendbarkeit bzw.
Nicht-Anwendbarkeit von Regelsequenzen. Der Hauptteil der entwickelten Theorie in die-
ser Dissertation ist nicht nur auf Graphtransformationen anwendbar. Sie wird ausserdem
formuliert im abstrakteren Rahmenwerk der adhesiven High-Level-Transformation. Somit
konnen¨ 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 fuhrt.¨ Die Zertifizierung, basierend auf Ana-
lysetechniken fur¨ Graphtransformation, wird illustriert am Fallbeispiel einer Fahrstulkon-
¨trolle. Ausserdem wird die aktuelle Werkzeugunterstutzung in AGG, hinsichtlich der Zer-
tifizierung von regelbasierten Modellen mittels Graphtransformation, vorgestellt.Acknowledgements
Writing this thesis was a challenge that I was able to accept, by and by, thanks to the
encouragement of several people accompanying me during the last few years.
In particular, I would like to thank . . .
Hartmut Ehrig, for the continuous monitoring of this thesis and for giving me the oppor-
tunity to work in your group, benefit from your wealth of experience, and learn from the
accuracy and intensity that you apply when doing research.
Fernando Orejas, for enabling my research stays at the UPC in Barcelona where we had
several inspiring discussions, providing a solid basis for joint work and encouraging me to
keep working on many subjects elaborated in this thesis.
Gabriele Taentzer, for your valuable comments with regard to this thesis, for believing
in my skills, and for being such an animating counterpart. I hope to be able to continue
our close cooperation in the near future. In this regard, many thanks also to Stefan Jurack
and Katharina Mehner for our productive Berlin-Marburg-Munich collaboration during the
past two years.
Mauro Pezze,` for facilitating my research stay in your group at the university of Milano,
Bicocca, where you gave me the opportunity to report on my research and to learn about
inventive applications developed in your lab. In this regard, special thanks also to Leonardo
Mariani, for the fruitful cross-border cooperation beyond my stay and to all members of
the lab, for being such welcoming interim colleagues.
Annegret Habel, for our recently started cooperation – in the middle of writing up this
thesis. I look forward to continuing our joint work.
The many friendly and inspiring colleague researchers of the graph transformation com-
munity that I met during conferences, workshops, and research stays, making these gath-
erings to memorable and motivating experiences.
My colleagues in Berlin, with whom I share – or shared – daily working life, for your
companionship during seminars, co-authoring papers, teaching, TFS breakfasts, coffee
breaks, floor chats, . . . . Special thanks to Claudia Ermel, Ulrike Prange, and Alexander
Rein for carefully proofreading parts of this thesis, and to Olga Runge, for being so hard-
¨working when implementing new features in AGG. Thank you to Kate Schlicht, for your
support concerning all kinds of administrative matters. Moreover, many thanks to Maria
Oswald and Margit Russ, for the enjoyable joint time as office mates.
My friends, for having fun with me and encouraging me, and giving me timely distrac-
tions from graph transformation and all that kind of stuff. Special thanks to Mieke, for
your professional advice with regard to the musical example in the introduction.
My family, and in particular, my parents, for presenting me with an always welcoming
home, helping me to hang in there: ”bedankt”.
Daniel, for giving me the special kind of energy needed to bring this thesis to an end.Contents
1 Introduction 7
2 Rule-Based Modeling using Graph Transformation 17
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Modeling with Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3 Rule-Based Modeling using Graph Transformation . . . . . . . . . . . . . 26
2.4 Independence and Parallelism . . . . . . . . . . . . . . . . . . . . . . . . 40
2.5 Concurrency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
2.6 Conflicts and Causal Dependencies for Transformations . . . . . . . . . . . 52
2.7 Critical Pairs and Critical Sequences . . . . . . . . . . . . . . . . . . . . . 62
2.8 Independence, Conflicts and Causal Dependencies for Rules . . . . . . . . 72
2.9 Applicability and Non-Applicability of Rule Sequences . . . . . . . . . . . 79
2.10 Embedding and Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . 94
2.11 Efficient Conflict and Causal Dependency Detection . . . . . . . . . . . . . 104
3 Rule-Based Modeling using High-Level Transformation 113
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
3.2 Modeling with High-Level Structures . . . . . . . . . . . . . . . . . . . . 115
3.3 Rule-Based Modeling using High-Level Transformation . . . . . . . . . . 121
3.4 Independence and Parallelism . . . . . . . . . . . . . . . . . . . . . . . . 126
3.5 Concurrency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
3.6 Conflicts and Causal Dependencies for Transformations . . . . . . . . . . . 140
3.7 Critical Pairs and Critical Sequences . . . . . . . . . . . . . . . . . . . . . 148
3.8 Independence, Conflicts and Causal Dependencies for Rules . . . . . . . . 154
3.9 Applicability and Non-Applicability of Rule Sequences . . . . . . . . . . . 162
3.10 Embedding and Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . 174
3.11 Efficient Conflict and Causal Dependency Detection . . . . . . . . . . . . . 183
54 Certifying Rule-Based Models 185
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
4.2 Road to Certification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186
4.3 Certifying a Selection of Properties . . . . . . . . . . . . . . . . . . . . . . 194