//img.uscri.be/pth/cfc27f24d08b4df5b2b44d13ac70e47368b63cbc
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

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

258 pages
Certifying Rule-Based Modelsusing Graph Transformationvorgelegt vonDiplom-MathematikerinLeen LambersFakultat¨ IV — Elektrotechnik und Informatikder Technischen Universitat¨ Berlinzur Erlangung des akademischen GradesDoktor der NaturwissenschaftenDr. rer. natgenehmigte DissertationPromotionsausschuss:Vorsitzende: Prof. Dr. Sabine GlesnerBerichter: Prof. Dr. Hartmut Ehrig Prof. Dr. Fernando OrejasBerichterin: Prof. Dr. Gabriele TaentzerTag der wissenschaftlichen Aussprache: 30. Oktober 2009Berlin 2010D 83AbstractMany systems exhibit rule-based behavior that can be modeled very well by means of graphtransformation. In this thesis, a new graph transformation theory is introduced for a moreexpressive 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 alsoallows so-called negative application conditions. Present analysis techniques are extendedfor this more expressive kind of graph transformation. These allow, amongstother things, the static detection of potential conflicts and causal dependencies betweentransformations, 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 techniquesare introduced and present techniques are improved. One new technique enables, for exam-ple, the static analysis of applicability (resp. non-applicability) of rule sequences.
Voir plus Voir moins

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
4.4 Application Areas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230
4.5 Tool Support . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
5 Comparing, Concluding, and Continuing 237
5.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237
5.2 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241
5.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243Chapter 1
Introduction
When people in a concert hall are listening, for example, to a Beethoven piano sonata, then
they are probably simply enjoying a wonderful evening of music. Only a minority of the
audience might be aware of the fact that some modeling was conducted in order to realize
such a concert evening. If there were no scores, for example, it would be very difficult for
the musicians to play the piano sonata that Beethoven had in mind about two hundred years
ago. Instead, Beethoven wrote down the notes for his piece of music into scores, and that
is why people today can still enjoy his music. Precisely these scores can be understood as
a model for his music.
By means of the musical example, I would like to point out to the reader, in an intro-
ductory way, the characteristics of modeling that play an important role in this thesis. In
particular, I concentrate on the way models abstract from contextual data, the communi-
cation of models by formulating them in a specific language, and how models provide an
advantage for the analysis of the modeling subject.
A fundamental property of models is that they abstract from the reality that they de-
scribe. For example, the scores for the piano sonata usually do not give any information
about which pianist should interpret them – or even on which kind of piano the music
should be played. As long as the pianist masters the techniques required for playing the
music, expressed by the scores, the concert evening can take place. Moreover, the model
does not give complete information about the temperament of the artist when playing the
music. Therefore, although the notes are the same, and annotations on the scores about
tempo, temperament, and sound volume might be given, concerts will be similar, but not
identical. There is still freedom for the artist when interpreting the scores.
Another important property of models is that they are expressed in a proper modeling
language, which can be understood or should be learnt by the model interpreter. For exam-
ple, musicians understand the language of scores after learning how to read them. Thanks
to this common language, composers can communicate their music – the subject that they
are modeling. Moreover, as already mentioned, the existence of such a modeling language
for music enables us to listen to music that was composed a couple of centuries earlier. The
scores keep hold of the music in their own language.
7CHAPTER 1. INTRODUCTION
A third property of models, which I would like to highlight, is that their analysis is useful
for finding out more about the modeling subject. For example, music theoreticians listen
to live or recorded music of a certain composition in order to understand better what the
composer is trying to express with it. However, in addition, they examine the scores to find
out more about the character of the music. When examining the scores, it is easy to find
out the timbre in which a piece of music is written. If someone does not have an absolute
pitch, however, it becomes difficult to find out the timbre just by listening to the music. In
particular, when analyzing contemporary music, specific kinds of mathematical techniques
might be used to examine the scores. Such type of analysis leads to a better understanding
of the music. It would be very tedious – or sometimes nearly impossible – to arrive at the
same level of understanding by just listening to the music. Even in the case that merely
scores, and no recordings, for some musical piece are available, it is possible to obtain a
good impression of the music through examining the scores.
The kind of models that I concentrate on in this thesis are rule-based. Rules are able
to reflect dynamics in the system being modeled in the following way: they express what
condition holds before (resp. after) a certain system change occurs. A rule, therefore,
encloses a so-called precondition and postcondition. The modeling language I concentrate
on in this thesis is graph transformation [109]. It is a visual and formal language enabling
us to describe rule-based models in a very concise way. In addition, it enables us to apply
analysis techniques on these models. If we expect that specific properties hold in our
system, then they can be verified on the rule-based model of our system. If the verification
of the property by means of graph transformation theory is successful, then a corresponding
certification may be added to the rule-based model.
The use of graph transformation as a modeling language for systems showing rule-
based behavior has been successful in the last few decades in many application fields [30,
108], for example, the modeling of distributed systems, visual language definition, object-
oriented modeling, and model transformation. The advantage of graph transformation is
that, on the one hand graphs visualize in a natural way the inner structure of complex sys-
tem data and on the other hand, we have graph rules expressing modifications of these
structures in an easily understandable and schematic way. Another important advantage
is the formal foundation of graph transformation, enabling concise modeling and formal
analysis. The expressiveness of graph transformation has been increased significantly since
its emergence in the 70s as generalization of Chomsky grammars and term rewriting in
the context of formal languages. In the mean time, graph transformation is able to sup-
port the precise modeling of a wide range of applications. However, the development of
corresponding graph transformation theory has not always kept up with this evolution.
Therefore, the formal analysis of these more expressive models becomes at least inac-
curate or impossible. In order to verify specific properties of rule-based models, graph
transformation theory is indispensable though. Moreover, it is important for the increasing
success of this modeling technique. In particular, if safety-critical systems are modeled us-
ing graph transformation, then powerful analysis techniques are essential. Furthermore, in
view of the commercialization of specific applications, formal analysis of the correspond-
ing models can be of particular importance in order to avoid expensive development cycle
8iterations.
Negative application conditions (NACs) [44] make graph transformation more expres-
sive as a modeling technique. However, the development of theory has not completely kept
up with the introduction of these conditions. NACs forbid specific structures before or after
applying a rule, and are already used extensively in modeling praxis using graph transfor-
mation (see, for example, [19, 59, 84, 116]). Therefore, as the first main topic in this thesis,
we concentrate on the generalization of analysis techniques for graph transformation with
so-called negative application conditions (NACs). In addition, the efficiency of already ex-
isting analysis techniques is improved, and new kinds of analysis techniques are proposed.
As a second topic in this thesis, we propose a generic way to apply analysis techniques,
rooted in graph transformation theory, to verify specific properties of rule-based models.
If the verification of the property is successful, then a corresponding certificate can be
awarded. Moreover, for a selection of properties the road to certification is outlined, using
graph transformation analysis techniques. This allows for documenting and developing
concise tool support with regard to these properties, enabling the automation of the certifi-
cation process.
This thesis starts off with an informal description of the main contents of this work at
the end of this chapter. It should enable the reader to decide if the of this thesis
might be interesting to study more in detail. First, we introduce the running example, the
control of an elevator, and use it to illustrate the characteristics of rule-based modeling.
Moreover, we explain how graph transformation comes into play for the purpose of rule-
based modeling. Finally, we sketch the main properties, dealt with in this thesis, that can be
certified using graph transformation, and illustrate it on the example of the elevator control.
Chapter 2 is concerned with presenting the graph transformation theory that can be used
for rule-based modeling. One of the main achievements of this thesis is that existing graph
transformation theory in the algebraic approach is extended to graph transformation with
so-called negative application conditions. These conditions express that specific structures
are forbidden before or after applying a rule. Another achievement of this thesis, with
regard to the extension of graph transformation theory, is the introduction of a new analysis
technique, called applicability analysis of rule sequences. Moreover, this thesis improves
the efficiency of existing analysis techniques detecting statically potential conflicts and
causal dependencies between rules. The theory introduced in this chapter is explained
continuously using the running example of the elevator control. Note that most results in
this chapter are instantiated from the corresponding results in the abstract framework of
adhesive HLR systems with NACs, as presented in the next chapter.
Chapter 3 presents the main results of Chapter 2 in the more abstract framework of ad-
hesive HLR systems with NACs, another important achievement of this work. This abstract
framework is based on a special kind of category, called the NAC-adhesive HLR category.
Formulating all results on this more abstract level has the following main advantages: the
proof reasoning for all results is performed on the basis of category theory, mostly allow-
ing for more elegant and compact proofs than for the set-theoretical case. Moreover, the
obtained results can be instantiated for the transformation theory of all kinds of high-level
structures. Not only graph transformation is a valid instantiation, but also, for example,
9CHAPTER 1. INTRODUCTION
typed attributed graph transformation, hypergraph transformation, algebraic signature or
specification transformation, and Petri net transformation. Readers who are not interested
in the categorical background of rule-based modeling, as presented in this chapter, might
also skip it.
After these two theoretical chapters, Chapter 4 explains how this theory can be applied
for the purpose of certifying rule-based models using graph transformation. It presents a
general road map towards certification supported by analysis techniques based on graph
transformation theory. In this thesis, thereby, we concentrate on static analysis techniques.
They run on components of the rule-based model without actually applying the rules (cf.
compile time). In contrast, dynamic techniques might have to run through the whole state
space generated by the rule-based model, which in many cases is infinitely big (cf. run
time). A selection of properties, significant for rule-based models, is presented, for which
the road to certification is described. On the running example of the elevator control it is
illustrated how each of these properties can be certified. Moreover, typical application areas
are described for certifying rule-based models using graph transformation, as presented
in this thesis. Finally, in this chapter, tool support for certifying rule-based models is
discussed. In particular, a survey is given on tool support for the certification process
in the tool environment AGG [115, 114, 13, 1]. It supports the algebraic approach to
graph transformation, and consists of a graph transformation engine, analysis tools and a
graphical user interface for convenient user interaction.
Chapter 5 starts with an overview of related work. It points out why the certification
approach of rule-based models as presented in this thesis can be a good alternative to other
verification techniques for graph transformation. In the second section of this chapter,
we summarize the main results of this thesis, and outline the relationship with own work
published already. Finally, in the last section, the most important lines of future work
arising from this thesis are discussed.
10