Model Checking

NUMMER:	150324
KÜRZEL:	ModChe
MODULBEAUFTRAGTE:R:	Prof. Dr. Thomas Zeume
DOZENT:IN:	Jun.-Prof. Thomas Zeume
FAKULTÄT:	Fakultät für Informatik
SPRACHE:	Deutsch
SWS:	4 SWS
CREDITS:	5 CP
ANGEBOTEN IM:	jedes Wintersemester

PRÜFUNGEN

FORM:	mündlich oder schriftlich
TERMIN:	Siehe Prüfungsamt.

LERNFORM

Vorlesung mit begleitenden Übungen

LERNZIELE

Die Studierenden lernen wie sich verteilte Systeme durch Transitionssysteme modellieren
und Eigenschaften in logischen Spezifikationssprachen wie LTL und CTL spezifizieren lassen.
Sie sollen elementare Algorithmen zur Überprüfung von Eigenschaften in Transitionssystemen
kennenlernen. Sie sollen ein Verständnis für die Möglichkeiten und Grenzen des Model
Checking entwickeln, und in die Lage versetzt werden, sich eigenständig mit fortgeschrittenen
Methoden des Model Checkings auseinanderzusetzen.

INHALT

Wie kann die Korrektheit von Software und Hardware formal überprüft werden? Im Model
Checking werden Software- und Hardware-Module durch Transitionssysteme formalisiert; gewünschte
Eigenschaften mit Hilfe logischer Formalismen formal beschrieben; und mit Hilfe
von Algorithmen automatisiert überprüft, ob ein Transitionssystem eine formal spezifizierte
Eigenschaft besitzt. In dieser Veranstaltung werden die theoretischen Grundlagen des Model
Checkings vermittelt, mit einem Fokus auf logik-basierten Spezifikationssprachen. Die Spezifikationssprachen
LTL und CTL werden eingeführt, ihre Ausdrucksstärke untersucht, und
die wichtigsten algorithmischen Ansätze für das Model Checking vorgestellt.

VORAUSSETZUNGEN CREDITS

Bestandene schriftliche oder mündliche Prüfung

EMPFOHLENE VORKENNTNISSE

∙ Grundlagenvorlesungen Mathematik,
∙ Einführung in die Theoretische Informatik (ggf. kann das nötige Wissen auch nachgeholt
werden),
∙ Hilfreich: Logik in der Informatik, Datenstrukturen und elementare Programmierkenntnisse

LITERATUR

Einstiegsliteratur für diese Veranstaltung sind die Bücher:
∙ Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
∙ Clarke Jr, E. M., Grumberg, O., Kroening, D., Peled, D., und Veith, H. Model checking.
MIT press.2018.

AKTUELLE INFORMATIONEN

Nicht im WS22/23! Ab SS23 im Sommersemester!