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


Wahlpflicht-Praktikum im WS 2000/2001

Automatische Verifikation reaktiver Systeme

Allgemeine Informationen

Dozent: Prof. Dr. Javier Esparza
Übungsbetrieb: Stefan Römer, Claus Schröter

Zeit: Montags 15.30-17.00 Uhr
Raum: 2705 (Stammgelände)
Anmeldung: Die zentrale Einschreibung (Login: prakt) fand bereits vom 24. bis 26. Juli 2000 statt.
Teilnehmerzahl: maximal 20 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 - entweder in einem der letzten Semester, oder aber begleitend zu diesem Praktikum im WS 2000/2001; der entsprechende Übungsbetrieb wird mit dem Praktikum koordiniert, sodaß beide Veranstaltungen im Wintersemester 2000/2001 besucht werden können.
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.

Javier Esparza, E-mail: esparza@in.tum.de, Tel. 289-22405, Stammgelände Raum 3169
Stefan Römer,   E-mail: roemer@in.tum.de,   Tel. 289-22403, Stammgelände Raum 3167
Claus Schröter, E-mail: schroete@in.tum.de, Tel. 289-22403, Stammgelände Raum 3167



Stefan Römer (Last modification: 2000/06/29-10:49)