Formal Methods Laboratory

General Information:

  • Practical Laboratory in English
  • 5 ECTS-Credits
  • Two presentations and one oral examination 

A miniaturized urban environment  represents the center of the laboratory. It consists of a number of traffic lights, parking gates, and mobile robots that navigate along a road network which is placed on a 2.5m x 2.5m wooden platform.



The content of the laboratory is divided in three task:

  • Modeling of the various parts using discrete transition systems.
  • Verification of different LTL properties of various subsystems of the urban environment.
  • Controller synthesis for the mobile agents to enforce certain LTL specifications.


The module Modeling and Verification of Embedded Systems, Experience in C/C++ programming.

Course Material:

Available at moodle