RVS-Lehrveranstaltungen - Wintersemester 1998/1999

Spezifikation und Verifikation verteilter Systeme

Beleg-Nr.: 39 21 18
Treffen (neue Zeit!): Do, 10.00-12.00, D6-135

In den letzten 10 Jahren hat sich die alltägliche Welt verändert. Verschiedene Passagier-Flugzeuge fliegen und Autos bremsen nicht nur mit Hilfe, sondern unter völliger Kontrolle der Rechner. In einem Flugzeug gibt es viele verschiedene kommunizierende Prozessoren, die die verschiedenen Funktionen unterstützen. Solche Systeme werden verteilte Systeme genannt. Wie können wir sagen, wie ein solches System sich verhalten wird? Eine solche Beschreibung nennt man eine Spezifikation. Dazu, sei eine Spezifikation gegeben, sowie ein System-Design oder Code. Wie können wir sicher sein, dass dieses Design genau so funktioniert, wie die Spezifikation spezifiziert? Testen ist unmöglich denn es gibt zu viele Ablauf-Möglichkeiten. Es muss bewiesen werden. Dieses Vorgehen nannt man Verifizieren. Das Aufbauen eines formalen Beweises für einen Algorithmus für nebenläufige Systeme, ist von der Art her mehr Programmierung als reine Mathematik. Ich benutze das TLA-System von Leslie Lamport als Verifikations-Werkzeug. Wir werden auf den folgenden Beispiele konzentrieren:

ein formaler Beweis in TLA, der beweisst, dass ein Array ein abstrakten Buffer implementiert;
ein formaler Beweis eines Algorithmus: der Shared-Memory Lazy-Caching Algorithmus von Afek, Brown, Merritt.
ein Beweis im Aufbau: Verifikation des Radio-Link-Protokolls (einer Art von Sliding-Window-Protokoll)

Ausserdem werden wir die alltägliche Benutzung von formalen Methoden diskutieren (überwiegend: Spezifikation ohne genaue Verifikation), z.B.

eine Spezifikation in Engineering: ein Teil des Flight-Crew-Operating-Manuals für den Airbus A320 als TLA-Predicate-Action-Diagramme geschrieben;

Der Kurs enthält eine Einführung in die Logik und die Art und Weise, einen formalen Beweis mit der "hierarchischen Methode" von Lamport aufzubauen.

Theorie ist nutzlos ohne Praxis, sowie für das Verstehen in der Lehre als auch für die Informatik. Deswegen finden sich freitags die "normale" Vorlesungen statt. Donnerstags diskutieren wir in der Form eines Seminars oder eine Übungsgruppe, wie ein Beweis in TLA aufgebaut werden könnte. Als Beispiel nehmen wir eine vorläufige Version des RLP-Protokolls.

Wesentliche Literatur

Formal but Lively Buffers in TLA+, P. B. Ladkin
Analysis of a Technical Description of the Airbus A320 Braking System, P. B. Ladkin
Lazy Caching in TLA, P. Ladkin, L. Lamport, D. Roegel, B. Olivier
Lazy Cache Implements Complete Cache, P. Ladkin
Verschiedene TLA-Dokumente von der TLA Home Page

Das Y2K-Problem

Beleg-Nr.: 39 21 50
Treffen (neue Zeit!): Fr, 10.00-12.00, D6-135

Wegen der Jahrtausendwende wird ein "Sonder"-Problem auftreten - und in Sonderfälle ist es schon aufgetreten. Die Jahreszahl wird im Computer-Bereich oft mit zwei Buchstaben kodiert und wird sich beim Jahrtausendwechsel von "99" auf "00" ändern, welche als Nummer einen niedrigen Wert hat und nicht immer als Nachfolgewert erkannt wird. Solche Kodierungen gibt es nicht nur in datumsrelevanter Software sondern auch in allgemeiner Software sowie Firmware und Hardware. Das Problem, die möglichen Einzelfehler zu beheben, ist von der englischen Zeitschrift The Economist als das teuerste Technologie-Problem aller Zeiten bezeichnet worden. Es ist auch so, daß es nicht mehr genügend Zeit gibt, den bekannten Teil des Problems vor der Jahrtausendwende zu beheben. In vielen Fällen, die bereits untersucht worden sind, liegen die betroffenen Fehler tiefer als vorher gedacht. Was ist zu tun?

In diesem Seminar wird versucht, die Breite des Problems zu verstehen und abzuschätzen, sowie mögliche Maßnahmen zu diskutieren und zu entwickeln (es wird wahrscheinlich keine Lösung geben). Es ist für alle von Interesse, die die Absicht haben in der Industrie sowie der Wirtschaft oder im Business-Bereich in den nächsten zwei Jahren tätig zu sein.

WB-Graphen: Projekt-Seminar

Beleg-Nr.: 39 21 30
Beginn: Läuft schon n.V. Bitte bei Ladkins Sprechstunde anmelden

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

The WB-Analysis Home Page beinhaltet Verweise auf der wesentlichen Literatur.

Arbeitsgemeinschaft Rechnernetze und Verteilte Systeme

Beleg-Nr.: 39 21 42
Beginn: Läuft schon n.V. Bitte bei Ladkins Sprechstunde anmelden

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.