Praktikum Model Checking
Aktuelles
- 14.4.2008: Die Vorlesung entfällt dieses Semester vollständig, da Prof. Knapp eine Vertretungsprofessur der Universität Augsburg angenommen hat.
Inhalt
Unter Model Checking versteht man Verfahren zur automatischen Analyse
reaktiver Systeme wie etwa eingebettete Steuerungen
(z.B. Airbagauslösung im Auto) oder Kommunikations- und
kryptographische Protokolle.
Auf Grund der Vielzahl von möglichen Abläufen, die zu nicht oder
nur schwer reproduzierbaren Fehlersituationen führen ("race
conditions") ist die Entwicklung reaktiver Systeme traditionell sehr
fehleranfällig. Andererseits werden solche Systeme häufig als
Basiskomponenten in Umgebungen eingesetzt, bei denen Fehler teuer sind
oder sogar eine Gefährdung von Leib und Leben bedeuten können. Es
wurden daher verschiedene Techniken entwickelt, mit denen Modelle
reaktiver Systeme rechnergestützt auf kritische Eigenschaften
überprüft werden können. Dabei werden alle mölichen
Abläufe des Modells betrachtet, so dass eine weit bessere
Fehlerabdeckung erreicht werden kann als durch bloße Testläufe.
Model Checking wird mittlerweile in der Industrie (etwa bei Intel,
IBM, Siemens, AT&T und Motorola) produktiv eingesetzt und auch
weiterentwickelt. Auch im Fahrzeug- und Flugzeugbau, im Bereich
Consumer Electronics sowie allgemein bei Prozess-Steuerungen werden
derzeit Modelchecking-Verfahren erprobt und evaluiert. Bewerber mit
entsprechendem Hintergrund haben exzellente Chancen in den
betreffenden Entwicklungsabteilungen.
Das Praktikum gliedert sich in zwei Teile, die zeitlich parallel ablaufen:
Im ersten Teil lernen Sie, Model Checker zur Analyse von reaktiven
Systemen einzusetzen. Ihre Aufgabe wird es sein, verbal bzw. durch
Pseudo-Code beschriebene Systeme, u.a. Mutex-Algorithmen, einfache
Steuerungen, Schaltkreise und Protokolle so zu modellieren, dass
Aussagen über deren Korrektheit gemacht werden können. Dabei
werden sowohl Sicherheitseigenschaften (z.B. Deadlockfreiheit) als
auch Lebendigkeitseigenschaften (z.B. Aushungerungsfreiheit)
untersucht, die z.T. in temporaler Logik formuliert werden. Der
nötige Hintergrund in formalen Techniken (faire Transitionssysteme,
temporale Logik) wird im Praktikum vermittelt.
Im zweiten Teil sollen Sie einen Einblick in die zu Grunde liegenden
Algorithmen erhalten, indem Sie selbst schrittweise einen kleinen
Model Checker schreiben. Die dabei verwendeten Programmiertechniken
werden im Praktikum besprochen.
