Name
Abstract | ||
|---|---|---|
Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC the system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the $k$-th instance to be satisfiable a counterexample for a given safety property has been found. In this paper we present a first approach to apply BMC to networks of timed automata (that is a system of several interacting subautomata) where parts of the network are unspecified (so called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. We provide solutions to this problem for two timed automata communication models. For the simple synchronization model, a BMC approach based on fixed transitions is introduced resulting in a SAT-Modulo-Theory formula. With respect to the use of bounded integer variables for communication, we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/MTV.2010.19 | Microprocessor Test and Verification |
Keywords | Field | DocType |
automata theory,computability,formal verification,real-time systems,SAT-Modulo-theory formula,bounded model checking,incomplete networks,real-time systems,satisfiability,timed automata,verification,BMC,Blackbox,SMT,Timed Automata,quantified SMT | Automata theory,Model checking,Computer science,Boolean satisfiability problem,Algorithm,Computability,Theoretical computer science,Solver,Counterexample,Formal verification,Bounded function | Conference |
ISSN | ISBN | Citations |
1550-409 | 978-1-61284-287-5 | 8 |
PageRank | References | Authors |
0.53 | 14 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christian Miller | 1 | 36 | 4.39 |
| Karina Gitina | 2 | 10 | 0.91 |
| Christoph Scholl | 3 | 346 | 32.07 |
| B. Becker | 4 | 191 | 21.44 |