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.
Similar content being viewed by others
Notes
The techniques presented in this paper can be adapted to handle synchronizations which are not in A m .
References
Ábrahám E, Becker B, Klaedtke F, Steffen M (2005) Optimizing bounded model checking for linear Hybrid Systems. In: VMCAI, pp 396–412
Akshay S, Bollig B, Gastin P (2007) Automata and logics for timed message sequence charts. In: FSTTCS, pp 290–302
Alur R, Yannakakis M (1999) Model checking of message sequence charts. In: CONCUR, pp 114–129
Audemard G, Bozzano M, Cimatti A, Sebastiani R (2005) Verifying industrial hybrid systems with MathSAT. Electron Notes Theor Comput Sci 119(2):17–32
Ben-Abdallah H, Leue S (1997) Timing constraints in message sequence chart specifications. In: FORTE, pp 91–106
Bengtsson J, Jonsson B, Lilius J, Yi W (1998) Partial order reductions for timed systems. In: CONCUR, pp 485–500
Bruttomesso R, Cimatti A, Franzén A, Griggio A, Sebastiani R (2008) The MathSAT4 smt solver. In: CAV. Springer, Berlin, pp 299–303
Bu L, Cimatti A, Li X, Mover S, Tonetta S (2010) Model checking of hybrid systems using shallow synchronization. In: FORTE, pp 155–169
Chandrasekaran P, Mukund M (2006) Matching scenarios with timing constraints. In: FORMATS, pp 98–112
Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: CAV, pp 359–364
Cimatti A, Mover S, Tonetta S (2011) Efficient scenario verification for Hybrid Automata. In: CAV, pp 317–332
Cimatti A, Mover S, Tonetta S (2011) HYDI: a language for symbolic hybrid systems with discrete interaction. In: EUROMICRO-SEAA, pp 275–278
Cimatti A, Mover S, Tonetta S (2011) Proving and explaining the unfeasibility of Message Sequence Charts for hybrid systems. In: FMCAD
Damm W, Harel D (2001) LSCs: breathing life into message sequence charts. Form Methods Syst Des 19(1):45–80
Dubrovin J, Junttila T, Heljanko K (2011) Exploiting step semantics for efficient bounded model checking of asynchronous systems. Sci Comput Program
Fränzle M, Herde C (2005) Efficient proof engines for bounded model checking of hybrid systems. Electron Notes Theor Comput Sci 133:119–137
Fränzle M, Herde C (2007) HySAT: an efficient proof engine for bounded model checking of hybrid systems. Form Methods Syst Des 30(3):179–198
Ghilardi S, Nicolini E, Ranise S, Zucchelli D (2007) Combination methods for satisfiability and model-checking of infinite-state systems. In: CADE, pp 362–378
Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: CAV, pp 72–83
Heljanko K, Niemelä I (2003) Bounded LTL model checking with stable models. Theory Pract Log Program 3(4–5):519–550
Henzinger TA (1996) The theory of hybrid automata. In: LICS. IEEE Comp. Soc., Los Alamitos, pp 278–292
Henzinger TA, Ho P (1995) HyTech: the Cornell HYbrid TECHnology tool. In: Hybrid systems II. LNCS, vol 999, pp 265–293
ITU-T (1996) Recommendation Z.120 - message sequence charts
Klose J, Wittke H (2001) An automata based interpretation of Live Sequence Charts. In: TACAS, pp 512–527
Ladkin P, Leue S (1992) On the semantics of message sequence charts. In: FBT, pp 88–104
Ladkin PB, Leue S (1995) Interpreting message flow graphs. Form Asp Comput 7(5):473–509
Li S, Balaguer S, David A, Larsen KG, Nielsen B, Pusinskas S (2010) Scenario-based verification of real-time systems using Uppaal. In: Formal methods system design, pp 200–264
Mauw S, Reniers MA (1997) High-level message sequence charts. In: SDL forum, pp 291–306
de Moura L, RueßH, Sorea M (2003) Bounded model checking and induction: from refutation to verification. In: CAV, pp 14–26
Müller O, Stauner T (2000) Modelling and verification using linear hybrid automata—a case study. Math Comput Model Dyn Syst 71:71–89
Pan M, Bu L, Li X (2009) TASS: timing analyzer of scenario-based specifications. In: CAV, pp 689–695
Pike L (2005) Real-time system verification by k-induction. Tech. Rep. NASA/TM-2005-213751, NASA
Samer M, Veith H (2007) On the notion of vacuous truth. In: LPAR, pp 2–14
Schuppan V (2009) Towards a notion of unsatisfiable cores for LTL. In: FSEN, pp 129–145
Sheeran M, Singh S, Stålmarck G Checking safety properties using induction and a SAT-solver
Tonetta S (2009) Abstract model checking without computing the abstraction. In: FM, pp 89–105
Vardi M (1995) An automata-theoretic approach to linear temporal logic. In: Banff higher order workshop, pp 238–266
Walter D, Little S, Myers CJ, Seegmiller N, Yoneda T (2008) Verification of analog/mixed-signal circuits using symbolic methods. IEEE Trans Comput-Aided Des Integr Circuits Syst 27(12):2223–2235
Wang F (2005) Symbolic parametric safety analysis of linear hybrid systems with BDD-like data structures. IEEE Trans Softw Eng 31(1):38–51
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Cimatti, A., Mover, S. & Tonetta, S. SMT-based scenario verification for hybrid systems. Form Methods Syst Des 42, 46–66 (2013). https://doi.org/10.1007/s10703-012-0158-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-012-0158-0