Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-62-52-M-6

Verification of Reactive Systems (M, 8.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-62-52-M-6 Verification of Reactive Systems 8.0 CP (240 h)

Basedata

CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in SuSe
Level [6] Master (General)
Language [EN] English
Module Manager
Lecturers
Area of study [INF-ES] Embedded Systems and Robotics
Reference course of study [INF-88.79-SG] M.Sc. Computer Science
Livecycle-State [NORM] Active

Courses

Type/SWS Course Number Title Choice in
Module-Part
Presence-Time /
Self-Study
SL SL is
required for exa.
PL CP Sem.
4V+2U INF-62-52-K-6
Verification of Reactive Systems
P 84 h 156 h
U-Schein
ja PL1 8.0 SuSe
  • About [INF-62-52-K-6]: Title: "Verification of Reactive Systems"; Presence-Time: 84 h; Self-Study: 156 h
  • About [INF-62-52-K-6]: The study achievement "[U-Schein] proof of successful participation in the exercise classes (ungraded)" must be obtained.
    • It is a prerequisite for the examination for PL1.

Examination achievement PL1

  • Form of examination: written exam (Klausur) (60-180 Min.)
  • Examination Frequency: each semester
  • Examination number: 66251 ("Verification of Reactive Systems")

Evaluation of grades

The grade of the module examination is also the module grade.


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)

Competencies / intended learning achievements

Upon successful completion of the module, students will be able to
  • specify temporal properties of reactive systems,
  • select suitable specification logics for this purpose,
  • understand the functioning of model testing procedures,
  • implement own verification procedures.

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 of the module (informal)

None

Requirements for attendance of the module (formal)

None

References to Module / Module Number [INF-62-52-M-6]

Course of Study Section Choice/Obligation
[INF-88.79-SG] M.Sc. Computer Science [Core Modules (non specialised)] Computer Science Theory [WP] Compulsory Elective
[INF-88.79-SG] M.Sc. Computer Science [Core Modules (non specialised)] Formal Fundamentals [WP] Compulsory Elective
[INF-88.79-SG] M.Sc. Computer Science [Specialisation] Specialization 1 [WP] Compulsory Elective