Directed model checking for timed automata [Elektronische Ressource] / Sebastian Kupferschmid

Sebastian Kupferschmid

Sujets

• Informatik

Informations

• Publié par: albert-ludwigs-universitat_freiburg
• Publié le: 01 janvier 2009
• Nombre de lectures: 24
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

Sebastian Kupferschmid
Directed Model Checking for
Timed Automata
Doktorarbeit
Institut fur¨ Informatik
Technische Fakultat¨
Albert-Ludwigs-Universitat¨ Freiburg
November 2009Tag der Disputation:
18. Dezember 2009
Dekan:
Prof. Dr. Hans Zappe, Albert-Ludwigs-Universitat¨ Freiburg
Gutachter:
Prof. Dr. Bernhard Nebel,sitat¨ Freiburg
Prof. Dr. Andreas Podelski, Albert-Ludwigs-Universitat¨ FreiburgTo my familyZusammenfassung
Die vorliegende Dissertation mit dem Titel “Directed Model Checking for
Timed Automata” befasst sich mit der gerichteten Modellprufung¨ fur¨ Real-
zeitsysteme. Die Arbeit gliedert sich in zwei einfuhrende¨ Teile und einen in-
haltlichen Teil. Der erste Teil fuhrt¨ in das Gebiet der Modellprufung¨ ein. Hier
werden grundlegende Konzepte wie z. B. Kripke Struktur, temporale Logik und
das Problem der Modellprufung¨ vorgestellt. Der Teil endet mit einer kurzen
Beschreibung existierender Modellprufungsv¨ erfahren.
Der zweite Teil behandelt Realzeitsysteme und gerichtete Modellprufung.¨
Er enthalt¨ die Definitionen, die zum Verstandnis¨ dieser Dissertation notig¨ sind.
Zuerst wird die Syntax und die Semantik von Realzeitautomaten eingefuhrt.¨ Da
Zeit in diesem Modell durch reelle Zahlen modelliert wird, ist der Zustands-
raum eines Realzeitautomaten ein uberabz¨ ahlbar¨ großes Transitionssystem. De-
shalb scheinen Realzeitsysteme ungeeignet fur¨ die Modellprufung¨ zu sein. Das
ist allerdings nicht der Fall, da sich diese Zustandsraume¨ endlich partition-
ieren lassen. Im Anschluss wird die gerichtete Modellprufung¨ fur¨ Realzeit-
systeme eingefuhrt.¨ Neben der Vorstellung eines allgemeinen Algorithmus fur¨
die gerichtete Modellprufung¨ werden hier auch existierende Ansatze¨ fur¨ die
gerichtete Modellprufung¨ diskutiert.
Der dritte Teil bildet den Hauptteil der Arbeit. Es werden verschiedene
¨ ¨ ¨Heuristiken und Verbesserungen fur die gerichtete Modellprufung eingefuhrt.
In Kapitel 5 wird die erfolgreichste Relaxierung aus dem Gebiet der Hand-
lungsplanung auf die gerichtete Modellprufung¨ fur¨ Realzeitautomaten adaptiert
und erweitert. Mit den resultierenden Heuristiken ist es moglich,¨ erreichbare
Fehlerzustande¨ in Systemen zu finden, die mit zuvor vorgeschlagenen Heuris-
tiken nicht entdeckt werden konnen.¨ Im darauf folgenden Kapitel wird Pradi-¨
katenabstraktion verwendet, um sogenannte Musterdatenbanken zu erzeugen.
Durch die Kombination von bekannten Techniken aus den Bereichen der Mo-
dellprufung¨ und der kunstlichen¨ Intelligenz erhalt¨ man eine Familie von Heuris-II
tiken, die mit dem aktuellen Stand der Technik mithalten konnen.¨ In Kapitel 7
wird eine weitere Musterdatenbank-Heuristik, die auf dem Prinzip der russis-
chen Puppen basiert prasentiert.¨ Der Ansatz zielt darauf ab, diejenigen Teile
des Systems so gut wie moglich¨ zu erhalten, die unmittelbar relevant fur¨ die zu
uberpr¨ ufende¨ Eigenschaft sind. Mit der resultierenden Heuristik lassen sich be-
weisbar kurzeste¨ Fehlerpfade in den großten¨ unserer Fallbeispiele finden. Mit
der Technik, die in Kapitel 8 prasentiert¨ wird, lasst¨ sich heuristische Suche
im Allgemeinen deutlich beschleunigen. Dieser Ansatz kann mit vielen Heuris-
tiken kombiniert werden und skaliert oft deutlich besser als gierige Suche. Gle-
ichzeitig liefert das Verfahren erheblich kurzere¨ Fehlerpfade als gierige Suche.
Im letzten Kapitel wird zuerst eine auf Gegenbeispielen basierende Abstrak-
tionsverfeinerung fur¨ Realzeitsysteme prasentiert.¨ Danach wird anhand einiger
Beispiele demonstriert, dass gerichtete Modellprufung¨ bei fehlerhaften Syste-
men oft deutlich performanter als Abstraktionsverfeinerung ist.
Die Dissertation schließt mit einer Diskussion der wesentlichen Ergebnisse
des dritten Teils und einem Ausblick auf zukunftige¨ Forschungsaufgaben in
diesem Gebiet.Acknowledgments
I wrote the thesis at hand while I was a member of the research group on the
Foundations of Artificial Intelligence at Albert-Ludwigs-Universitat¨ Freiburg,
headed by Bernhard Nebel. It has been a long while from the very beginning of
my PhD studies to the completion of the thesis. During that period, many people
directly or indirectly contributed to it. Now, I would like to take the opportunity
to thank them.
First of all, I want to thank my adviser Bernhard Nebel. Bernhard gave me
the necessary freedom to pursue my own ideas. At the same time he gave me
valuable advice and pushed me at the right time to get this thesis finally done. I
am really thankful for that. Andreas Podelski served as the second reviewer for
this thesis. I not only want to thank Andreas for this service, but also for many
fruitful discussions and a successful collaboration.
Special thanks go to Jor¨ g Hoffmann. Especially in the beginning of my PhD
studies, Jor¨ g helped me a lot to gain ground in heuristic search. For me, working
with Jor¨ g was like learning from him. Many thanks for that. Special thanks
also go to Malte Helmert, for being a friend and an exceptional officemate.
Whenever I had a scientific question Malte almost always had a brilliant answer
to it. I thank Malte for the great time we had, too much coffee and listening
to Helge Schneider. And of course, special thanks also go to Martin Wehrle. I
want to thank Martin for an intensive and very productive collaboration and for
providing valuable feedback on several drafts of this thesis. I really enjoyed our
pair programming sessions in which we created MCTA. It was always fun to
work with Martin.
I also want to thank the German Research Foundation (DFG) that partly
supportedy this work as part of the Transregional Collaborative Research Cen-
ter “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14
AVACS, http://www.avacs.org/). The many inspiring discussions and collabora-
tions we had in the R3 subproject were a valuable contribution to this thesis.IV
In addition to Bernhard, Andreas, Jor¨ g, and Martin, I particularly want to thank
Henning Dierks, Klaus Drager¨ , Bernd Finkbeiner, and Jan-Georg Smaus. I also
want to thank Kim G. Larsen and Gerd Behrmann from Aalborg University.
Following my visit in Aalborg in 2004, they greatly supported me in getting
acquainted with the implementation aspect of model checking timed automata.
This thesis was proofread very carefully by different people over and over
again. I am very thankful to those who undertook this laborious task: Malte
Helmert, Robert Mattmuller¨ , Gabi Roger¨ , Jan-Georg Smaus, Martin Wehrle, and
¨Stefan Wolfl. I also want to thank all my former and current colleagues at the
research group on the Foundations of Artificial Intelligence. Thank you all for
the many helpful discussions we had, for the nice Oberseminars, and for playing
table soccer. It was always fun to work in such a pleasant working environment.
Last but definitely not least, I also want to thank my family and friends for
their moral support. My heartfelt thanks go to all of them. I especially want to
thank Birte Kruger¨ , Anne Bongers, Tobias Sing, Stefan Hugger, Malte Helmert
and my parents Angelika and Hans-Peter Kupferschmid.
Freiburg, November 2009 Sebastian KupferschmidContents
Part I Model Checking: Motivation, Temporal Logic, Methodology
1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.1 Real-time Systems, Verification and Heuristics . . . . . . . . . . . . . . . 4
1.2 An Illustrative Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1 Motivation, Goals and History. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.1 Kripke Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.2 A Branching Time Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.2.3 The Model Checking Problem . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Model Checking Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.1 Abstraction-based Methods . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.2 Symbolic Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.3 Bounded . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.3.4 Directed Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 20
Part II Real-time Systems
3 Model Checking for Real-time Systems . . . . . . . . . . . . . . . . . . . . . . . 23
3.1 Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.1.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.2 Timed Automata Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.3 The Region Automaton . . . . . . . . . . . .