258
pages

Voir plus
Voir moins

Vous aimerez aussi

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 conﬂicts and causal dependencies between

transformations, and the of local conﬂuence in cases of conﬂicts. 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 certiﬁcation of a selection of properties

in rule-based models. The certiﬁcation, based on graph transformation analysis techniques,

is illustrated by a case study of an elevator control system. Moreover, the current tool sup-

port for certiﬁcation 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 Konﬂikten oder kausalen Abhangigk¨ eiten zwischen Transfor-

mationen, und das Feststellen von lokaler Konﬂuenz im Falle eines Konﬂikts. Zu diesem

Zweck wurde die Theorie der kritischen Paare erweitert. Es werden auch neuartige Analy-

setechniken eingefuhrt¨ und die bisherigen werden teilweise efﬁzienter 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 Zertiﬁzierung einer Auswahl

von Eigenschaften der regelbasierten Modelle fuhrt.¨ Die Zertiﬁzierung, basierend auf Ana-

lysetechniken fur¨ Graphtransformation, wird illustriert am Fallbeispiel einer Fahrstulkon-

¨trolle. Ausserdem wird die aktuelle Werkzeugunterstutzung in AGG, hinsichtlich der Zer-

tiﬁzierung 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, beneﬁt 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, ﬂoor 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 ofﬁce 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 Conﬂicts and Causal Dependencies for Transformations . . . . . . . . . . . 52

2.7 Critical Pairs and Critical Sequences . . . . . . . . . . . . . . . . . . . . . 62

2.8 Independence, Conﬂicts and Causal Dependencies for Rules . . . . . . . . 72

2.9 Applicability and Non-Applicability of Rule Sequences . . . . . . . . . . . 79

2.10 Embedding and Conﬂuence . . . . . . . . . . . . . . . . . . . . . . . . . . 94

2.11 Efﬁcient Conﬂict 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 Conﬂicts and Causal Dependencies for Transformations . . . . . . . . . . . 140

3.7 Critical Pairs and Critical Sequences . . . . . . . . . . . . . . . . . . . . . 148

3.8 Independence, Conﬂicts and Causal Dependencies for Rules . . . . . . . . 154

3.9 Applicability and Non-Applicability of Rule Sequences . . . . . . . . . . . 162

3.10 Embedding and Conﬂuence . . . . . . . . . . . . . . . . . . . . . . . . . . 174

3.11 Efﬁcient Conﬂict and Causal Dependency Detection . . . . . . . . . . . . . 183

54 Certifying Rule-Based Models 185

4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185

4.2 Road to Certiﬁcation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 difﬁcult 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 speciﬁc 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 ﬁnding 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 ﬁnd

out more about the character of the music. When examining the scores, it is easy to ﬁnd

out the timbre in which a piece of music is written. If someone does not have an absolute

pitch, however, it becomes difﬁcult to ﬁnd out the timbre just by listening to the music. In

particular, when analyzing contemporary music, speciﬁc 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 reﬂect 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 speciﬁc properties hold in our

system, then they can be veriﬁed on the rule-based model of our system. If the veriﬁcation

of the property by means of graph transformation theory is successful, then a corresponding

certiﬁcation 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 ﬁelds [30,

108], for example, the modeling of distributed systems, visual language deﬁnition, 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 modiﬁcations 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 signiﬁcantly 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 speciﬁc 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 speciﬁc 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 speciﬁc 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 ﬁrst 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 efﬁciency 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 speciﬁc properties of rule-based models.

If the veriﬁcation of the property is successful, then a corresponding certiﬁcate can be

awarded. Moreover, for a selection of properties the road to certiﬁcation 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 certiﬁ-

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

certiﬁed 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 speciﬁc 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 efﬁciency of existing analysis techniques detecting statically potential conﬂicts 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

speciﬁcation 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 certiﬁcation 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 inﬁnitely big (cf. run

time). A selection of properties, signiﬁcant for rule-based models, is presented, for which

the road to certiﬁcation is described. On the running example of the elevator control it is

illustrated how each of these properties can be certiﬁed. 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 certiﬁcation 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 certiﬁcation

approach of rule-based models as presented in this thesis can be a good alternative to other

veriﬁcation 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