Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Course INF-62-52-K-6

Verification of Reactive Systems (4V+2U, 8.0 LP)

Course Type

SWS Type Course Form CP (Effort) Presence-Time / Self-Study
- K Lecture with exercise classes (V/U) 8.0 CP 156 h
4 V Lecture 56 h
2 U Exercise class (in small groups) 28 h
(4V+2U) 8.0 CP 84 h 156 h

Basedata

SWS 4V+2U
CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in SuSe
Level [6] Master (General)
Language [EN] English
Lecturers
Area of study [INF-ES] Embedded Systems and Robotics
Livecycle-State [NORM] Active

Possible Study achievement

  • Verification of study performance: proof of successful participation in the exercise classes (ungraded)
  • Details of the examination (type, duration, criteria) will be announced at the beginning of the course.

Contents

  • propositional logic: syntax, semantics, normal forms, sequence calculus, SAT solver
  • binary decision diagrams: BDD algorithms, FDDs and ZDDs
  • Transition systems: simulation and bisimulation, symbolic representation
  • µ-calculus: syntax and semantics, global and local model checking
  • ω automata: Definition, automata/borel hierarchy, Boolean operations on automata, transformation of acceptance conditions, determinization
  • temporal logics: LTL, CTL, CTL*, reduction to µ-calculus and ω automata
  • monadic predicate logics: S1S and LO2 (theory of linear orders 2nd stage), equivalence to ω automata, embedding of Presburg logic, equivalence of LO1 and temporal logic, simplex algorithm and Fourier/Motzkin method
  • induction-based verification: limited model checking, interpolation-based model checking, property directed reachability (PDR)

Literature

  • C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008
  • E.M. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 2000
  • B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, B. Berard, M. Bidoit, A. Finkel and F. Laroussinie, A.
  • Petit, L. Petrucci and P. Schnoebelen, Systems and Software Verification. Model-Checking Techniques and Tools, Springer, 2001
  • K. Schneider, Verification of Reactive Systems, Springer, 2003

Requirements for attendance (informal)

None

Requirements for attendance (formal)

None

References to Course [INF-62-52-K-6]

Module Name Context
[INF-62-52-M-6] Verification of Reactive Systems P: Obligatory 4V+2U, 8.0 LP
Course-Pool Name
[INF-ES_V-KPOOL-6] Lectures of the teaching area Embedded Systems and Robotics