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


Wahlpflicht-Praktikum im WS 2001/2002

Automatische Verifikation reaktiver Systeme

Allgemeine Informationen

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

Zeit: Montags 14.30-16.00 Uhr s.t., ab 15.10.2001
Raum: 2710 (Stammgelände)
Anmeldung: Die zentrale Einschreibung (Login: prakt) fand vom 19. bis 23. Juli 2001 statt.
Teilnehmerzahl: 30 Studierende.

Bereich: Informatik I (alte Prüfungsordnung) - Informatik III (neue Prüfungsordnung)
Voraussetzungen: Bestandenes Vordiplom. Ein Besuch der Veranstaltung ,,Nichtsequentielle Systeme und nebenläufige Prozesse'' wird vorausgesetzt.
Scheinerwerb:
Übungsaufgaben: Mindestens 60 Prozent der insgesamt erreichbaren Punkte;
Programmieraufgaben: lauffähige, korrekt arbeitende Implementierungen der Algorithmen.

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 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: 2001/06/15-15:03)