Title :
Bounded Model Checking of Incomplete Real-time Systems Using Quantified SMT Formulas
Author :
Miller, Christian ; Gitina, Karina ; Becker, Bernd
Author_Institution :
Inst. of Comput. Sci., Albert-Ludwigs-Univ., Freiburg, Germany
Abstract :
Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is bounded model checking (BMC) where the system is iteratively unfolded and transformed into a satisfiability problem. In this paper, we apply BMC to incomplete networks of timed automata, i.e. systems containing so-called black boxes. In this context, we answer the question of unrealizability, that is, is a safety property violated regardless of the implementation of the black boxes. We focus on problems where the error path depends on the behavior of the black boxes such that an encoding using universal quantification is needed. This yields more advanced quantified SMT formulas, which can no longer be solved by conventional SMT solvers. Taking several prevalent communication models into account, we show how to encode the unrealizability problem and present several procedures to solve the resulting quantified SMT formulas efficiently using And-Inverter-Graphs extended by linear constraints over reals. Finally, we give experimental results to show the applicability of our verification methods.
Keywords :
automata theory; computability; formal verification; real-time systems; and-inverter-graphs; black box; bounded model checking; incomplete real-time system; linear constraint; quantified SMT formula; safety property; satisfiability problem; system verification; timed automata; universal quantification; Automata; Benchmark testing; Clocks; Encoding; Production; Protocols; Synchronization; blackbox; bounded model checking; incomplete designs; quantified SMT; timed automata;
Conference_Titel :
Microprocessor Test and Verification (MTV), 2011 12th International Workshop on
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4577-2101-4
DOI :
10.1109/MTV.2011.13