Formal Synthesis of Embedded Systems
General Information:
- Lecture and tutorial in English
- 2 SWS Lecture, 1 SWS tutorial
- 5 ECTS-Credits
- Written closed-book exam.
This course is the successor course of Modeling and Verification of Embedded Systems and focus on automated controller synthesis techniques for embedded systems to provably enforce desired specifications. The embedded systems range from discrete over continuous to hybrid systems. Different specifications like simple reachability and safety specifications or more complex general reactivity one specifications are considered. Many applications, including task planning for mobile robots, industrial process design and adaptive cruise controllers, are used throughout the course to illustrate the various concepts.
Content:
- Models of embedded/cyber-physical/hybrid systems: transition systems, finite state automata, control systems, system composition;
- Formal specifications: linear temporal logic, safety, reachability, generalized reactivity one;
- Controller synthesis for finite systems: two player games, maximal and minimal fixed points, safety games, reachability games, generalized reactivity one games;
- Abstraction and refinement: system relations, controller refinement, quotient systems;
- Infinite systems: linear control systems, nonlinear control systems;
- Applications: task planning for mobile robots, industrial process design, adaptive cruise controllers, pendulum like control systems.
Recommended Reading:
G. Reißig, A. Weber and M. Rungger. "Feedback Refinement Relations for the Synthesis of Symbolic Controllers," IEEE TAC, 2017
P. Tabuada. "Verification and Control of Hybrid Systems," Springer, 2009.
C. Baier and J.-P. Katoen. "Principles of Model Checking," The MIT Press, 2008.
Lecture notes and exercises:
Available at moodle.