SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty.
Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke · 2014
tical testing We present a novel approach for solving the probabilistic bounded reachability problem of hybrid systems with parameter uncertainty. Standard approaches to this problem require numerical so-lutions for large optimization problems, and become unfeasible for systems involving nonlinear dynamics over the reals. Our approach combines randomized sampling of probabilistic system parameters, SMT-based bounded reachability analysis, and statistical tests. We utilize δ−complete decision procedures to solve reachability analysis in a sound way, i.e., we always decide correctly if, for a given combination of parameters, the system actually reaches the unsafe region. Compared to standard simulation-based analysis methods, our approach supports non-deterministic branch-ing, increases the coverage of simulation, and avoids the zero-crossing problem. We demonstrate that our method is feasible for general hybrid systems with parametric uncertainty by applying the implemented tool SReach to various nonlinear hybrid systems with parametric uncertainty. 1