Recent Advances In Verification And Analysis Of Hybrid Systems

Formal verification of properties is a very important area of analysis of hybrid systems. It is, indeed, essential to use methods and tools to guarantee that the global behaviour of a system is correct and consistent with the specifications. This is especially true for safety properties that insure that the system is not dangerous for itself or its environment.Classically, verification of Safety properties may be performed with reachability computation in the hybrid state space. Basic ideas have not really evolved since the first works, however new techniques have been proposed and algorithms have been improved.The aim of this talk is to present the problem of verification and reachability computation for hybrid systems and to propose a classification of recent improvements. To overcome the difficulties in verification and reachability analysis it is necessary to make choices regarding general principles, algorithms and mathematical representation of regions of the continuous state space. These choices depend on each other and must be consistent. However all approaches are based on common considerations that will be used to structure the talk.