RVS-Lehrveranstaltungen, Wintersemester 1999-2000

Grundlagen der System-Korrektheit und des ~-Versagens

Ein System ist ein Artefakt, deswegen hat es Ziele. Um diese Ziele zu erreichen, muß es ein vernünftiges Design geben und dieses Design implementiert werden. Also hat ein System mindestens diese drei Teile: Ziel, Design (-Spezifikation) und physikalische Realisierung. Normalerweise hat man einen vierten: eine Ziel-Ausschreibung (die sogenannte Anforderungs-Spezifikation) und oft bleibt das Ziel unspezifisch. Wie können wir sicher sein, daß das System genau tut, was wir vorhaben? Was für Fehlermöglichkeiten gibt es? Die Fehleranalyse ist ein wichtiger Teil des Ingenieurwesens. Fehler bei rein stofflichen Artefakten wie Brücken zeigen Zustandsänderungen: irgendetwas bricht zusammen. Bei dynamischen Systemen, wie von Computern unterstützte, gibt es Verhaltens-Fehler, ohne das etwas zusammenbricht. Diese Art Fehler führt oft zu Beschreibungs- und Analyse-Schwierigkeiten. Wir werden sehen, wie sich mit Hilfe der WB-Graph-Methode die Geschichte der Ereignisse eines fehlerhaften Verhaltens rekonstruieren lassen kann.

Am interessantesten sind die Systeme, die nicht nur einen physikalischen Teil haben, sondern auch einen `menschlichen' Teil, wie z.B. Flugzeuge. Flugzeug Vor- un Unfälle sind gründlich untersucht und sorgfältig dokumentiert. Im Seminar berichten wir über Vor- und Unfälle von Flugzeugen und anderen Systemen. Das Projekt-Seminar (siehe unten) wird die neue Why-Because-Analyse auf Unfallberichte anwenden.

Die Veranstaltung ist in zwei Teile geteilt, um so Zuhörer die Vorlesungen teilnehmen können, ohne das sie auch Hausarbeit im Seminar-Bereich machen müssen. Teilnehmer mit Lust auf Hausarbeit die auch zum Spitzenforschung gehört sind auf dem Projekt-Seminar Why-Because-Analyse hingewiesen.

Literatur

Wir werden die WB-Graph Methode für Analyse von Vor- und Unfall-Berichten anwenden. Die WB-Graph-Methode ist eine Entwicklung von Prof. Ladkin, um Kausal-Faktoren in Unfälle genau anzugeben und zu analysieren. Wir werden neue Beispiele bearbeiten und Unterstützung-Tools entwickeln.

Literatur

In diesem Semester werden wir u.a. Vorträge von DiplomandInnen in RVS zuhören: Karsten Loer (WB-Analyse vom Unfall in Nagoya), Hagen Barth (DiDoLog, ein System fü automatisches Einrichten von Handbücher von Endliche-Zustands-Beschreibungen); Thorsten Gerdsmeier (Semantik Definition der Programmiersprache DATR und deren Implementation als Virtuelle-Keller-Maschine, in Action Semantics, Natural Semantics und TLA+). Alle sind eingeladen, die Interesse an Problemen mit der Spezifikation, Verifikation und Analyse von Systemen haben. Themen sind:

• Methoden um Systeme zu spezifizieren;
• Beweise der Korrektheit dieser Systeme;
• Unterstützung der Beweise mit Hilfe der Theorem-Provers Eves und PVS;
• Beispiele wie das Radio-Link-Protokoll RLP1 und der Lazy-Caching-Algorithmus von Afek, Brown, Merritt;
• Praktische UNIX-System- und WWW-Server-Verwaltung;
• Weiterentwicklung der Tools fü WB-Graphen, für die, die Interesse in den Themen des Projekt Seminars haben, allerdings nicht im Projekt-Seminar teilnehmen können.