The current trend in engineering is to embed microprocessors and sensors in almost every new or existing electromechanical system and critical infrastructure. Such systems have been recently referred to as Cyber-Physical Systems (CPSs) since they bridge the Cyber world of computation and communication with the Physical world of engineered systems. CPSs achieve enhanced functionality and performance for the users with ultimate goal the augmented system safety. At the same time, though, they increase the complexity of the engineered systems. The big challenge in CPSs is how to tame this complexity in order to guarantee correct and, most importantly, safe system operation.

This talk addresses such emerging issues from two distinct directions. First, we propose a method for analyzing the behavior of CPSs which must satisfy real-time and other operational constraints. Typical examples of such systems are analog and mixed-signal integrated circuits and medical devices. The advantages of our approach are that it is scalable and that it provides coverage guarantees. Second, we develop a framework for the provably correct automatic synthesis of controllers starting from high level specifications. The application domain for this methodology is robotic motion planning.

Georgios E. Fainekos is currently a Doctoral Candidate in the Department of Computer and Information Science at the University of Pennsylvania under the supervision of professor George J. Pappas. He received his Diploma degree in Mechanical Engineering from the National Technical University of Athens in 2001 and his M.Sc. degree in Computer and Information Science from the University of Pennsylvania in 2004. His research interests include formal methods, hybrid and embedded control systems, real-time systems, robotics and unmanned aerial vehicles. He was finalist for the best student paper in ICRA 2007.