SMT-based verification of hybrid systems

Hybrid automata are a widely used framework to model complex critical systems, where continuous physical dynamics are combined with discrete transitions.
Several classes of hybrid automata can be encoded into infinite-state transition systems, and then verified using techniques based on Satisfiability Modulo Theories (SMT) solvers (e.g. bounded model checking, k-induction, IC3, ...).
We show different encodings of hybrid automata in infinite-state transition systems, amenable to verification using SMT-based techniques.The encodings cover different classes of hybrid systems, either in a precise or in an over-approximated way.
Then, we show efficient techniques to solve the scenario-based verification problem for a network of hybrid automata.
The problem consists of checking if the network accepts or rejects some desired interactions among the components, expressed using Message Sequence Charts (MSC).
We present two efficient approaches, one tailored to feasibility and the other to the unfeasibility of the MSC. Both approaches rely on the concept of local-time semantics to compose the asynchronous automata.
Finally, we will show the modeling language used to encode hybrid automata in hycomp, a tool that extend the capabilities of the model checker NuSMV to analyze hybrid automata.
This talk present several joint works with Alessandro Cimatti, Alberto Griggio, Ashish Tiwari, Stefano Tonetta.