Exploiting step semantics for efficient bounded model checking of asynchronous systems

Reference:

Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Exploiting step semantics for efficient bounded model checking of asynchronous systems. Science of Computer Programming, 77(10–11):1095–1121, 2012.

Abstract:

This paper discusses bounded model checking (BMC) for asynchronous systems. Bounded model checking is a technique that employs the power of efficient SAT and SMT solvers for model checking. The main contribution of this paper is the presentation of a simple modeling formalism independent way of translating an asynchronous system into a transition formula for three partial order semantics: the exists-step semantics, its generalization, the relaxed exists-step semantics, and a novel variant that combines the latter with the idea of process semantics. Step and process semantics have been introduced in earlier works for different low level asynchronous system formalisms to improve the efficiency of BMC. However, this paper is the first one showing how to translate the semantics for any asynchronous system modeling formalism including high-level data manipulation operations while encoding the independence of actions in a dynamic fashion. Thus, the approaches have been extended to cover a larger class of modeling formalisms. The technical approach uses the notion of a coherent encoding of the transition relation, making for a simple and elegant translation of the partial order semantics in question. The presented translations have been implemented and we present extensive empirical results comparing the efficiency of the different translations to each other as well as as to an explicit state model checker DiVinE on its own BEEM benchmark suite.

Keywords:

bounded model checking, step encodings, process semantics, asynchronous systems, SMT

Suggested BibTeX entry:

@article{DubJunHel:SCP-AVOCS,
    author = {Jori Dubrovin and Tommi Junttila and Keijo Heljanko},
    journal = {Science of Computer Programming},
    language = {eng},
    number = {10--11},
    pages = {1095--1121},
    publisher = {Elsevier},
    title = {Exploiting step semantics for efficient bounded model checking of asynchronous systems},
    volume = {77},
    year = {2012},
}