Title: Simulation-Based Verification of Hybrid Systems involving Novel Dynamic Refinement
Speaker: Hao Ren, ECpE Graduate Student
Abstract: Hybrid system verification tools based on reachability analysis suffer from fast growing error propagation introduced by overapproximation techniques used both at continuous and discrete stages. The continuous dynamics usually lacks analytical solutions to a starting condition, while the location of discrete jumps are subject to errors of simulations.
We present a simulation-based verification framework for systems modeled by hybrid automata. In this framework, a simulation is used as a reference for a class of system behaviors starting close to the start of the reference simulation. Any deviation from the reference trace is bounded at any finite time. A feature of our work, that makes it distinct from prior simulation-based verification works, is the flexibility of dynamically applying repartitioning in the process. Repartitioning is applied during continuous evolution for better error propagation, where as it is applied also during discrete transitions for correctly handling the effect of accumulated error that can introduce state jumps and impact reachability computation. We have developed a prototype verifier implementing our algorithms and provide verification results from several benchmarks to show its effective performance.