A True-Concurrency Encoding for BMC of Compositional Systems

This paper studies Bounded Model Checking (BMC) of invariant properties on compositional systems. To alleviate the path explosion problem resulting from interleaving, an ideal approach is to let the system execute in true-concurrency. However, since it is difficult for the true-concurrency execution manner to obtain all reachable global states, this technique has been rarely employed to verify those properties requiring to check all reachable global states-such as invariant properties. Verification of such properties still adheres to the interleaving semantics. Observed that even for properties such as invariants, it is possible to verify them via checking only a fraction of the global states, this paper presents a true-concurrency encoding for invariant property verification of compositional systems. The crucial innovation is a macro-step technique, which executes a sequence of consecutive transitions in true-concurrency. With this technique, we are able to (1) significantly reduce the exponential number of paths due to interleaving, and (2) greatly cut down the number of SAT calls required for BMC to verify the property. Experimental results of real problems show speed increases from 4.8 to 2957 times that of the standard verification method.