CTL
29 May 2012 - 15h00
Reachability Analysis of Hybrid Systems Using Support Functions (Phd Defense)
by Rajarshi RAY from Verimag
Abstract: In model based design, one constructs a mathematical model of the system and uses it to design the system so that it exhibits the desired properties. For safety critical systems, it can be of utmost importance to verify these safety properties on the model, e.g., to account for parameter variations. Computing a finite number of system behaviors via simulation is not sufficient to guarantee safety properties. With a reachability analysis one can compute a cover of all possible system behaviors, potentially infinite, accounting for any non-determinism in the model, and with which one can guarantee safety properties. Systems of interest often exhibit both continuous and discrete behavior and such systems are called hybrid systems. Reachability computation is considered hard for continuous and hybrid systems. Only recently, scalable methods for reachability computation have been developed based on implicit set representations using the mathematical construct of support functions. In this thesis, we develop an extendable tool called SpaceEx for reachability of hybrid systems. Two reachability algorithms have been implemented in SpaceEx, one based on the PHAVer tool for linear hybrid automata and the other based on support functions for piecewise affine dynamics. The support function based algorithm has been tuned and its scalability has been improved by switching set representations. We propose an improved image computation algorithm for discrete transition that further reduces the over-approximation error and illustrate its accuracy and efficiency with several case studies.
Jury:
- Prof. Eugene Asarin, Université Paris Diderot - Paris 7, Rapporteur
- Prof. Radu Grosu, Vienna University of Technology, Rapporteur
- Prof. Andreas Podelski, University of Freiburg, Examinateur
- Dr. Colas Le Guernic, DGA, Examinateur
- D.R. Oded Maler, Verimag-CNRS, Directeur de these
- MCF Goran Frehse, Universite Joseph Fourier Grenoble 1, Co-Directeur de these
