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:
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.
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.
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:
Das Y2K-Problem
Beleg-Nr.: 39 21 50
Treffen (neue Zeit!): Fr, 10.00-12.00, D6-135
WB-Graphen: Projekt-Seminar
Beleg-Nr.: 39 21 30
Beginn: Läuft schon n.V. Bitte bei Ladkins Sprechstunde anmelden
Literatur
Arbeitsgemeinschaft Rechnernetze und Verteilte Systeme
Beleg-Nr.: 39 21 42
Beginn: Läuft schon n.V. Bitte bei Ladkins Sprechstunde anmelden
Zurück zur ...
Startseite des kommentierten Vorlesungsverzeichnisses
Startseite der Gruppe RVS
P. B. Ladkin