Spezifikation und Verifikation verteilter Systeme

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)

• 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ä 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

Wegen der Jahrtausendwende wird ein Sonderproblem auftreten -- und in Sonderfälle ist schon aufgetreten. Die Jahreszahl ist oft im Computer-Bereich als zwei Buchstaben kodiert und wird sich von "99" auf "00" ändern, welche als Nummer einen niedrigen Wert hat und nicht immer als Nachfolgewert genommen wird. Solche Kodierungen sind nicht nur in Datumsbetroffene Software aber 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 Zeit bezeichnet worden. Es ist auch so, daß es nicht genügend Zeit mehr gibt, den bekannten Teil des Problems vor der Jahrtausendwende zu beheben, sowie daß in allen Fällen, die schon untersucht worden sind, liegen die betroffenen Fehler tiefer als vorher gedacht. Was zu tun?

In diesem Seminar wird versucht, die Breite des Problems zu verstehen und zu schätzen, und mögliche Massnahmen zu diskutieren und zu entwickeln (es wird wahrscheinlich keine Lösung geben). Es wüde alle interessieren, die Absicht haben, in der Industrie sowie der Wirtschaft oder Business-Bereich in den nächsten zwei Jahren einzusteigen.

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.

Zurück zur ...