Semantik und Verifikation verteilter Systeme [SVVS]

Aktuelles

Inhalt

Gegenstand dieser Vorlesung ist die formale Beschreibung und Analyse von reaktiven (d.h. nicht terminierenden, mit ihrer Umwelt kommunizierenden) Systemen, wie sie z.B. in Form von Betriebssystemen oder Kommunikationsprotokollen auftreten. Die Grundlage bildet die Prozeßalgebra CCS, deren Syntax und Semantik besprochen und an konkreten Beispielen erläutert wird. Anschließend werden Logiken vorgestellt, mit denen gewünschte Systemeigenschaften wie z.B. Deadlockfreiheit spezifiziert und für die jeweilige CCS-Prozeßbeschreibung überprüft werden können.

Zuordnung

Theoretische Informatik, Informatik Vertiefung

Voraussetzungen

Vordiplom in Informatik

Sonstiges

Die Veranstaltung gehöhrt zum Vertiefungsgebiet Theorie der Programmierung von Prof. Dr. K. Indermark.

Der Übungsbetrieb

Die Aufgabenblaetter werden jeweils Donnerstags in der Vorlesung ausgeteilt. Die bearbeiten Aufgaben werden eine Woche später zu Beginn der Donnerstagsvorlesung eingesammelt und am folgenden Montag in der Frontalübung vorgerechnet. Um den Uebungsschein zu erhalten muss man mindestens 50 % der Uebungspunkte erreichen und eine Klausur oder mündliche Prüfung am Ende des Semesters erfolgreich absolvieren.

In den Übungen dürfen sich Studenten zu einer Gruppe von maximal zwei Personen zusammenschliessen und gemeinsam Lösungen abgeben. Falls Programme/CCS-Spezifikationen zu erstellen sind, so sind diese als e-mail an den Übungsgruppenleiter zu senden. Zusaetzlich sind mit Kommentaren versehene Listings der Programme abzugeben.

Einige Aufgaben sind mit Hilfe des Verifikationstools Truth zu erstellen, daß hier am Lehrstuhl im Rahmen der Arbeitsgemeinschaft "Modellierung verteilter Systeme" ( MCS ) entwickelt wird. Es sind Versionen für Linux und Solaris kostenlos verfügbar und können hier heruntergeladen werden. Außerdem kann eine CD mit der erforderlichen Software zur Installation am Lehrstuhl geliehen werden. Weiterhin ist das System auch im CIP-Pool installiert. Eine Kurzanleitung ist hier zu finden. In der ersten Übung, die Ausnahmsweise in Raum 5054 stattfindet, wird das Verifikationstool vorgestellt. FAQs gibt es hier.

Die erste Übung findet am Montag, den 19.10.98, in Raum 5054 statt.
Ausgabe des ersten Übungblattes: Montag, 19.10.98
Abgabe des ersten Übungblattes: Donnerstag, 22.10.98

Die Aufgabenblätter

Die Folien

Rückfragen

Martin Leucker