SMT-based Scenario Verification for Hybrid Systems
Technical Report
Abstract
Hybrid automata are a widely used framework to model complex critical
systems, where continuous physical dynamics are combined with discrete
transitions. The expressive power of Satisfiability Modulo Theories
(SMT) solvers can be used to symbolically model networks of hybrid
automata, using formulas in the theory of reals, and SAT-based
verification algorithms, such as bounded model checking and
k-induction, can be naturally lifted to the SMT case.
In this paper, we tackle the important problem of scenario-based verification, i.e. checking if a network of hybrid automata accepts some desired interactions among the components, expressed as Message Sequence Charts (MSCs). We propose a novel approach, that exploits the structure of the scenario to partition and drive the search, both for bounded model checking and k-induction. We also show how to obtain information explaining the reasons for infeasibility in the case of invalid scenarios.
The expressive power of the SMT framework allows us to exploit a local time semantics, where the timescales of the automata in the network are synchronized upon shared events. The approach fully leverages the advanced features of modern SMT solvers, such as incrementality, unsatisfiable core extraction, and interpolation. An experimental evaluation demonstrates the effectiveness of the approach in proving both feasibility and unfeasibility, and the adequacy of the automatically generated explanations.