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


Wahlpflicht-Praktikum

Automatische Verifikation reaktiver Systeme

Dozent: Prof. Dr. J. Esparza
Zeit: steht noch nicht fest
Raum: steht noch nicht fest
Bereich: Informatik I (alte Prüfungsordnung) -- Informatik III (neue Prüfungsordnung)
Voraussetzungen: bestandenes Vordiplom; Besuch der Veranstaltungen Petrinetze oder Nichtsequentielle Systeme nebenläufiger Prozesse empfehlenswert
Praktikumsleiter: Stefan Römer
Anmeldung: die zentrale Einschreibung findet wie üblich in der HP-Halle an den beiden ersten Semestertagen, dem 4. und 5. November, in der Informatik-Halle statt. Voraussichtlich ab 7. Novemeber hängt die Teilnehmerliste in der Informatikhalle aus, bzw. wird gepostet.
Scheinerwerb: Lösen der Übungs- und Programmieraufgaben

Wichtig!
Das Praktikum Automatische Verifikation reaktiver Systeme zählt nach der alten Prüfungsordnung als Wahlpflichtpraktikum im Bereich Informatik I (Praktische Informatik), nach der neuen Prüfungsordnung (gültig ab November 1996) aber im Bereich Informatik III. Studenten, die nach der neuen Prüfungsordnung DHP machen, können den Schein wohl nicht als Praktikumsschein zu Informatik I verwenden!

Hintergrund

Unter einem reaktiven System versteht man ein System, das Rückwirkungen mit seiner Umgebung eingeht, mit dieser kommuniziert. Die Entwicklung von reaktiven Systemen gestaltet sich im allgemeinen recht schwierig, da für die Überprüfung der korrekten Funktionsweise (Verifikation) eine unüberblickbare Vielzahl möglicher Systemzustände in Betracht gezogen werden muß. Besonders schwierig ist dies bei verteilten reaktiven Systemen, also einer Ansammlung mehrerer parallel an einer Problemstellung arbeitender Komponenten, welche untereinander vernetzt sind und miteinander kooperieren (und konkurrieren). Die Verteiltheit bezieht sich dabei neben der eigentlichen Kontrolle der Verarbeitung auch auf die der Daten.
Die automatische Verifikation solcher Systeme beschäftigt sich mit der Frage, wie sich bestimmte/beliebige Aussagen (auf möglichst effiziente Weise) mit Hilfe eines Rechners überprüfen lassen. Dazu gehört das Testen von Sicherheits- (intuitiv: ,, nichts Schlechtes wird passieren``) und Lebendigkeitsaussagen (,, etwas Gutes wird eintreten``).
Eine Möglichkeit für die Untersuchung des Verhaltens reaktiver, verteilter Systeme mit endlichen Zustandsräumen ist es, die Menge der erreichbaren Zustände zu betrachten. Dazu muß der Zustandsraum auf geeignete Weise konstruiert werden; dieser kann sehr groß sein.

Inhalt

Auf semantischer Ebene beschränken wir uns in diesem Praktikum weitgehend auf Petri-Netze, da dieses Modell eine anschauliche Struktur besitzt und bereits entsprechende Programme vorhanden sind.
Im Praktikum soll ein Programm zur automatischen Verifikation von Systemeigenschaften, ein sogenannter Model Checker für 1-sichere Petri-Netze implementiert werden. Die Eigenschaften über dem System sind diejenigen, die sich in einer bestimmten Logik ausdrücken lassen. Wir werden die Logik CTL (Computational Tree Logic) benutzen, das ist eine einfache temporale Logik, bei der die Struktur der Zeit mit einem unendlichen Baum korrespondiert (sogenannte ,, branching time logic``).
Eine naheliegende Möglichkeit zur Realisierung eines solchen Model Checkers basiert auf der Konstruktion des zugehörigen Erreichbarkeitgraphen, der alle möglichen, vom Startzustand aus erreichbaren Systemzustände enthält. Auf dieser Struktur lassen sich dann einfach Verifikationen wie Fragen der Erreichbarkeit vornehmen.
Ausreichende Teilnehmerzahl vorausgesetzt, wird angestrebt, auch alternative Methoden zu implementieren, beispielsweise sogenannte Binary Decision Diagrams, kurz BDDs.
Es stehen eine Datenstruktur für Petri-Netze sowie eine einfache Funktionsbibliothek (in C) zur Verfügung, welche viele grundlegende Operationen auf Netzen bereitstellt, so daß diese Teile nicht selbst ausprogrammiert werden müssen.
Das Praktikum setzt keine speziellen Kenntnisse voraus; Programmiererfahrung in C und Interesse an Petri-Netzen sind jedoch von Vorteil.

Durchführung

In jeder Praktikumswoche findet ein zwei stüdiges Treffen statt, bei dem Einführungen in die Themengebiete gegeben sowie Aufgaben und Lösungen besprochen werden. Außerdem dient es dazu, Fragen der Praktikumsteilnehmer(inn)en zu beantworten.
Das Praktikum gliedert sich in zwei Teile:

Neben dem eigentlichen Programmcode wird auch eine (knappe) schriftliche Dokumentation (Ausarbeitung) erwartet.

Bei erfolgreicher Teilnahme wird ein unbenoteter Schein vergeben.

Für weitere Rückfragen stehen wir gern zur Verfügung.

Javier Esparza, Tel. 2892-2405, Stammgelände Raum 3169,
e-mail:  esparza@informatik.tu-muenchen.de

Stefan Römer, Tel. 2892-2403, Stammgelände Raum 3167, e-mail: roemer@informatik.tu-muenchen.de



Frank Wallner
Mon Aug 5 12:01:51 MET DST 1996