inf455 - Model Checking (Complete module description)

inf455 - Model Checking (Complete module description)

Original version English PDF Download
Module label Model Checking
Modulkürzel inf455
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Verwendbarkeit des Moduls
  • Master's Programme Computing Science (Master) > Theoretische Informatik
Zuständige Personen
  • Wehrheim, Heike (module responsibility)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Prerequisites

Useful previous knowledge: Logic
Skills to be acquired in this module

Model checking is a technique for the automatic verification of hardware and software systems. In the course, the students develop knowledge and skills in requirements specification via temporal logic and the automatic algorithmic checking of systems with respect to requirements.
Professional competence
The students:

  • name the operators in temporal logics and the differences between linear-time and branching-time logics, - specify requirements in LTL and CTL
  • translate LTL formulae to Büchi automata
  • construct BDDs for boolean functions
  • describe CTL formulae in fixpoint form
  • apply model checking algorithms to Kripke structures
  • know the expressivity of bisimulation


Methodogical competence
The students:

  • apply formal modelling techniques
  • prove properties of temporal logics
  • use model checking tools for the verification of systems


Social competence
The students:

  • work on tasks in groups and discuss solutions
  • develop system descriptions in groups and interpret results of tools


Self-competence
The students:

  • organize their own work for the course
Module contents
  • temporal logics LTL and CTL
  • Büchi automata
  • explicit model checking
  • Binary decision diagrams
  • Lattices, fixpoints, CTL as transformers
  • Symbolic 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
Language of instruction English
Duration (semesters) 1 Semester
Module frequency every summer term
Module capacity unlimited
Teaching/Learning method V + Ü
Previous knowledge Useful previous knowledge: Logic
Lehrveranstaltungsform Comment SWS Frequency Workload of compulsory attendance
Lecture 2 SoSe oder WiSe 28
Exercises 2 SoSe oder WiSe 28
Präsenzzeit Modul insgesamt 56 h
Examination Prüfungszeiten Type of examination
Final exam of module

Weekly homework assignments, lab assignments in a block, oral examination at the end

Portfolio