Technische Universität München, Fakultät für Informatik
Bereich: 3 SWS Vorlesung im Bereich Informatik III (Theoretische Informatik)
Termin: Do. 14.30-17.00, A 009, Beginn 25.4.02 Ort: Raum A 009, Augustenstraße 77, Rückgebäude, Erdgeschoß
Schein: durch Teilnahme an Semestralklausur
In der Vorlesung werden die Grundlagen der Temporalen Logik und die wichtigsten Verfahren des Model Checking von temporalen Eigenschaften behandelt. Model Checking ist eine automatisierbare Technik zur Verifikation des zeitlichen Verhaltens von Systemen (insbesondere reaktiven Systemen). Dieser Ansatz wurde bereits erfolgreich in der Praxis eingesetzt, z.B. um Fehler in komplexen industriellen Schaltungen, aber auch in Protokollen oder Controllern zu finden. Es ist zu erwarten, dass sich Model Checking als ein Standardverfahren im Design reaktiver Systeme etablieren wird, neben den klassischen Methoden zur Qualitätssicherung wie statische Analyse und Testen. In der Vorlesung werden sowohl die theoretischen Grundlagen ausführlich behandelt als auch die Verfahren auf exemplarische Problemstellungen angewandt.
1. Modellierung von temporalen Systemen
2. Aussagen- und Prädikatenlogik
3. Modale und Temporale Logiken
4. Computation Tree Logik
5. Lineare temporale Logik
6. Grundlegende Model Checking Verfahren
7. Symbolisches Model Checking
8. Binäre Entscheidungsdiagramme (BDDs)
9. Model Checking und Automatentheorie
10. Arbeiten mit partiellen Ordnungen
11. Äquivalenzen zwischen Modellen
12. Abstraktionen und Symmetrien
13. Kompositionale und modulare Verifikation
E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking, MIT Press, 1999.
E.M. Clarke, B.-H. Schlingloff, Model Checking, in Handbook of Automated
Reasoning, Band II, S. 1637--1790, Elsevier, 2001.
Weitere Literatur wird in der Vorlesung angegeben
Vorlesung 25.4.02
Vorlesung 2.5.02
Vorlesung 16.5.02
Vorlesung 23.5.02
Vorlesung 6.6.02
Vorlesung 13.6.02 ausgefallen
Vorlesung 20.6.02
Vorlesung 27.6.02
Vorlesung 4.7.02
Vorlesung 11.7.02
Vorlesung 18.7.02
Übungsblatt 1 Übungsblatt 2 Übungsblatt 3 Übungsblatt 4 Übungsblatt 5 Übungsblatt 6