RVS-Lehrveranstaltungen - Wintersemester 1999/2000

Grundlagen der System-Korrektheit und des -Versagens

Vorlesungs-Beleg-Nr.: 39 21 24
Seminars-Beleg-Nr.: 39 21 30
Vorlesungs--Beginn: 15.10.99
Seminar--Organisatorisches Treffen: 14.10.99 um 10.00
Beides im Seminarraum D6-135

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- und 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

The Success and Failure of Artifacts, a hypertextbook by Prof. Ladkin.

Safeware: System Safety and Computers, by Prof. Nancy Leveson, (Addison-Wesley 1995).

Computer-Related Risks by Dr. Peter Neumann, Moderator of the RISKS-Forum, (Addison-Wesley, 1995).

Formalising Failure Analysis [ Abstract | Paper ]
Thorsten Gerdsmeier, Peter Ladkin, Karsten Loer, 4 June 1997, Report RVS-Occ-97-06
Analysing the 1993 Warsaw Accident With a WB-Graph Draft Version Michael Höhl and Peter Ladkin, 12 June 1997.
A Tool For Building and Analysing WB-Graphs
Thorsten Gerdsmeier, 3 March 1997, Research Report RVS-RR-97-02
Recommended by Prof. D. Gibbon, Linguistik und Literaturwissenschaft, Uni Bielefeld.
Analysing the Cali Accident With a WB-Graph
Thorsten Gerdsmeier, Peter Ladkin and Karsten Loer
Second Version, 13 March 1997 (first version, 14 January 1997), Research Report RVS-RR-97-01
in Participant's Proceedings of the first Workshop on Human Error and Systems Development,
Technical Report GAAG TR-97-2, Glasgow Accident Analysis Group, University of Glasgow.
Computer-Related Incidents with Commercial Aircraft, ed. Peter Ladkin, a hypertext compendium of news and commentary on these issues.
News and Comment on the AeroPeru B757 Accident
Peter Ladkin
8 November 1996, Research Report RVS-RR-96-16
Explaining Failure with Tense Logic
Peter Ladkin
10 September 1996, Research Report RVS-RR-96-13
Formalism Helps in Describing Accidents
Peter Ladkin
4 September 1996, Research Report RVS-RR-96-12
The X-31 and A320 Warsaw Crashes: Whodunnit?
Peter Ladkin
Revised version 28 January 1996, Research Report RVS-RR-96-08

Why-Because-Analyse und Einzelprojekten: Projekt-Seminar

Beleg-Nr.: 39 21 32
Beginn: Organisatorisches Treffen Mittwoch 20.10.99 um 11.00 in D6-131

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

Why-Because Analysis: Formal Reasoning About Incidents, Buch (in PS/PDF-Form) von Peter Ladkin und Karsten Loer.
A Tool For Building and Analysing WB-Graphs
Thorsten Gerdsmeier, 3 March 1997, Research Report RVS-RR-97-02
Recommended by Prof. D. Gibbon, Linguistik und Literaturwissenschaft, Uni Bielefeld.

Arbeitsgemeinschaft Rechnernetze und Verteilte Systeme

Beleg-Nr.: 39 21 42
Beginn: Organisatorisches Treffen Mittwoch 20.10.97 um 11.00 in D6-131

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;
Weiterentwicklung der WBA;
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.