When Lyapunov goes to Church, formal synthesis of complex systems emerges


Prof. Dr. Majid Zamani

29.06.2016, 10:00, room 4981


Embedded control software plays a crucial role in many safety-critical applications: modern vehicles, for instance, use software to control steering, fuel injection, and airbag deployment. These applications are examples of so-called cyber- physical systems (CPS), where software components interact tightly with physical systems. Although CPS have become ubiquitous in modern technology due to great advances in computational devices, the development of core control software running on these systems is still ad hoc and error-prone. In this talk, I will propose a transformative design process, in which the controller code is automatically synthesized from higher-level correctness requirements. The proposed techniques are unified in that they combine techniques from discrete systems theory from computer science (e.g.  infinite games) with continuous dynamical systems from control theory (e.g. Lyapunov stability). The proposed automated synthesis of embedded control software holds the potential to develop complex yet reliable CPS while reducing verification and validation costs