Veranstaltungsnummer 042311 (INF-BSC-306)
Titel Einführung in die Grundlagen des Model Checking
Veranstalter This email address is being protected from spambots. You need JavaScript enabled to view it.
Klassifikation Wahlmodul (BPO)
Semester Wintersemester 2019/20
SWS 3 (2V+1Ü)
Kreditpunkte 4 nach BPO
Ort und Zeit

Vorlesung: Dienstag 14:15-16:00 Uhr, OH 12, Raum 1.055
Beginn: 8.10.

Übung: Mittwoch, 10:15-12:00 Uhr, OH 12, Raum 1.055 (14-tägig)
Beginn: tba

Querverbindungen GTI, Logik, Software-Konstruktion
Voraussetzungen GTI-Stoff wird vorausgesetzt
Logik ist hilfreich, aber nicht unbedingt notwendig
 Materialien  im Moodle-Arbeitsraum

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Wie lässt sich die Korrektheit von Software und Hardware formal  überprüfen? In dieser Veranstaltung betrachten wir

  • wie sich Systeme durch Transitionssysteme formalisieren lassen,
  • wie Eigenschaften von Systemen mit Hilfe logischer Formalismen formal beschrieben werden können, und
  • wie automatisiert überprüft werden kann, ob ein Transitionssystem eine formal spezifizierte Eigenschaft besitzt.

Schwerpunkt der Veranstaltung sind die theoretischen Grundlagen des Model Checking für lineare und verzweigende Zeit. Zur Spezifikation von Eigenschaften werden die Logiken LTL und CTL verwendet. Ihre grundlegenden Eigenschaften aus Sicht der Logik und Komplexitätstheorie sowie Zusammenhänge zur Spieltheorie werden dargestellt. Die wichtigsten algorithmischen Ansätze für das Model Checking sowie Techniken zur Größenreduktion von Transitionssystemen werden vorgestellt.

Grundlage dieser Veranstaltung ist das Buch:

  • Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.