Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

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

(1) , (1) , (1)
1

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.
Fichier principal
Vignette du fichier
978-3-642-30793-5_6_Chapter.pdf (397.48 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

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

Licence

Attribution - CC BY 4.0

Identifiers

Cite

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⟩
248 View
186 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More