SMT-based verification of hybrid systems

Sergio Mover - Fondazione Bruno Kessler - Trento
Date and time
Tuesday, November 19, 2013 at 5:00 PM - 4:45 p.m. rinfresco; 5:00 p.m. inizio seminario
Ca' Vignal - Piramide, Floor 0, Hall Verde
Programme Director
Graziano Pravadelli
External reference
Publication date
October 27, 2013
Computer Science  


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.     

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234