On the Synthesis of Correct-by-design Embedded Control Software

The tight integration of computational systems with the physical world, now known as Cyber-Physical Systems, is believed to hold great promise for the competitiveness of several industries such as automotive, aerospace, chemical production, energy, healthcare, manufacturing, etc. Within Cyber-Physical Systems, embedded control software plays a major role by monitoring and regulating several continuous variables through feedback loops. Nevertheless, the design of embedded control software is still considered an art for which no rigorous and comprehensive design methodologies exist. In order to detect and eliminate design flaws and the unavoidable software bugs, a larger part of the design budget is consumed with validation and verification efforts.

In this talk, I will propose a new paradigm for the synthesis of embedded control software. By changing the emphasis from verification to design, I will show that it is possible to synthesize correct-by-design embedded control software while providing formal guarantees of correctness and performance. This proposal is grounded on several technical results describing how differential equation models for control systems can be transformed into equivalent finite-state models for the purpose of software design. The new finite-state models offer a common language within which it is possible to express and solve design problems meeting computational and physical requirements. In particular, I will show how it is possible to automatically synthesize controllers enforcing discrete specifications (languages, finite state machines, temporal logics, etc) on continuous systems. The synthesized controllers describe both the continuous control laws as well as its correct-by-design software implementation.

Paulo Tabuada was born in Lisbon, Portugal, one year after the Carnation Revolution. He received his "licenciatura" degree in Aerospace Engineering from Instituto Superior Tecnico, Lisbon, Portugal in 1998 and his Ph.D. degree in Electrical and Computer Engineering in 2002 from the Institute for Systems and Robotics, a private research institute associated with Instituto Superior Tecnico. Between January 2002 and July 2003 he was a postdoctoral researcher at the University of Pennsylvania. After spending 3 years at the University of Notre Dame as an Assistant Professor he joined the Electrical Engineering Department at the University of California at Los Angeles.

Paulo Tabuada was the recipient of the Francisco de Holanda prize in 1998 for the best research project with an artistic or aesthetic component awarded by the Portuguese Science Foundation. He was a finalist for the Best Student Paper Award at the 2001 American Control Conference and at the 2001 IEEE Conference on Decision and Control, as a student, and at the 2008 IEEE Conference on Decision and Control, as an advisor. He was the recipient of a NSF CAREER award in 2005 and is an IEEE Senior Member. He co-edited the volume Networked Embedded Sensing and Control published by Springer, co-chairs the International Conference Hybrid Systems: Computation and Control 2009 (HSCC'09), and serves as an associate editor for the IEEE Embedded Systems Letters.

His research interests include modeling, analysis, and control of real-time, embedded, networked, and distributed systems; geometric control theory and mathematical systems theory.