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/C++ programming.
Course Material:
Available at moodle.