Seminars

Computational Modeling and Analysis for Complex Systems Seminar (CMACS) PDF files
Goran Frehse - Universite Joseph Fourier, Grenoble

07/20/2011, 2pm, GHC-8102

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, so-called hybrid systems. For example, the design of a car braking system might involve a model of the time-driven physics of the car as well as the event-driven decision of the brake controller. Hybrid systems are difficult to analyze, because even a small variation in states or parameters, or small error in the analysis algorithm could possibly 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 over approximation of the actual solution. The difficulty is to find set representations for which the necessary operators are efficient to compute, and yet provide satisfactory precision. 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 hundred and more variables. In this talk, we present the SpaceEx platform and illustrate how combining different set representations makes the approach efficient. 

Biography

Goran Frehse did his undergraduate work specializing in control theory and hybrid systems at Karlsruhe University, Germany, obtaining a Diploma (M.S. equivalent) in Electrical Engineering and Information Technology in 1999. In his graduate research he started developing the verification tool PHAVer, and worked on the compositional verification of hybrid systems at the Process Control Laboratory at Dortmund University, Germany, and the Institute for Computing and Information Sciences at Radboud University Nijmegen, Netherlands, from where he received a PhD in Computer Science in 2005. During two years as a PostDoc at Carnegie Mellon University in Pittsburgh and one year at Verimag in Grenoble, France, he expanded his research interests to analog and mixed-signal circuits. Since Sept. 2006 he is assistant professor at Verimag. His latest project is SpaceEx, a development platform for verification algorithms for hybrid systems.