Stud.IP Uni Oldenburg
Universität Oldenburg
04.12.2021 03:37:00
inf455 - Model Checking (Vollständige Modulbeschreibung)
Originalfassung Englisch PDF Download
Modulbezeichnung Model Checking
Modulkürzel inf455
Kreditpunkte 6.0 KP
Workload 180 h
Einrichtungsverzeichnis Department für Informatik
Verwendbarkeit des Moduls
  • Master Informatik (Master) > Theoretische Informatik
Zuständige Personen
Wehrheim, Heike (Modulverantwortung)
Lehrenden, Die im Modul (Modulverantwortung)
Teilnahmevoraussetzungen
Kompetenzziele
Model Checking ist eine Technik der automatischen Verifikation für Hardware und Software Systeme. Die Studierenden erhalten in der Vorlesung Kenntnisse und Fähigkeiten in der Anforderungsspezifikation mittels temporaler Logik und der automatischen Überprüfung des Systems bezüglich der Anforderungen durch algorithmische Verfahren.

**Fachkompetenzen**
Die Studierenden:
- benennen die Operatoren in temporalen Logiken und die Unterschiede zwischen linear-temporalen und branching-time Logiken, 
- spezifizieren Anforderungen in LTL und CTL,
- übersetzen LTL-Formeln in Büchi-Automaten,
- konstruieren BDDs für boole‘sche Funktionen,
- können CTL Formeln in Fixpunktform darstellen,
- wenden Modelchecking Algorithmen auf Kripkestrukturen an,
- kennen die Unterscheidungskraft von Bisimulation

**Methodenkompetenzen**
Die Studierende:
- wenden formale Modellierung an,
- beweisen Eigenschaften von temporalen Logiken,
wenden Modelchecking Werkzeuge zur Verifikation von Systemen an.  

**Sozialkompetenzen**
Die Studierenden:
- bearbeiten in Gruppen Übungsaufgaben, diskutieren Ergebnisse,
- entwickeln gemeinsam Beschreibungen von Systemen und interpretieren die Resultate von Werkzeugen

**Selbstkompetenzen**
Die Studierenden:
- organisieren sich selber bei der Arbeit an den Aufgabenstellungen des Moduls.
Modulinhalte
- Temporale Logiken LTL und CTL
-
Büchi Automate
-
Explizites Model Checking
- B
inary decision diagrams
- V
erbände, Fixpunkte, CTL als Transformer,  

- Symbolisches Model Checking
- Bisimulation

Literaturempfehlungen

Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press

E. M. Clarke, Orna Grumberg, Doron Peled: Model Checking, MIT Press
Links
Unterrichtsprachen Deutsch, Englisch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul
Aufnahmekapazität Modul unbegrenzt
Hinweise
Nützliche Vorkenntnisse: Logik
Modullevel / module level MM (Mastermodul / Master module)
Modulart / typ of module Wahlpflicht / Elective
Lehr-/Lernform / Teaching/Learning method
Vorkenntnisse / Previous knowledge
Lehrveranstaltungsform Kommentar SWS Angebotsrhythmus Workload Präsenz
Vorlesung
2 SoSe oder WiSe 28
Übung
2 SoSe oder WiSe 28
Präsenzzeit Modul insgesamt 56 h
Prüfung Prüfungszeiten Prüfungsform
Gesamtmodul
Wöchentliche Übungsaufgaben, Praktikumsaufgaben im Block, mündliche Prüfung am Ende   
Portfolio