Abstract: 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 MRIs 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 analysis 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 verification plays an important role in ensuring correctness of operation. I will show how it is possible to automatically synthesize controllers from discrete specifications (regular languages, finite state machines, temporal logics, etc) for continuous systems. The synthesized controllers describe both the continuous control laws as well as its correct-by-construction software implementation. I will end the talk with some ideas on how to extend these techniques towards distributed implementations.

The event is co-sponsored by the Department of Electrical and Computer Engineering.

Paulo Tabuada was born in Lisbon, Portugal in 1975. He received his “Licenciatura” degree in Aerospace Engineering from Instituto Superior Tecnico, Lisbon, Portugal in 1998 and his PhD 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. He is currently an assistant professor in the Department of Electrical Engineering at the University of Notre Dame. 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 both the 2001 American Control Conference and the 2001 IEEE Conference on Decision and Control and he was the recipient of a NSF CAREER award in 2005. His research interests include modeling, analysis and synthesis of discrete-event, timed, hybrid and embedded systems as well as geometric control theory of nonlinear and Hamiltonian systems, hierarchical and distributed control systems and categorical systems theory.