Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate

Abstract

We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a, trajectory to an unsafe state. The approach is to approximate how close a point is to being an initial point, of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for all optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verification algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts.