The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
|
|
|
On Bounded Model Checking of Asynchronous Systems
Toni Jussila
Dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the Department of Computer Science and Engineering for public examination and debate in Auditorium T1 at Helsinki University of Technology (Espoo, Finland) on the 18th of November, 2005, at 12 o'clock noon.
Dissertation in PDF format (ISBN 951-22-7904-5) [905 KB]
Dissertation is also available in print (ISBN 951-22-7903-7)
Abstract
This dissertation studies the verification of reachability properties of concurrent systems where the components of the system are Labeled Transition Systems (LTSs) using a symbolic model checking technique called Bounded Model Checking (BMC). BMC is a technique that seeks to answer the question whether among the system's executions shorter than some given number of steps there is one (or more) violating a given property. Answering this question is reduced to propositional satisfiability, i.e., to a propositional formula that is satisfiable iff there is such a violating execution. The translation from a system to a formula is polynomial in the size of the system but the running time of the propositional solver can be exponential in the number of atomic propositions in the formula. This number, on the other hand, correlates directly with the number of execution steps that the formula models.
Traditionally, LTSs are model checked by composing the components into a synchronized product and then applying a model checking algorithm on this product. The executions of the synchronized product are called interleaving executions. The research hypothesis of this work is that by using other composition operators than the one yielding the synchronized product, more efficient BMC algorithms can be obtained. The added efficiency comes from the fact that with these operators, propositional formulas with fewer atomic propositions are obtained. The reduction in the number of atomic propositions follows from the fact that fewer execution steps are needed to cover the same state space than when the synchronized product is used.
Three techniques to create composition operators are presented, namely (i) partial-order semantics, (ii) on-the-fly determinization, and (iii) local transition merging. These techniques can be combined in many ways.
The dissertation demonstrates that given a system of LTSs and a bound, a BMC formula modeling the executions of the products applying partial-order semantics and on-the-fly determinization can be created efficiently. That means that the translation effort is polynomial and the size of the resulting formula is linear in the size of the system and the bound.
The third of the applied techniques, local transition merging, provides potentially dramatic reductions to the bound needed to detect a violation of a reachability property. The size of the BMC formula modeling this execution model is no more linear, though, since a complicated constraint is needed.
The dissertation concludes with some experimental results comparing the products against each other and two state-of-the-art model checking tools.
Keywords: verification, symbolic methods, bounded model checking, labeled transition systems, partial order methods
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
© 2005 Helsinki University of Technology
Last update 2011-05-26