Vorlesung (Hauptstudium)
Model Checking
Prof. Dr. Christel Baier
In unserem Alltagsleben werden wir in zunehmendem Maße mit moderner Informationstechnologie (PCs, Internet, Mobiltelefone, Türschließmechanismus von ICE-Toiletten, etc.) konfrontiert und geraten damit immer mehr in Abhängigkeit von deren Zuverlässigkeit. In vielen Fällen (sog. sicherheitskritische Systeme) kann das Auftreten von Fehlern fatale Folgen haben. Beispielsweise wird der durch den Fehler im Pentium Dividierer entstandene finanzielle Verlust auf 500 Mio. Dollar geschätzt; während die Funktionstüchtigkeit von in der Intensivmedizin eingesetzten Computersystemen lebensrettend sein kann.
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 Entwicklungsprozessen integriert.
Die Vorlesung beschäftigt sich mit dem Entwurf und der vollautomatischen Verifikation paralleler Systeme. Schwerpunktmäßig werden die Modellierung paralleler Systeme und die temporalen Logiken CTL, LTL, TCTL als Beschreibungsformalismen sowie zugehörige Model Checking Algorithmen behandelt.
| Zeit, Ort | Mi, Fr 9-11, HS 1 |
| Semesterwochenstunden | 4V + 2Ü |
| Übungen | n.Vereinb. (Prof. Dr. Christel Baier) |
| Voraussetzungen | Vordiplom | | Nachfolgeveranstaltungen | Seminar (Hauptstudium) im Sommersemester 2005 |
| Bereich (alte DPO) | A,C |
| Bereich (neue DPO) | A2 |
| Prüfungsmöglichkeiten | A oder C (nach Absprache, alte DPO), Modul A2 bzw A (neue DPO) |
| Informationen im WWW | http://web.informatik.uni-bonn.de/I/Lehre/Vorlesungen/VPS-0405 |
|
Übersicht: alle Semester
Reale und robuste Implementierung geometrischer Algorithmen
Einführung in die Computer Graphik