Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

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

Résumé

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.
Fichier principal
Vignette du fichier
978-3-642-30793-5_6_Chapter.pdf (397.48 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01528739 , version 1 (29-05-2017)

Licence

Paternité

Identifiants

Citer

Roland Kindermann, Tommi Junttila, Ilkka Niemelä. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. 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. pp.84-100, ⟨10.1007/978-3-642-30793-5_6⟩. ⟨hal-01528739⟩
256 Consultations
190 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More