Vorlesung Temporale Logik und Modelchecking

Organisatorisches

 

Temporale Logik und Modelchecking (3 VL,1 Ü) 

Wahlmodul ab 4. Semester           

      Vorlesung
        Montag       14-16, HS F         Wehrheim
        Donnerstag 14-15, HS F

      Übungen                        
        Donnerstag 15-16, HS F         Wehrheim

      Scheinerwerb
         DPO4: mündliche Prüfung
         DPO3: 50% der Übungsaufgaben, aktive Teilnahme an der Übung

Inhalt

In der Vorlesung wird eine bestimmte Klasse von Logiken, die sogenannten temporalen Logiken vorgestellt. Temporale Logiken erlauben es, zeitliche Aussagen über das Verhalten von Systemen zu formulieren. Sie werden deshalb oft zur Beschreibung von Systemanforderungen (erwünschten Eigenschaften) benutzt. Es existieren algorithmische Verfahren, die überprüfen, ob ein System eine durch eine temporallogische Formel beschriebene Eigenschaft erfüllt. Damit kann die Korrektheit von Systemen gegenüber bestimmten Eigenschaften nachgewiesen (verifiziert) werden. Eine solche Überprüfung bezeichnet man auch als Modelchecking. Sofern der Zustandsraum des Systems endlich ist, kann das Modelchecking vollautomatisch von einem Werkzeug (einem sogenannten Modelchecker) durchgeführt werden.

In der Vorlesung werden zwei temporale Logiken (LTL und CTL) sowie Modelchecking Algorithmen für sie vorgestellt. Die Möglichkeit des vollautomatischen Modelcheckings wird an Hand des LTL-Modelcheckers SPIN erläutert, mit dem (auch in den Hausübungen!) einige kleinere Beispiele (wie etwa verteilte Algorithmen, Protokolle) verifiziert werden.

Literatur

[1] E. Clarke, O. Grumberg, D. Peled: Model checking, MIT Press, 1999.

[2] Z. Manna and A. Pnueli: The temporal logic of reactive and concurrent systems - Safety, Springer, 1991.

[3] G.J. Holzmann: Design and Validation of Computer Protocols, Prentice Hall, 1990.

[4] G.J. Holzmann: The Spin Model Checker, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295. (gzipped postscript)

Ein großer Teil der Vorlesung wird [1] als Grundlage benutzen. Allerdings wird nicht genau die Reihenfolge von [1] eingehalten. [2] ist ein allgemeines Buch über temporale Logik. [4] beschreibt den Modelchecker, der in den Übungen benutzt werden soll. Zu Spin gibt es auch eine WWW-Seite, die viele Infos enthält (unter anderem auch weitere Literatur). [3] ist ein Buch allgemein über den Entwurf und die Validierung von Kommunikationsprotokollen. Darin wird auch Spin zur Verifikation eingesetzt.

Übungsaufgaben

Promela-Programme

Einige Beispielprogramme aus der Vorlesung:

Heike Wehrheim