NUMMER: | 150324 |
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 |
WORKLOAD: | |
ANGEBOTEN IM: | jedes Wintersemester |
BESTANDTEILE UND VERANSTALTUNGSART
Beginn: Donnerstag den 29.10.2020 Vorlesung Donnerstags: ab 10:00 bis 12.00 Uhr im Online Übung: siehe "Sonstiges"
LERNFORM
Wintersemester 2020/2021 Die Organisation und sämtliche Kursaktivitäten erfolgen über einen Moodle-Kurs. Moodle-Kurs: https://moodle.ruhr-uni-bochum.de/m/course/view.php?id=32921
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- 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
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