The efficiency of the compositional verification ofinvariants depends on the abstraction, which may lead to verificationincompleteness. The invariant strengthening and statepartitioning techniques are proposed in this paper. The formercould refine the overapproximation by removing the unreachablestates, and the latter is a variant of counterexample-guidedabstraction refinement. Integrated with these two refinementtechniques, a unified compositional verification framework is presentedto strengthen the abstraction and find counterexamples. Some examples are included to show that the verification of thesafety properties in component-based systems has been achievedby our framework.
展开▼
