Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata

Abstract : Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based BMC approaches for TAs search for finite counter-examples and infinite lasso-shaped counter-examples. This paper shows that lasso-based BMC cannot detect counter-examples for some linear time specifications expressed, e.g., with LTL or Büchi automata. This paper introduces a new SMT-based BMC approach that can find a counter-example to any non-holding Büchi automaton or LTL specification and also, in theory, prove that a specification holds. Different BMC encodings tailored for the supported features of different SMT solvers are compared experimentally to lasso-based BMC and discretization-based SAT BMC.
Document type :
Conference papers
Holger Giese; Grigore Rosu. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7273, pp.84-100, 2012, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-30793-5_6〉
Liste complète des métadonnées

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01528739
Contributor : Hal Ifip <>
Submitted on : Monday, May 29, 2017 - 3:54:03 PM
Last modification on : Monday, May 29, 2017 - 3:55:35 PM
Document(s) archivé(s) le : Wednesday, September 6, 2017 - 11:22:45 AM

File

978-3-642-30793-5_6_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Roland Kindermann, Tommi Junttila, Ilkka Niemelä. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. Holger Giese; Grigore Rosu. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7273, pp.84-100, 2012, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-30793-5_6〉. 〈hal-01528739〉

Share

Metrics

Record views

66

Files downloads

64