Formaler Entwurf Verteilter Systeme

Vorlesung im WT 2008:

Formaler Entwurf Verteilter Systeme: Methoden und Werkzeuge

 
Dozent:  Prof. Dr.-Ing. Markus Siegle

Zeit:  Donnerstag 08:00-09:30, erster Termin 10. Jan. 2008
Raum: 36/01241

Inhalt

Moderne Verteilte Systeme, wie z.B. Prozessüberwachungssysteme, verteilte Web-Server oder verteilte Datenbanken müssen hohe Anforderungen erfüllen. Ihr Verhalten muss zum einen funktional korrekt und vollständig sein, was z.B. bedeutet, dass auf eine bestimmte Eingabe mit der passenden Ausgabe reagiert wird, oder dass das System sich nicht verklemmt. Zum andern müssen solche Systeme meist strenge Anforderungen an ihr zeitliches Verhalten erfüllen. Z.B. kann gefordert werden, dass eine bestimmte Transaktion innerhalb einer vorgegebenen Zeitspanne abgeschlossen sein soll, oder dass die Wartezeit eines anfragenden Klienten einen bestimmten Höchstwert nicht oder nur in seltenen Ausnahmefällen überschreiten soll.
In dieser Lehrveranstaltung  werden formale Methoden vorgestellt, mit deren Hilfe die Struktur und das dynamische Verhalten von komplexen verteilten (oder allgemeiner ausgedrückt: nebenläufigen) Systemen spezifiziert werden kann. Wir behandeln insbesondere die beiden Spezifikationsformalismen Petrinetze und Prozessalgebren, und diskutieren ihre mathematischen Eigenschaften und die darauf aufbauenden Analyseverfahren.
Weiterhin behandeln wir die Frage nach der Formalisierung von Anforderungen an ein solches verteiltes System. Wir werden sehen, dass temporale Logiken hierfür ein wertvolles Hilfsmittel darstellen. Es wird gezeigt, wie man mit der Methode des sog. Model Checking komplexe Anforderungen, die mit Hilfe einer temporalen Logik formuliert wurden, automatisch überprüfen kann. Neben den Verifikationsalgorithmen für die weit verbreitete Logik CTL werden Erweiterungen in Richtung von Realzeiteigenschaften angesprochen.
In den Übungen besteht auch Gelegenheit, Software-Werkzeuge kennenzulernen, die die in der Vorlesung behandelten Techniken realisieren.

 

Skript und Folien zur Vorlesung werden im Download-Bereich zur Verfügung gestellt.

Übungen:  (wöchentlich 45 min im Anschluss an die Vorlesung, Übungsleiter ist Johann Schuster
 

Literatur: siehe Angaben im Skript

Zusatzmaterial (CTL Fallstudie): http://www.ece.concordia.ca/~tahar/coen7501/notes/5-mc-case-01.06-4p.pdf