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 programming.