Model-Checking SS 2008

Neuigkeiten | Termine | Inhalt | Übungen | Folien | Links

Model-Checking (zu deutsch auch: Modellprüfung) ist eine Technik für die automatische Verifikation von Hardware- und Softwaresystemen. Gegeben ein solches System und eine Korrektheits-Spezifikation, prüft ein Model-Checker, ob das System korrekt arbeitet.

Model-Checking wird seit Mitte der 80er Jahre benutzt und hat seitdem enorme Fortschritte erzielt, insbesondere im Hardware-Bereich. Heuzutage haben alle wichtigen Hardwarehersteller Model-Checking-Gruppen, die Software-Werkzeuge entwickeln und für die Verifikation von großen Schaltkreisen anwenden. Letztes Jahr wurde den Erfindern des Model-Checking der Turing-Award verliehen.

In der Vorlesung werden die Grundlagen von Model-Checking behandelt. Es wird erklärt, wie Systeme modelliert werden, und wie man Korrektheits-Spezifikationen mit Hilfe temporaler Logiken ausdrücken kann. Es werden dann die Algorithmen beschrieben, die automatisch testen, ob das Modell die in temporaler Logik formulierten Eigenschaften besitzt. In der Vorlesung werden auch einige weit verbreitete Tools vorgestellt wie z.B. Spin und SMV. Als Zuhörer werden Sie Gelegenheit haben, diese Werkzeuge auszuprobieren.

Im Wintersemester findet eine weiterführende Vorlesung mit dem Titel Model-Checking II statt, die von Herrn Esparza gehalten wird.

Für das Verständnis der Vorlesung werden lediglich einige allgemeine Kenntnisse aus dem Grundstudium vorausgesetzt.

Literatur:

Die Vorlesung orientiert sich nicht an einem bestimmten Buch. Zum tieferen Verständnis können jedoch z.B. folgende Werke dienen:

• Clarke, Grumberg, Peled: Model Checking, MIT Press, 1999
• Emerson: Temporal and Modal Logic, Kapitel 16 in "Handbook of Theoretical Computer Science", vol. B, Elsevier, 1991
• Holzmann: The SPIN Model Checker, Addison-Wesley, 2003

Die in der Vorlesung verwendeten Folien werden hier zu finden sein.