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 - Modellierung von Systemen, Eigenschaften von Systemen und deren Spezifikation und verschiedene Model-Checking Methoden.

Aktuelles

Zum Seminar

Zuordnung	Hauptstudium, Theoretische Informatik
Beginn	14.10.2008
Zeit	Di 11-13 Uhr
Ort	RUD 25, IV.113
Dozent	Daniela Weinberg
Studienpunkte	3

Vorträge

Anforderung an den Vortrag

• das Thema möglichst anhand von Beispielen veranschaulichen
• Zuhörer nicht mit Definitionen überschütten
• Formalismen, Definitionen in Maßen einsetzen
• ggf. (interessante) Tools vorstellen

Anforderung an den Vortragenden

• Ausarbeitung eines Themas
• selbständige Literaturrecherche
• Vortrag halten, mindestens 60 min

Termine

	Termin	Thema	Vortragender	Folien
-1	14.10.2008	Einführung, Themenvergabe	Daniela Weinberg
0	21.10.2008
1	28.10.2008	Systeme, Petrinetze	Tanja Richter	Folien
2	04.11.2008	Automaten/ Kripkestrukturen, CTL, LTL	Daniela Weinberg	Folien
3	11.11.2008	Systemeigenschaften: Sicherheit, Lebendigkeit	Leonard Kausch	Folien
4	18.11.2008	Nebenläufigkeit/ Fairness	Jan Engelsberg	Folien
5	25.11.2008	Äquivalenzklassen: Traces, ..., Simulation, Bisimulation	Tim Johannes Hartmann	Folien
6	02.12.2008	ausgefallen
7	09.12.2008	LTL model-checking	Jan Birkholz	Folien
8	16.12.2008	CTL model-checking	Michael Berlin
	23.12.2008	Ferien
	30.12.2008	Ferien
9	06.01.2009	Symmetrien	Sebastian Debray
10	13.01.2009	Partial Order Reduction	Jingyang Yu
11	20.01.2009	BDD basiertes model-checking	Moritz Lemm
12	27.01.2009	SAT basiertes model-checking	Dorian Weber
13	03.02.2009	Timed Automata, TA model-checking	Sara Budde

Literatur

• siehe Themenliste unten

Bü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

1. Systeme

I. Was ist ein System? Systemgrößen, Zustand, Arten von Systemen

2. Modelle

I. Petrinetze

• Lectures on Petri Nets I: LNCS 1491
• Jensen: Coloured Petri nets (3 Bände)

II. Zustandsautomaten/ Kripke Strukturen

• Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.

3. Temporal Logic

I. 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

I. Sicherheit und Lebendigkeit

• Alpern, Schneider. Defining Liveness.
• E. Allen Emerson. Temporal and Modal Logic. Kapitel 7-7.1

II. 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

III. 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

I. LTL MC

• Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.

II. CTL MC

• Clarke, Grumberg, Peled: Model Checking. MIT Press, 3. Auflage, 2001.

III. Reduktionen

a. 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;

b. POR

• 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. Symbolic Model Checking

I. 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

II. 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

I. Modellierung

• B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.1-5.3

II. Timed Model-Checking

• B. Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools; Kapitel 5.4-5.5