Den meisten Systemen der Praxis liegt ein sehr großer oder gar unendlicher Zustandsraum zugrunde. Die Systemvalidierung (d.h. der Nachweis, daß das System die gewünschten funktionalen oder quantitativen Eigenschaften erfüllt) ist deshalb extrem schwierig; von hand so gut wie unmöglich. Stattdessen greift man auf Methoden zurück, die eine computer-unterstützte Systemanalyse ermöglichen. Model Checking ist eine vollautomatisierbare Validierungstechnik, die im Kontrast zu den traditionellen (manuellen) Korrektheitsbeweisen steht. Es hat sich insbesondere für die Verifikation von Schaltkreisen und Protokollen bewährt und ist heute in zahlreichen industriellen Entwicklungsprozesesen integriert.
Die Vorlesung beschäftigt sich mit dem Entwurf und der vollautomatischen Verifikation paralleler Systeme. Schwerpunktmäßig werden die Modellierung paralleler Systeme, CTL, LTL und TCTL als Beschreibungsformalismen sowie zugehörige Model Checking Algorithmen behandelt.
Termin und Ort:
| Mittwoch 11.15-13.00, HS C |
| Freitag 11.15-13.00, HS 1 |
Bereich: A und C
Übungen: Begleitend zur Vorlesung werden theoretische und praktische Übungen angeboten, die von Herrn Alexander Asteroth, Frank Ciesinski, Marcus Größer, Sascha Klüppelholz, Peter Orbanz und Jörn Ossowski durchgeführt werden. Die Teilnahme an den Übungen wird dringend empfohlen, da sich der Stoff nur so angemessen vertiefen läßt. Die theoretischen Übungen finden mittwochs entweder von 9-11 (N201) oder 13-15 (N327-Gruppe 1, HS1-Gruppe 2) statt. Die praktischen Übungen finden unregelmäßig freitags 13-15 in HS 1 statt.
Scheinerwerb: Den HörerInnen der Vorlesung wird die Möglichkeit zum Scheinerwerb gegeben. Der Schein ist zwar nicht prüfungsrelevant; jedoch werden bei der Vergabe von Seminar-, Praktikums- oder Diplomarbeitsplätzen u. Ä. Studierende, die einen Schein erlangt haben, bevorzugt berücksichtigt. Näheres hierzu wird in der Vorlesung bekanntgegeben.
Voraussetzungen: Vordiplom in Informatik
Nachfolge-/Begleitveranstaltungen: Für das SS 2002 ist eine Vorlesung über ``Binäre Entscheidungsgraphen'' geplant, die zahlreiche Bezüge zur Hardwareverifikation aufweist. Weiter werden ab SS 2002 Seminare, Praktika und/oder eine Projektgruppe zum Thema ``Model Checking'' angeboten werden.
Prüfungen: geeignet für Diplomprüfungen der Bereiche A oder C, nach Absprache.
Unterlagen: Skript, Übungsblätter und andere Informationen zur Vorlesung werden unter
zu finden sein.
Literatur: Siehe Skript.