Seminar: Model-Checking
Wir studieren in diesem Seminar computergestützte Verfahren, mit denen überprüft werden kann, ob ein gegebenes Modell eines Systems eine gegebene Spezifikation erfüllt. Der Schwerpunkt liegt hierbei auf den Grundlagen moderner Model-Checking-Programme, der Modellierung von Systemen, Eigenschaften von Systemen und deren Spezifikation sowie verschiedene Model-Checking-Methoden.
Aktuelles
- Bitte Rücksprache zur Vortragsvorbereitung halten, Vorbereitung der Vorträge bis spätestens 29.1.2010
- Termin festgelegt und Themen verteilt,
- Themen und Literaturliste online gestellt
Zum Seminar
| Zuordnung | Hauptstudium, Theoretische Informatik |
|---|---|
| Einführung | Do. 15.10.2009 9-11 Uhr |
| Zeit | Blockseminar, 12. und 13. Februar 2010, 9:00 |
| Ort | RUD 26, 1'307 |
| Dozent | Dirk Fahland |
| Studienpunkte | 3 |
Vorträge
In diesem Seminar wollen wir einen umfassenden Überblick über Techniken zur automatisierten Verifikation von Systemen gewinnen. Wir gehen dabei zunächst auf die grundlegenden Konzepte der computergestützen Verifikation ein, beleuchten dann einige Probleme, die sich aus der Komplexität der Aufgabe ergeben und betrachten fortgeschrittene Verifikationstechniken.
Jede/r Seminar-Teilnehmer/in hält einen Vortrag von etwa 40min Dauer, leitet die zum Thema gehörige Diskussion und stellt, sofern vorhanden, interessante Tools zum Thema vor. Die Literatur soll selbständig recherchiert und die Vorträge sollen selbständig ausgearbeitet werden. Im Vortrag soll das Thema möglichst anhand von Beispielen veranschaulicht werden; Formalismen und Definitionen gehören hier nicht hin. Der Vortrag soll durch ein etwa 5-seitiges Handout unterstützt werden.
Wir werden die Themen der Vorträge (Liste siehe unten) bei der Einführungsveranstaltung verteilen und ein thematisch geschlossenes Seminar-Programm aufstellen. Während des Block-Seminars werden wir dann in kompakter Form von den Grundlagen bis zu Anwendungen und fortgeschrittenen Techniken einen umfassenden Überblick über die automatisierte Verifikation gewinnen.
Seminar-Programm
| Termin | Thema | Vortragender | Folien | |
| 0 | Do. 15.10. | Einführung und Themenvergabe | Dirk Fahland | Einführung Vortragstipps |
| 1 | Fr. 12.2. | Systeme und Petrinetze (1, 2.1) | Simon Heiden | |
| 2 | Automaten/Kripkestrukturen, LTL und CTL (2.2, 3.1) | Frank Habermann | ||
| 3 | Systemeigenschaften: Sicherheit und Lebendigkeit (4.1) | Pierre-André Kotulla | ||
| 4 | Nebenläufigkeit und Fairness (4.2, 4.3) | Daniel Ball | ||
| 5 | Verifikation verteilter Systeme (4.4) | Michael Fiedler | ||
| 6 | Äquivalenzklassen (5) | Kirill Yasinovskiy | ||
| 7 | Sa. 13.2. | LTL-Model-Checking (6.1) | Matthias Füssel | |
| 8 | CTL-Model-Checking (6.2) | Ouerghi Belhassen | ||
| 9 | Reduktion: Symmetrien (6.3) | David Pincus | ||
| 10 | Reduktion: Partial-Order Reduction (6.4) | Sebastian Schütze | ||
| 11 | BDD-basiertes Modelchecking (7.1) | Stephan Allner | ||
| 12 | SAT-basiertes Modelchecking (7.2) | David Asher | ||
| 13 | Timed Automata und Timed Modelchecking (8) | Zheng Wang |
Literatur
Ausgewählte Fachartikel und einzelne Kapitel sind in der Themenliste unten angeführt. Die Literaturliste ist nicht vollständig sondern bietet lediglich Einstiegspunkte in das Thema, eine weitergehende Recherche und Lektüre ist empfohlen. Einen Überblick über das Thema bieten die folgende Lehrbücher.
- B. Berard et al.: Systems and Software Verification - Model-Checking Techniques and Tools
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
- Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, MIT Press
Themen
Der Vortrag eines Themas, das nicht in dieser Liste enthalten ist, ist prinzipiell nicht ausgeschlossen, muss aber vorher abgeklärt werden.
1. Systeme
Was ist ein System? Systemgrößen, Zustand, Arten von Systemen
2. Modelle
2.1 Petrinetze
- Lectures on Petri Nets I: LNCS 1491
- Jensen: Coloured Petri nets (3 Bände)
2.2 Zustandsautomaten/ Kripke Strukturen
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
3. Temporale Logik
3.1 CTL, LTL
- Michael Huth and Mark Ryan. Logic in Computer Science. Kapitel 3.2-3.3, 3.8.2-3.8.3
- E. Allen Emerson. Temporal and Modal Logic. Kapitel 1-3
4. Eigenschaften von Systemen
4.1 Sicherheit und Lebendigkeit
- Alpern, Schneider. Defining Liveness.
- E. Allen Emerson. Temporal and Modal Logic. Kapitel 7-7.1
4.2 Nebenläufigkeit
- E. Allen Emerson. Temporal and Modal Logic. Kapitel 5.1-5.2, 5.4
- G.D. Plotkin, V.R. Pratt. Teams can see pomsets. http://boole.stanford.edu/abstracts.html
4.3 Verifikation verteilter Systeme
- E. Allen Emerson. Temporal and Modal Logic. Kapitel 7.2-7.4
5. Äquivalenzklassen
- R. J. van Glabbeek. The Linear Time - Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes. In: Handbook of Process Algebra. Elsevier. pp. 1-99. 2001. (oder online auf seiner homepage)
- Simulation/ Bisimulation: Robin Milner. "Communicating and Mobile Systems: the pi-calculus". Cambridge University Press. 1999.
6. Explizites Model-Checking
6.1 LTL-Model-Checking
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
6.2 CTL-Model-Checking
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
6.3 Reduktionen: Symmetrien
- Karsten Schmidt. How to calculate Symmetries of Petri nets, Acta Informatica 36, S. 545-590
- Karsten Schmidt. Integrating Low Level Symmetries into Reachability Analysis;
6.4 Reduktionen: Partial-Order-Reduction
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
- Valmari, Antti: State of the Art Report: Stubborn Sets. In: Petri Net Newsletter 46 (1994), S. 6-14
7. Symbolisches Model-Checking
7.1 BDD-basiertes CTL-Model-Checking
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.
- B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.1-5.3
7.2 SAT-basiertes Model-Checking
- Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu;
- Symbolic Model Checking without BDDs., TACAS 1999, S. 193-207
8. Timed Automata
8.1 Modellierung
- B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.1-5.3
8.2 Timed Model-Checking
- B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.4-5.5
9. Software-Model-Checking
9.1 Predicate Abstraction/Abstrakte Interpretation
- Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis. Springer (2005)
- Susanne Graf and Hassen Saidi. Construction of Abstract State Graphs with PVS. In: Computer Aided Verification 1997, Lecture Notes in Computer Science, Volume 1254, S. 72-83
10. Verteilte Systeme II
10.1 Unfoldings
- J. Esparza, S. Romer, and W. Vogler. An Improvement of McMillan's Unfolding Algorithm. In T. Margaria and B. Steffen, editors, Proc. of TACAS'96, Passau, LNCS 1055, S. 87-106, Springer, 1996.
- Esparza, J.: Model checking using net unfoldings. Sci. Comp. Program. 23(2-3): 151-195, 1994
10.2 Verifikation offener Systeme
- Orna Kupferman, Moshe Y. Vardi, Pierre Wolper, Module Checking, Information and Computation, Volume 164, Issue 2, 29 January 2001, S. 322-344
Theorie der Programmierung | Kontakt | zuletzt geändert am 17.11.2009 10:30