Klaus Varrentrapp
Unter Model Checking versteht man eine automatisierbare
Technik zur Verifikation 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 konkrete Problemstellungen
angewandt.
1. Modellierung von Systemen
2. Aussagen- und Prädikatenlogik
3. Temporale Logiken
4. Grundlegende Model Checking-Algorithmen
5. Binäre Entscheidungsdiagramme (BDDs)
6. Symbolisches Model Checking
7. Model Checking in der Praxis
8. Model Checking und Automatentheorie
9. Transformationen in klassische Logik
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.
zurück zum Inhaltsverzeichnis dieser Seite
Vorlesung 25.10.01
Vorlesung 1.11.01
Vorlesung 8.11.01
Vorlesung 15.11.01
Vorlesung 22.11.01
Vorlesung
29.11.01
Vorlesung 6.12.01
Vorlesung 13.12.01
Vorlesung 20.12.01
Vorlesung 10.1.02
Vorlesung 17.1.02
Vorlesung 24.1.02
Vorlesung
31.1.02
Am 7.2.02 findet die Vorlesung nicht statt
Vorlesung 14.2.02