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


Wahlpflicht-Praktikum im WS 2002/2003

Automatische Verifikation reaktiver Systeme

Allgemeine Informationen

Leitung: Prof. Dr. Dr. h.c. W. Brauer
Verantwortlicher Mitarbeiter: Stefan Römer

Zeit: Montags 14.00-16.00 Uhr, ab 14.10.2002
Raum: Achtung: ab sofort im Hörsaal 3 (00.06.011) !!!
Übungsbetrieb: hier entlang.
Anmeldung: Die zentrale Einschreibung (Login: prakt) findet vom 15. bis 18. Juli 2002 statt.
Teilnehmerzahl: 24 Studierende.

Bereich: Informatik III (Theoretische Informatik)
Voraussetzungen: Bestandenes Vordiplom. Ein Besuch der Veranstaltungen ,,Nichtsequentielle Systeme und nebenläufige Prozesse´´ und/oder ,,Petrinetze´´ ist sehr wünschenswert.
Scheinerwerb:
Übungsaufgaben: Mindestens 60 Prozent der insgesamt erreichbaren Punkte;
Programmieraufgaben: lauffähige, korrekt arbeitende Implementierungen der Algorithmen.

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 Informationen zu Aufgabenblättern, Werkzeugdokumentationen etc. hier entlang.

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


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



Stefan Römer (Last modification: 2002/07/03-09:49)