Counterexample-Guided Abstraction Refinement for Component-Based Systems

Compositional verification of invariants is a technique for alleviating the state explosion problem in component-based verification. The efficiency of these methods depends on abstraction, which leads to verification incompleteness. In this paper, we present a unified framework that combines compositional abstraction and counterexample-guided abstraction refinement (CEGAR) to address this incompleteness problem. We propose two refinement approaches: invariant strengthening and state partitioning. In the case of a spurious counterexample, our proposed invariant strengthening approach refines the abstraction by eliminating the infeasible states. The state partitioning approach exploits the semantics of component based systems and obtains a more precise system. Any safety property that holds on the abstraction is guaranteed to hold on the model refined by the state partitioning approach. The examples and experiments in this paper show that our verification method can achieve conclusive results in the verification of safety properties with deadlock freedom in component-based systems.