On the synthesis of correct-by-design embedded control software

Paulo Tabuada from UCLA

Recent advances in information technology are fostering the use of embedded microprocessors and wireless radios in the most diverse everyday objects. Examples include portable accessories such as mobile phones and PDAs; home appliances such as refrigerators, toasters and coffee machines; medical equipment such as defibrillators, dialysis machines and MRI’s among many other systems.
  
These embedded computing devices react to stimuli originating both from the continuous environment and from other neighboring devices resulting in complex behavior that is difficult to analyze and to prescribe. In this talk I will focus on the problem of synthesizing embedded control software that is provably correct-by-design. This approach contrasts with current techniques where formal verification plays an important role in ensuring correctness of operation. I will show how it is possible to automatically synthesize controllers from discrete specifications (languages, finite state machines, temporal logics, etc) for purely continuous systems. The synthesized controllers describe both the continuous control laws as well as its correct-by-design software implementation.

Paulo Tabuada 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.  His research interests include modeling, analysis and control of real- time, embedded, networked and distributed systems; geometric control theory and mathematical systems theory.