[Technical Faculty]

Verifikation nebenläufiger Programme und ihre Werkzeugunterstützung (080207)
Vorlesung im Sommersemester 2004

Termin Vorlesung: Montag und Mittwoch, 08:15-09:45, LMS2 - R. Ü1
Termin Übung: Mittwoch, 12:15-13:45, LMS2 - R. Ü2
Beginn: 14. April 2004
Dozent: Willem-Paul de Roever
Übungsbetreuung: Harald Fecher, Ben Lukoschus, Immo Grabe

Die vollständigen studientechnischen Daten sind über das Univis-System zu erfragen.



Nachweislich korrekte Programme sind ein Ziel, das öfter gewünscht oder gefordert als erreicht wird. Der Anwendung formaler Methoden bei der Programmentwicklung, so wünschenswert oder gar notwendig sie erscheint, steht der oft immense Aufwand entgegen, formale Beweise durchzuführen.

Modelchecking ist eine Technik zur Verifikation von endlichen und zunehmend auch unendlichen Systemen. Im Gegensatz zu Theorembeweisern oder gar ``Papier-und-Bleistift-Verifikationen'' zielen sie auf eine automatische Überprüfung von Eigenschaften eines Systems. Dies erklärt die zunehmende Akzeptanz von Modelcheckern in der Industrie. In bestimmten Bereichen, speziell bei der Hardwareverifikation und dem Chipentwurf, wird Modelchecking mittlerweile routinemäßig als Teil des Entwurfszyklus eingesetzt. Als Disziplin verbindet es die Gebiete der mathematischen Logik mit algorithmischen Fragen nach effizienten Suchstrategien, adäquater Maschinenrepräsentierung und anderem mehr.

Ziel der Vorlesung ist es, in die Prinzipien der automatischen Beweiswerkzeuge und ihre algorithmischen Umsetzungen einzuführen sowie einen Einblick in den aktuellen Stand moderner Werkzeuge auf dem Gebiet zu geben. Ein Schwerpunkt der begleitenden Übungen wird demzufolge auch der Umgang mit verschiedenen Beweiswerkzeugen sein.

Zwei Schwerpunkte der Veranstaltung bilden zum einen Bücher und Material zu temporalen Logiken von Amir Pnueli [7] [8]. Zum anderen Leslie Lamports TLA (``temporal logic of actions'') und der zugehörige TLC Modelchecker [6]. Punkte, die in der Vorlesung behandelt werden, sind

Materialien

Die Vorlesung basiert auf:

Folien

Übungsaufgaben

Tools

Links

References

[1]
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

[2]
D. Déharbe. A tutorial introduction to symbolic model checking. In R. J. G. B. de Queiroz, editor, Logic for Concurrency and Synchronization, Trends in Logic -- Studia Logica Library, pages 215--239. Kluwer Academic Publishers, 2003.

[3]
K. Engelhardt and W.-P. de Roever. Towards a practitioners' approach to Abadi and Lamport's method. Formal Aspects of Computing, 7:550--575, 1995.

[4]
G. J. Holzmann. The Spin Model Checker. Addison-Wesley, 2003.

[5]
M. R. A. Huth and M. D. Ryan. Logic in Computer Science: Modelling and Reasining about Systems. Cambridge University Press, 2000.

[6]
L. Lamport. Specifying Systems. The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.

[7]
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.

[8]
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer-Verlag, 1995.

Maintained by: Ben Lukoschus  (bls@informatik.uni-kiel.de) and Harald Fecher  (hf@informatik.uni-kiel.de)


Pages last (re-)generated June 28, 2004
This document was translated from LATEX by HEVEA.