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

Allgemeine Informationen

Dozent: Prof. Dr. J. Esparza
Zeit: Dienstags, 9.00-11.00 st
Raum: 2205
Beginn: Mittwoch, 4. November 1998, 15.00 Uhr, Raum S-2229
Bereich: Informatik I (alte Prüfungsordnung) -- Informatik III (neue Prüfungsordnung)
Voraussetzungen: bestandenes Vordiplom; Besuch der Veranstaltungen Nichtsequentielle Systeme und nebenläufige Prozesse oder Petrinetze sehr empfehlenswert
Praktikumsleiter: Christine Röckl und Stefan Römer
Anmeldung: die zentrale Einschreibung findet wie üblich in der HP-Halle an den beiden ersten Semestertagen, dem 2. und 3. November, in der Informatik-Halle statt. Voraussichtlich ab 4. November 1998 hängt die Teilnehmerliste in der Informatikhalle aus bzw. wird in ,,tum.info.studium'' gepostet.
Scheinerwerb: 60 Prozent der Punkte beim 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 für den 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

Das Praktikum gliedert sich in zwei parallel laufende Teile:
Das Praktikum setzt keine speziellen Kenntnisse voraus; Programmiererfahrung in C und Interesse an CCS und/oder Petri-Netzen sind jedoch von Vorteil.

Durchführung

In jeder Praktikumswoche findet ein zweistündiges Treffen statt, bei dem Einführungen in die Themengebiete gegeben, sowie Aufgaben und Lösungen besprochen werden. Außerdem dienen die Treffen dazu, Fragen der Praktikumsteilnehmer(innen) zu beantworten.

Bei erfolgreicher Teilnahme wird ein unbenoteter Schein vergeben.

Übungsbetrieb


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

Javier Esparza, Tel. 289-22405, Stammgelände Raum 3169,
e-mail: esparza@in.tum.de

Christine Röckl, Tel. 289-28237, Stammgelände Raum 2205, e-mail: roeckl@in.tum.de

Stefan Römer, Tel. 289-22403, Stammgelände Raum 3167, e-mail: roemer@in.tum.de



Stefan Römer
Fri Jul 10 13:45:23 MET 1998