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


Wahlpflicht-Praktikum im WS 2003/2004

Automatische Verifikation reaktiver Systeme

Allgemeine Informationen

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

Zeit: Montags 14.00-15.30 Uhr s.t., ab 20.10.2003
Raum: MI-03.09.014
Übungsbetrieb: hier entlang.
Anmeldung: Bitte per E-mail bei mir melden!

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 (bei Master-Studierenden benoteter) 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-17200, Raum 03.11.060



Stefan Römer (Last modification: 2003/06/18-11:43)