Dozent: Prof. J. Esparza
Übungen: Michael Luttenberger

Vertiefungslinie: Sichere und zuverlässige Softwaresysteme

Zeit und Ort:
Mo 15:45-17:15 im Raum 0.457
Übung Do 15:45-17:15 (14-tägig) im Raum 0.124
Übungstermine: 21.4. (Einführung in Spin), 28.4., 12.5., 2.6., 16.6., 30.6., 14.7.

Hörerkreis: Studierende im Hauptstudium

Empfehlenswert für:
Erweiterte Kenntnisse in den Gebieten Verifikation, Anwendungen der Automatentheorie, Logik

Inhalt:
Model-Checking ist eine Technik für die automatische Verifikation von Hardware- und Softwaresystemen. Seit den ersten Arbeiten, die Mitte der 80er Jahren diese Technik als eine theoretische Möglichkeit etablierten, ist der Fortschritt enorm gewesen, 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.

In der Vorlesung werden die Grundlagen von Model-Checking behandelt. Zuerst wird erklärt, wie Systeme modelliert werden. Anschliessend werden temporale Logiken eingeführt, die als Spezifikationssprachen dienen. Es werden dann die Algorithmen beschrieben, die automatisch testen, ob das Modell die in temporaler Logik formulierten Eigenschaften besitzt. In der Vorlesung wird auch der bei Bell Labs entwickelte und weit verbreitete Model-Checker Spin behandelt.

In der Vorlesung wird das Thema Model-Checking vertieft, welches bereits in Grundlagen der Softwarezuverlässigkeit im WS 2004/05 angesprochen wurde. Eine vorige Teilnahme an der Grundlagen-Vorlesung ist nützlich, wird jedoch nicht vorausgesetzt.

Aktuelle Version der Folien: 1 Folie pro Seite, 4 Folien pro Seite

Literatur:

• Clarke, Grumberg, Peled: Model Checking, MIT Press, 1999
• Peled: Software Reliability Methods, Springer, 2001
• Emerson: Temporal and Modal Logic, Kapitel 16 in "Handbook of Theoratical Computer Science", vol. B, Elsevier, 1991
• Vardi: An Automata-Theoretic Approach to Linear Temporal Logic, LNCS 1043, 1996

Tools:

• SPIN
  Für Spin werden unter Win32 noch folgende Programme u.U. benötigt:
  
  • cygwin + gcc
  • Tcl/Tk
  Kurze Installationsanleitung für Windows:
  • cygwin-Installer (setup.exe) starten und Standardauswahl+gcc-Pakete (unter Devel auswählen) herunterladen/installieren.
  • Den Pfad zum Verzeichnis [cygwin]\bin in die PATH-Variable eintragen.
  • Die Datei spin406.exe nach [cygwin]\bin entpacken und in spin.exe umbenennen.
  • Die Datei xspin402.tcl in ein beliebiges, leeres Verzeichnis kopieren.
  • ActiveTcl installieren.
  Unter Linux sollte es ausreichen, Spin zu kompilieren (make -f make_unix im src-Verzeichnis) und das erstellte Binary in ein beliebiges Verzeichnis im Suchpfad zu kopieren. Sollte Tcl/Tk nicht installiert sein, dann findet sich unter obigem Link ebenfalls eine Linux-Version.
  
  HINWEIS: Darauf achten, dass man genug Rechte beim Ausführen von Spin besitzt. Ansonsten KÖNNTE es zu ,,Anomalien'' kommen :).

Übungsblätter:

• Spin-TutoriaL: PDF, museum.pml
  Hier gibt's die Promela- und LTL-Dateien für die Spin-Einführung
  
• 1. Übungsblatt: [PDF], [PS]
• 2. Übungsblatt: [PDF], [PS]
• 3. Übungsblatt: [PDF], [PS]
  Lösungsvorschlag: [PDF]
• 4. Übungsblatt: [PDF], [PS]
  Lösungsvorschlag: [PDF]
• 5. Übungsblatt: [PDF], [PS]
• 6. Übungsblatt: [PDF], [PS] (korrigierte Version !)