Symbolic-Numeric Reachability Analysis of Hybrid Systems

We consider the problem of reachability analysis in hybrid systems defined by the closed-loop interaction of a complex, continuous time plant model with a software-based controller. In practice, the plant model is, often, a coarse approximation of the real-world operating environment of the software, whereas the software itself is the artifact that ends up being deployed in the final system. In this talk, we summarize the state-of-the-art techniques for purely symbolic and purely numeric approaches to reachability analysis of hybrid systems. We make the case for approaches that combine simulation-based exploration of the plant state-space with a corresponding symbolic exploration of the controller. We propose a simple yet elegant method to carry out this joint symbolic-numeric exploration based on an abstraction of the plant model, and present promising experimental results on software-in-the-loop setups that are beyond the scope of many existing verification tools.