Vorlesungsankündigung
(Wintersemester 1998/99)
Verifikationsmethoden für
parallele Systeme
Für viele parallele Systeme, die in der Praxis eingesetzt werden,
wie z.B. Systeme zur Steuerung des Flugverkehrs oder Systeme, die im
Bankwesen oder bei der Raumfahrt eingesetzt werden, kann das
Auftreten eines Fehlers katastrophale Folgen haben.
Bedingt durch
die Größe der Systeme ist
es in vielen Fällen nicht möglich,
die Zuverlässigkeit des Systems von Hand nachweisen.
Ziel der Vorlesung ist es, Verifikations-Techniken
und zugehörige Spezifikations-Formalismen vorzustellen,
mit denen sich parallele Systeme automatisch
analysieren und verifizieren lassen.
Im ersten Teil der Vorlesung wird die Spezifikationssprache
$CCS$ eingeführt. Neben Techniken, die es
erleichtern, für eine gegebene $CCS$-Spezifikation eine
korrekte Implementierung zu entwerfen, werden
Verfahren vorgestellt, mit denen man für eine Implementierung
die Korrektheit bzgl. einer $CCS$-Spezifikation nachweisen kann.
Der zweite Teil wird sich mit temporaler Logik beschäftigen.
Termine:
Vorlesung:
Dienstag, 12-14 Uhr, V 302
Mittwoch, 16-18 Uhr, HS 9
Übung:
Mittwoch, 15-16 Uhr, C 01