Exploiting step semantics for efficient bounded model checking of asynchronous systems

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 ∃∃-step semantics, its generalization, the relaxed ∃∃-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 to an explicit state model checker DiVinE on its own BEEM benchmark suite.

► Step semantics is shown to accelerate bounded model checking of asynchronous systems. ► Independence of system components is exploited to cover reachable states faster. ► Redundancy allowed by step semantics is further diminished by our process semantics. ► Variants of step and process semantics are compared experimentally and analytically. ► Applying step semantics is automatable, with a SAT or SMT solver back-end.