Modelchecking
Vorlesung und Übung, Bereich SWT, WS 2003/04
Diese Lehrveranstaltung ist für den zweiten und dritten
Studienabschnitt geeignet.
Vorlesung
Mo 14.15-15.45 Uhr, D1.303, Beginn: 13. Okt. 2003
Übung
Mo 16.00-17.30 Uhr, D1.303 (14-tägig)
Dozent
Ekkart Kindler
(mailto:kindler@uni-paderborn.de),
Raum E3.167
Voraussetzungen
Stoff des Informatik-Grundstudiums, insbes. Modellierung.
Hilfreich aber nicht notwendig sind Kenntnisse aus der Lehrveranstaltung
Semantik von Programmiersprachen.
Prüfung
Je nach Anzahl der Teilnehmer wird am Ende des Semesters eine
mündliche Prüfung oder eine Klausur durchgeführt (voraussichtlich eine
mündliche Prüfung).
Zusammenfassung
Unter Modelchecking versteht man ein Sammelsurium von Verfahren zur
automatischen Überprüfung der Korrektheit verteilter bzw. reaktiver
Systeme. Dabei werden die gewünschten Eigenschaften des Systems durch
verschiedene Varianten der Temporalen Logik spezifiziert.
Im wesentlichen gibt es zwei verschiedene Verfahren: Die eine Variante
analysiert systematisch den Zustandsgraphen des betrachteten Systems;
die andere Variante benutzt Automaten. Eine naive Umsetzung dieser Verfahren
führt jedoch nicht zu praktisch einsetzbaren Verfahren.
In den letzten Jahren wurden jedoch eine Reihe von pfiffigen Algorithmen
und Datenstrukturen entwickelt, die Modelchecking viel effizienter gemacht
haben, so daß Modelchecking heute immer mehr auch in der Industrie
eingesetzt wird. Insbesondere wird es in sicherheitskritischen Anwendungen
oder im Hardwareentwurf eingesetzt, um Fehler frühzeitig erkennen zu
können.
In der Veranstaltungen werden wir die grundlegenden Konzepte des
Modelcheckings sowie die Techniken, die das effiziente Modelchecking
ermöglichen, kennen lernen.
Themenübersicht
- Einführung, Motivation und Überblick
- Modellierung reaktiver Systeme
- Temporale Logik (CTL*, CTL und LTL)
- Algorithmen
- Ein Modelchecker
- Fairness
- Binäre Entscheidungsdiagramme (OBDDs)
- Symbolisches Modelchecking
- Gegenbeispiele und Zeugen
- Ein Anwendungsbeispiel
- Modelchecking mit Automaten
- Halbordnungsreduktion
- Ausblick und Überblick
Unterlagen
Unter http://www.uni-paderborn.de/cs/kindler/Lehre/WS03/MC/unterlagen.html werden alle Unterlagen zur Vorlesung bereitgestellt
(Vorlesungsfolien, Übungsblätter, Musterlösungen, ...).
Literaturauswahl
E. M. Clarke, O. Grumberg, D. A. Peled:
Model Checking.
MIT Press, 1999.
K. Schmidt:
Modelchecking.
Vorlesungsskript, HU Berlin.
M. R. A. Huth, M. D. Ryan:
Logic in Computer Science: Modelling and reasoning about systems.
Cambridge University Press, 2000.