The orthogonality between static slicing and abstract method has been used to furtherly reduce the state space in model checking. However, static slicing can not always guarantee a slicing model with an desired size. This paper proposes a new approach which compute the over approximate slicing of an abstract state graph other than a counterpart of a static slicing. An overapproximate slicing is obtained by only considering the data dependence relations between predicates, which will always lead to a slice with an ideal size for verification. Though the overapproximate slice only has a weak property resistance power, it is an super set of the abstract state graph, which guarantees if a property $\phi$ is satisfied on the overapproximate slice, then the original specification is a model of $\phi$. And if there appears a spurious counterexample, then it increases the precision of the overapproximate slice by refinement to keep the verification cost as low as possible. We also provide sufficient proof for the correctness of our method. The experimental result shows that our method improves the scalability of model checking remarkably and scales better to a larger system.
RSS Feed