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.
Type de document :
Communication dans un congrès
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

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01528739
Contributeur : Hal Ifip <>
Soumis le : lundi 29 mai 2017 - 15:54:03
Dernière modification le : lundi 29 mai 2017 - 15:55:35
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 11:22:45

Fichier

978-3-642-30793-5_6_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

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〉

Partager

Métriques

Consultations de la notice

64

Téléchargements de fichiers

57