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.