Einführung in die Grundlagen des Model Checking SS 09

Veranstaltungsnummer 042311 (BA-306)
Titel Einführung in die Grundlagen des Model Checking
Veranstalter Prof. Dr. Thomas Schwentick
Klassifikation Spezialvorlesung (DPO), Wahlmodul (BPO)
Semester Sommersemester 2009
SWS 3 (2V+1Ü)
Kreditpunkte 4,5 im Diplom, 4 nach BPO
Ort und Zeit

Vorlesung: Montag 16:15-18:00 Uhr, OH 16, Raum 205

Übung: Mittwoch, 10:15-11:45 Uhr, OH 14, Raum 205 (14-tägig)

Querverbindungen GTI, Logik, Software-Konstruktion
Voraussetzungen GTI-Stoff wird vorausgesetzt
Logik ist hilfreich, aber nicht unbedingt notwendig
Schwerpunktgebiete (DPO) 1 (Softwarekonstruktion)
4 (Algorithmen,...)
5 (Sicherheit und Verifikation)

Aktuelles

Die Vorlesung entfällt am 6.7.09. Ersatztermin (nicht prüfungsrelevant) am 27.7.09.

Die Vorlesungstermine bis zum Ende des Semesters:

Logbuch

Hier finden Sie Informationen zum Verlauf der Vorlesung

Übungsblätter

Hier finden Sie die Übungsblätter.

Inhalt

Der Bedarf an Verifikation (von Teilen) des Entwurfs von Computersystemen
und Software hat in den letzten Jahren stark zugenommen. Gleichzeitig
haben sich auch die Möglichkeiten hierzu durch größere Rechenkraft und,
vor allem, durch verbesserte Methoden deutlich verbessert.

Model Checking bezeichnet eine Methode zur automatischen Verifikation
des Entwurfs nebenläufiger Systeme mit (zunächst) endlich vielen Zu-
ständen. Sie hat sich innerhalb der letzten 20 Jahre von einem reinen
Forschungsobjekt zu einer in der Industrie verwendeten Standardmethode
entwickelt. Sie wird insbesondere zur Verifikation von Schaltungen und
Kommunikationsprotokollen eingesetzt.

Die Grundidee ist, das zu verifizierende System als endliches
Transitionssystem und die zu verifizierenden Eigen-
schaften als Formeln einer geeigneten Temporallogik darzustellen. Das eigent-
liche Model Checking überprüft dann, ob die Formel in dem Transitions-
system gilt. Die praktische Herausforderung besteht darin, dass die Anzahl der
Zustände der Systeme riesig werden kann.

Die Vorlesung stellt die theoretischen Grundlagen des Model Checking
vor. Sie soll einen Überblick über die wichtigsten Grund-
lagen geben.

Einzelne Themen:

  • Modellierung durch Transitionssysteme
  • Temporallogiken: LTL und CTL
  • Einfache Auswertungsverfahren
  • Kompakte Repräsentation Boolescher Funktionen: OBDDs
  • Symboliches Model Checking
  • Model Checking konkret: NuSMV
  • Automatenbasiertes Model Checking
  • Methoden zur Größenreduktion der zu testenden Systeme
  • Echtzeitsysteme: TLTL, Zeitautomaten und UPPAAL

Literatur

  • Baier, Katoen: Principles of Model Checking. MIT Press, 2008.
  • Clarke, Grumberg, Peled:Model Checking. MIT Press, 3. Auflage, 2001.
  • Berard, Bidoit, Finkel, Laroussine, Petit, Petrucci, Schnoebelen, McKenzie: Systems and Software Verification. Springer, 2001.
  • Huth, Ryan:Logic in Computer Science (Kapitel 3 und 6).Cambridge University Press. 2004.
  • McMillan:Symbolic Model Checking. Kluwer, 1993. Die zugrunde liegende Dissertation von McMillan ist hier erhältlich.

Weiterführende Literatur wird in der Vorlesung genannt.

Die Vorlesung wurde in ähnlicher Form im Sommersemester 2006 gelesen. Dazu gibt es ein Folienskript. Allerdings wird die Vorlesung gründlich überarbeitet werden. Die aktualisierten Folien werden hier fortlaufend eingestellt. Im Zweifelsfall sind die aktuellen Folien maßgeblich.