Abstraction and abstraction refinement in the verification of graph transformation systems [Elektronische Ressource] / von Vitaly Kozyura

Sujets

• Informatik

Informations

• Publié par: universitat_duisburg-essen
• Publié le: 01 janvier 2009
• Nombre de lectures: 11
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Abstraction and Abstraction Refinement
in the Verification of
Graph Transformation Systems
Vom Fachbereich Ingenieurwissenschaften
Abteilung Informatik und angewandte Kognitionswissenschaft
der Unversit¨at Duisburg-Essen
zur Erlangung des akademischen Grades eines
Doktor der Naturwissenschaften (Dr.-rer. nat.)
genehmigte Dissertation
von
Vitaly Kozyura
aus Magadan, Russland
Referent: Prof. Dr. Barbara K¨onig
Korreferent: Prof. Dr. Arend Rensink
Tag der mu¨ndlichen Pru¨fung: 05.08.2009Abstract
Graph transformation systems (GTSs) form a natural and convenient specification
language which is used for modelling concurrent and distributed systems with dynamic
topologies. These can be, for example, network and Internet protocols, mobile processes
with dynamic behavior and dynamic pointer structures in programming languages. All
this,togetherwiththepossibilitytovisualizeandexplainsystembehaviorusinggraphical
methods, makes GTSs a well-suited formalism for the specification of complex dynamic
distributed systems.
Under these circumstances the problem of checking whether a certain property of
GTSs holds – the verification problem – is considered to be a very important question.
Unfortunately the verification of GTSs is in general undecidable because of the Turing-
completeness of GTSs. In the last few years a technique for analysing GTSs based on
approximation by Petri graphs has been developed. Petri graphs are Petri nets having
additional graph structure.
In this work we focus on the verification techniques based on counterexample-guided
abstraction refinement (CEGAR approach). It starts with a coarse initial over-approxi-
mation of a system and an obtained counterexample. If the counterexample is spurious
then one starts a refinement procedure of the approximation, based on the structure of
the counterexample. The CEGAR approach has proved to be very successful for the
verification of systems based on their over-approximations.
This thesis investigatesa counterexample-guidedabstractionrefinement approachfor
systemsmodelledwithGTSs. Startingwithagivenspuriouscounterexample,wedescribe
here how to construct a more exact approximation (by separating merged nodes) for
which this counterexamples disappears. This procedure can be performed repeatedly
for any number of spurious counterexamples. Furthermore, an incremental coverability
approach for Petri nets is developed, which allows one to speed-up the construction of
over-approximations of GTSs.
A well-known approach is to extend a modelling language with the possibility of de-
scribing attributes as values of some data types. The approximation-based verification
technique, including a counterexample-guided abstraction refinement, is hence also gen-
eralized in this work to attributed GTSs (AGTSs), where the attributes are abstracted
in the framework of abstract interpretation.
In the practical part, a verification tool Augur 2 is developed, which supports the
whole verification process for GTSs and AGTSs. A number of case studies (both at-
tributed and non-attributed GTSs) were successfully solved with Augur 2.Acknowledgement
First of all, I would like to thank my doctoral adviser, Barbara K¨onig, for being my
supervisor, for encouraging and challenging me throughout the academic program. This
workwouldnot havebeen possible without her. I wantto express my gratitudeto Javier
Esparza, whose works on Petri net unfolding have awakened my interests to the related
areasofcomputerscience. Ithankhimalsoforhissupportandadvicesonvariousaspects
of my work.
I also would like to thank my colleagues, Sander Bruggink, Tobias Heindel, Stefan
Kiefer, Michael Luttenberger, Claus Schr¨oter, Alin Stefanescu and Dejvuth Suwimon-
teerabuth, for their help and many interesting discussions on the topics of this thesis.
Also I thank a lot all students have being involved in the development of the verification
tool Augur. It was a very interesting and pleasant team work experience.
I am very grateful to my family, to my parents for their lifelong support, and to my
wife for being my friend and companion.
Finallymythanksgotothereviewersofthisthesisforreadingtheresultofmyefforts.Contents
1 Introduction 3
1.1 Verification of Graph Transformation Systems . . . . . . . . . . . . . . . . 3
1.2 Summary and Contribution of the Thesis . . . . . . . . . . . . . . . . . . 5
1.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.5 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2 Petri Nets 13
2.1 Introduction to Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Coverability Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3 Incremental Calculation of Coverability Graphs . . . . . . . . . . . . . . . 18
2.4 Backward Coverability Algorithm . . . . . . . . . . . . . . . . . . . . . . . 23
3 Graph Transformation Systems 26
3.1 Introduction to Graph Transformation Systems . . . . . . . . . . . . . . . 26
3.2 Verification of Graph Transformation Systems . . . . . . . . . . . . . . . . 28
4 Attributed Petri Nets and Graph Transformation Systems 37
4.1 Algebras and Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2 Attributed Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.3 Attributed Graph Transformation Systems. . . . . . . . . . . . . . . . . . 42
4.4 Verification of Attributed Graph Transformation Systems . . . . . . . . . 45
5 Counterexample-Guided Abstraction Refinement 53
5.1 Abstraction Refinement of Graph Transformation Systems . . . . . . . . . 53
5.1.1 Spurious Runs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.1.2 Relations on Nodes for Refining Abstract Runs . . . . . . . . . . . 55
5.1.3 Elimination of Spurious Runs . . . . . . . . . . . . . . . . . . . . . 58
5.1.4 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
5.2 Abstraction Refinement of Attributed Graph Transformation Systems . . 63
6 Augur – a Tool for the Analysis of Graph Transformation Systems 69
6.1 Brief Description of Augur 1 . . . . . . . . . . . . . . . . . . . . . . . . . 69
6.2 Software Design of Augur 2 . . . . . . . . . . . . . . . . . . . . . . . . . 70
6.3 System Architecture of Augur 2 . . . . . . . . . . . . . . . . . . . . . . . 72
6.4 Functionality and Usage . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
17 Case Studies 83
7.1 Public-Private Servers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
7.2 Firewall . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
7.3 Experiments with the Incremental Coverability Approach . . . . . . . . . 91
7.4 Random Graph Transformation Systems - Statistical Results . . . . . . . 93
7.5 Verifying Red-Black Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
7.6 Leader Election Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
7.7 Needham-Schroeder Protocol . . . . . . . . . . . . . . . . . . . . . . . . . 104
8 Conclusion and Future Work 108
A Basic Category Theory for Graph Rewriting 118
B Example in GTXL format 122
C Example in new GTXL format 124
D Example in GXL format 127
E Example of an SPL program 129
F Verification Example 131
2Chapter 1
Introduction
1.1 Verification of Graph Transformation Systems
In the last decades, the development of computers and networks, the appearance and
the rapidexpansionofInternettechnologieshaveled to increasingcomplexityandstrong
interconnection of computer systems. Under these circumstances, the problem of mod-
elling and analyzing complex distributed systems is considered to be a very important
question. Unfortunately, many of today’s methods describe distributed and mobile sys-
tems with formalisms that either have an infinite state space, making many interesting
questions undecidable, or a very a large state space, leading to the so-called state explo-
sion problem. This makes the important problem of modelling and verificationof mobile
and distributed systems a very difficult one.
The approach in this thesis is based on a rather natural and expressive modelling
language, namely graph transformation systems (GTSs) [95]. GTSs have their origin in
the late 1960’s and were developed up to now into a rich theory with many different
branches. The development was originally motivated by such areas of computer science
as pattern recognition, description of data types and compiler construction. Later, more
modern branches of computer science, such as computer networks with different topolo-
gies, mobile processes, UML diagrams and web services have also been specified and
analysed with GTSs. Being a natural generalization of formal language theory, based
on string rewriting and the theory of term rewriting, GTSs are also interesting from a
theoretical point of view.
For many structures in computer science, a static description of system states can be
obtained with the help of graphs in a rather natural way. As an example, we consider
computernetworks,wherestationscanberepresentedasnodesofgraphsandthenetwork
connections as edges. As a more specific example, we mention here pointer structures on
the heap in a programming lan