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.

Content:

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.

Preconditions:

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