NUMMER: | 211000 |
KÜRZEL: | ModCh |
MODULBEAUFTRAGTE:R: | Prof. Dr. Thomas Zeume |
DOZENT:IN: | Prof. Dr. Thomas Zeume |
FAKULTÄT: | Fakultät für Informatik |
SPRACHE: | Deutsch |
SWS: | 4 |
CREDITS: | 5 |
ANGEBOTEN IM: | jedes Sommersemester |
LERNZIELE
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. Diese Veranstaltung richtet sich an Studierende der Mathematik, Informatik und ITS.
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.
VORAUSSETZUNGEN CREDITS
Bestandene Modulabschlussprüfung
EMPFOHLENE VORKENNTNISSE
- Grundlagenvorlesungen Mathematik- Hilfreich: Logik in der Informatik, Datenstrukturen und elementare Programmierkenntnisse
LITERATUR
1. Clarke, Edmund M., Grumberg, Orna, Kroening, Daniel, Peled, Doron, Veith, Helmut "Model Checking", MIT Press, 20182. Baier, Christel, Katoen, Joost-Pieter "Principles of Model Checking", MIT Press, 2008