salle A. Turing CE4
16 janvier 2013 - 14h00
Approximation based Verification of Hybrid Systems
par Prabhakar Pavithra de IMDEA, Spain
Abstract: The increasing demand for automation in safety-critical applications such as aeronautics, automotive, industrial process control, medical devices and so on, has pressurized the need for scalable formal analysis techniques for ensuring reliable and error-free operation of the systems. A unique feature of these systems is the mixed discrete continuous behaviors they exhibit, which is due to the interaction between a digital computer controlling a physical entity. From the point of view of computability, presence of the continuous dynamics makes the problem challenging so much so that the verification of even simple properties becomes undecidable for a class of systems with fairly simple continuous dynamics. Approximations have proven to be a key component in dealing with the state space explosion resulting from the hybrid models. In this talk, I will discuss various approximation techniques for different classes of systems and properties, including, counter-example guided abstraction refinement and bounded error-approximations.
