inf455 - Model Checking (Complete module description)

inf455 - Model Checking (Complete module description)

Original version English PDF download
Module label Model Checking
Module code inf455
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
  • Master's Programme Computing Science (Master) > Theoretische Informatik
Responsible persons
  • Wehrheim, Heike (module responsibility)
  • Lehrenden, Die im Modul (authorised to take exams)
Prerequisites

Useful prerequisites:

set theory, propositional and predicate logic, finite automata
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
Recommended reading
  • 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+Ü
Type of course Comment SWS Frequency Workload of compulsory attendance
Lecture 2 SuSe or WiSe 28
Exercises 2 SuSe or WiSe 28
Total module attendance time 56 h
Examination Prüfungszeiten Type of examination
Final exam of module

at the end of the term

written or oral exam