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 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 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 construction software implementation. I will end the talk with some ideas on how to extend these techniques towards distributed implementations.
Class01
Friday, April 7, 2006 at 2 p.m.
8 St. Mary’s St. Room 901
Paulo Tabuada
Department of Electrical Engineering
University of Notre Dame
University of Notre Dame
On the Synthesis of Correct-by-Design Embedded Control Software
Abstract
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 form the Institute of 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. He co-edited the volume Networked Embedded Sensing and Control published in Springer’s Lecture Notes in Control and Information Sciences series.
His research interests include modeling, analysis and control of real-time, embedded, networked and distributed systems; geometric control theory and mathematical systems theory.
Host: Professor Belta
Student Host: James Kang