Fakultät für Informatik der Technischen Universität München,
Lehrstuhl für Theoretische Informatik und Grundlagen der KI


Hauptseminar im SS 2002

Model Checking

(Brauer, Csirik, Holzer, Kiehn, König, Römer, Rossmanith)




Die Übungsscheine können bei Frau Sterl (Raum 00.10.013) abgeholt werden.


Vorbesprechung: Donnerstag, den 31.01.2002, 14:00 Uhr, Raum S3224 (Südgelände)

Seminar-Termin: Dienstags 14:00-15:30 Uhr. Raum N0111.


Kontaktperson: Barbara König


Inhalt

Der Begriff Model Checking faßt automatische Verifikationsverfahren zusammen, bei denen die Übereinstimmung eines gegebenen Systems oder Programms mit einer Spezifikation überprüft wird. Die Spezifikation ist oft als logische Formel gegeben, beispielsweise als temporallogische Formel. Besonders interessant ist es, Model-Checking-Techniken auf verteilte und nebenläufige Systeme anzuwenden.

Als Beispiel betrachten wir folgendes System, das als Transitionssystem gegeben ist, und die Formeln

System
Der Zustand 5 erfüllt beispielsweise die Formeln F1 und F2, der Zustand 1 jedoch nur die Formel F2.

Wenn ein System durch ein überschaubares endliches Transitionssystem gegeben ist, dann kann direkt überprüft werden, ob die Spezifikation erfüllt ist. Im allgemeinen ergibt sich aus der Systembeschreibung jedoch ein extrem großes Transitionssystem, beispielsweise bei einer Menge von interagierenden Prozessen. Manchmal ist das Transitionssystem sogar unendlich groß und kann gar nicht endlich dargestellt und überprüft werden. In diesen Fällen verwendet man Model-Checking-Techniken, bei denen das Transitionssystem nicht vollständig erzeugt werden muß.

Model-Checking-Techniken sind in der Praxis sehr gut einsetzbar und haben inzwischen auch in der Industrie zahlreiche Anwendungen, z.B. im Bereich Chip-Design und Kommunikationsprotokolle. Auch die Software von Deich- und Schleusenprojekten in den Niederlanden wurde mit Model Checking verifiziert und dabei wurden auch mehrere Fehler ausgemerzt.

Ziel des Seminars ist es, die Grundlagen zu Model Checking zu vermitteln und verschiedene Techniken und ihre Anwendungen kennenzulernen.

Seminarablauf

Das Seminar basiert im wesentlichen auf einem Buch von Clarke, Grumberg und Peled mit dem Titel Model Checking.

Zu Beginn des Seminars werden in einem Vortrag von unserer Seite grundlegende Kenntnisse zu Model Checking, insbesondere in bezug auf temporale Logik, vermittelt. Hierzu erarbeiten sich die Teilnehmenden während der Semesterferien einen einführenden Text in dieses Gebiet. Die erste Seminarsitzung im Sommersemester dient der Besprechung dieses Textes.

Die darauf folgenden Sitzungen werden durch die Referate der Teilnehmenden, die jeweils eines der unten aufgeführten Referatthemen übernommen haben, gestaltet. Neben dem Referat ist eine ca. fünfseitige Ausarbeitung zu erstellen, die an sämtliche Seminarteilnehmende verteilt wird. Bei der Erarbeitung des Stoffes und der Konzeption des Vortrags steht eine/r der MitarbeiterInnen hilfreich zur Seite.

Vortragsthemen

Die den einzelnen Themen zugrundeliegende Literatur ist unten auf dieser Seite angegeben.

  Datum Thema Vortragende/r Betreuung
  1 16.4.2002 Einführung in Model Checking   -
  2 23.4.2002 Binary Decision Diagrams (BDDs) Kristofer Treutwein Peter Rossmanith
  3 30.4.2002 Symbolisches Model Checking Wolfgang Schwitzer Peter Rossmanith
  4 7.5.2002 Model Checking für den mu-Kalkül Christian Buttenberg Markus Holzer
  5 14.5.2002 Model Checking und Automatentheorie Sandra Auerhammer Markus Holzer
  6 28.5.2002 Partial Order Reduction Andreas Kollmer Barbara König
  7 4.6.2002 Entfaltungstechniken für Petri-Netze Visar Januzaj Stefan Römer
  8 11.6.2002 Abstraktion Benjamin Fingerle Barbara König
  9 18.6.2002 Symmetrie Yehua Zhang Astrid Kiehn
  10 2.7.2002 Software zum Model Checking (Demo) Stefan Unterhauser Stefan Römer
  11 12.7.2002 Systeme mit unendlich vielen Zuständen Jiming Yin Barbara König
  12 9.7.2002 Echtzeit-Systeme (diskrete Zeit) Alexander Troppmann Astrid Kiehn
  13 16.7.2002 Echtzeit-Systeme (kontinuierliche Zeit) Borislava Stoimenova Astrid Kiehn


Hinweise

Literatur

Software/Tools

(Thema 10)