April 4, 2011
Pavithra Prabhakar
Cyber Physical Systems (CPS) is a term broadly used to define systems in which the cyber world consisting of computation and communication is tightly connected to the physical world. These systems have applications in Automotives, Medical Devices, Aeronautics and Robotics among several other areas. These systems are often deployed in safety-critical systems and hence their reliable performance is of utmost importance.
Verifying CPS is challenging due to the presence of continuous components modeling the physical world. The complexity of verification of these systems increases with the complexity of the continuous components, and is undecidable for a relatively simple class of systems. In fact, the problem of computing one-step successors which is a basic step in various state space exploration based verification techniques is undecidable for complex dynamical systems. Hence, the verification of these systems relies on developing techniques which can compute good approximations of these systems efficiently. I will describe some of my work on approximation techniques for the verification of CPS. In particular, I will talk about a technique for approximating general CPS by polynomial systems, and some results on how this process of approximation can be efficiently automated. I will also describe a counter-example guided abstraction refinement technique for hybrid systems which automatically refines an abstraction when it is not sufficient to prove the correctness of the system. I will discuss various cyber physical systems which have been analysed using these techniques.