Lehre der AG Rechnernetze und Verteilte Systeme im Wintersemester 1996-97

Die folgende Beschreibung ist noch nicht endgültig.. PBL 19.8.96

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

Dieses Seminar findet im Sommersemester 1997 statt.

Die folgende Beschreibung ist noch nicht endgültig.. PBL 19.8.96

Im diesen Semester sind alle eingeladen, die Interesse an Problemen mit der Spezifikation und Verifikation von Systemen haben. Wir diskutieren die verschiedenen Methoden um Systeme zu spezifizieren und die Möglichkeit, die Korrektheit dieser Systeme zu beweisen. Dazu diskutieren und probieren wir die Theorem-Provers Eves und PVS. Als Themen nehmen wir die Spezifikation des Radio-Link-Protokolls (ein Teil der TDMA-Technik für den Cellular-Telefon-Service) und den Beweis des Lazy-Caching-Algorithmus von Afek, Brown, Merritt.

Wir richten auch im RVS-Bereich unser eigenes Unix-Netz ein. Wir diskutieren im AG-Seminar auch die Organisation und die wesentlichen Software-Tools wie NFS- und sendmail-Configuration. Für Interessenten gibt es die Mölichkeit, nach einiger Zeit im RVS-Netz-Dienst mitzuarbeiten.

Das Seminar trägt der sprunghaft wachsenden Bedeutung des World Wide Webs und der damit einhergehenden Informationsinflation sorge. Neben einer kurzen Einführung in HTML, stehen Design- und Aufbauaspekte im Vordergrund. Dabei wird besonders auf die Informationsdarstellung wert gelegt werden. Dazu werden Techniken der Gestaltung in HTML 2.0, in den Netscape HTML Erweiterungen behandelt, aber auch neue Methoden durch HotJava und VRML (Virtual Reality Markup Language). Im Sommersemester 1996 worden z.B. Vorträge gehalten über

• die Mathematik des Hypertexts (Ladkin)
• Theorien der Funktionen der Sprache (Gibbon)
• Frames (Büschking)
• die Virtuelle Uni in VRML (Hartmeier, Krause, Jäger, Kazik) Anstatt einer Seminararbeit werden kleinere Projekte verteilt, die im Seminar vorgstellt und dann als HTML-Struktur niedergelegt werden.

Zurück zur ...