course: Model Checking

number:
150324
teaching methods:
lecture with tutorials
media:
Moodle
responsible person:
Prof. Dr. Thomas Zeume
lecturer:
Prof. Dr. Thomas Zeume (Mathematik)
language:
german
HWS:
4
CP:
5
offered in:
winter term

dates in winter term

  • start: Thursday the 14.10.2021
  • lecture Thursdays: from 10:00 to 12.00 o'clock in IA 1/177
  • tutorial: siehe "Sonstiges"

Exam

Date according to prior agreement with lecturer.

Form of exam:oral
Registration for exam:FlexNow
Duration:30min

goals

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.

content

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.

requirements

  • 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

recommended knowledge

Keine

literature

  1. Clarke, Edmund M., Grumberg, Orna, Kroening, Daniel, Peled, Doron, Veith, Helmut "Model Checking", MIT Press, 2018
  2. Baier, Christel, Katoen, Joost-Pieter "Principles of Model Checking", MIT Press, 2008

miscellaneous

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