amphithéâtre, bâtiment IMAG de l'Univ. G
26 May 2016 - 17h00
Scalable Verification of Hybrid Systems (HDR)
by Frehse Goran from VERIMAG
26 May 2016 - 17h00
Scalable Verification of Hybrid Systems (HDR)
by Frehse Goran from VERIMAG
Abstract: In model-based design, a mathematical model of the system behavior is used to check whether it achieves the desired performance (e.g., rise or settling time) while satisfying critical safety constraints (e.g., saturation, overflow). This check can be difficult, in particular when the system is hybrid, i.e., has continuous dynamics (physics) as well as event-based dynamics (mode switching). The system may further be subject to a range of initial conditions, disturbances, parameter variations, etc. Techniques such as Monte-Carlo and corner case simulation help to gain confidence in the design, but require a large number of simulation runs and generally do not provide conservative answers.
Set-based reachability analysis can complement such trajectory-based analysis techniques. Instead of computing a sequence of points on a single trajectory, one computes a sequence of sets that covers all possible trajectories of the system. Starting from a given set of initial states, the cover is derived by repeatedly computing one-step successor states. In general, one-step successors can only be computed approximately and the computation scales poorly in the number of continuous variables. Furthermore, the approximation error requires attention since it can accumulate rapidly, leading to a cover that is too coarse, to state explosion, or preventing termination. Based on previous work by Le Guernic and Girard, we present an approach with precise control over the balance between approximation error and scalability. By lazy evaluation of abstract set representations, the precision can be increased in a targeted manner, e.g., to show that a particular transition is spurious. Each evaluation step scales well in the number of continuous variables. The set representations are particularly suited for clustering and containment checking, which are essential for reducing the state explosion. This provides the building blocks for refining the cover of the reachable set just enough to show a property of interest. The approach is illustrated on several examples.
Jury:
Dr. Alain Girault (INRIA), Président
Prof. Eugene Asarin (IRIF, Université Paris Diderot et CNRS), Rapporteur
Prof. Manfred Morari (ETH Zurich), Rapporteur
Prof. Pravin Varaiya (University of California Berkeley), Rapporteur
Prof. Rajeev Alur (University of Pennsylvania), Examinateur
Prof. Eric Goubault (École polytechnique), Examinateur
Dr. Oded Maler (CNRS), Examinateur
