salle A. Turing CE4
8 March 2012 - 14h00
Safety Analysis of Hybrid Systems with SpaceEx
by Goran Frehse from Verimag
Abstract: In a variety of application domains such as embedded and cyber-physical systems, model-based design relies on models that incorporate time-driven as well as event-driven behavior. These so-called hybrid systems are difficult to analyze, because even small errors in the analysis algorithm can lead to qualitatively different behaviors.
We verify safety properties of hybrid systems by computing their reachable states. Using set-based computations allows us to incorporate computation errors such that the resulting set is a conservative overapproximation of the actual solution. The difficulty is to find set representations for which the necessary operators are efficient to compute but still precise enough. In SpaceEx, our verification tool platform, we have implemented an algorithm that uses two set representations, polyhedra and support functions, to obtain maximum scalability. At each step of the algorithm, we choose the representation that provides the best compromise between speed and accuracy, based on the data and operator. While first-generation tools were limited to a few variables, we have used SpaceEx on hybrids systems with piecewise linear dynamics involving two hundred variables. In this talk, we present the SpaceEx platform and illustrate how combining different set representations makes the approach efficient.
