HyConSys
Home
Members
Teaching
News
Research
Publications
Software
Contacts
Contact us

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, and 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:

  • C. Baier and J.-P. Katoen. “Principles of Model Checking,” The MIT Press, 2008.

  • P. Tabuada. “Verification and Control of Hybrid Systems,” Springer, 2009.