Research On Counterexample Guided Abstraction Refinement Optimization Technology

The main bottleneck of model checking is the explosion of state space,which leads to the early detection of model is mainly used for the verification of small systems.In order to solve this problem,some methods,such as partial order reduction?ordered binary decision diagrams and abstraction,are proposed.In the above methods,abstraction technology is one of the important methods.Abstraction technology is one of the effective methods for the validation of large software systems,but one major obstacle is the abstraction of the system will introduce behaviors that not exist in the specific system,which may introduce spurious counterexamples.Therefore,it is necessary to refine the abstract model based on counterexample:(1)using dynamic abstraction refinement process to eliminate spurious counterexamples by refining Abstract model.The traditional counterexample guided abstraction refinement method can change the failure state by changing the set of visible variables,and other non-failure states are also affected.In this paper,we present a new method for partitioning failure states: adding the Boolean variable.The advantage of this method is that only the failure states are re-divided in the abstraction refinement,and other non-failure states are not affected.In this paper,a new method for finding the failure state is presented,which is based on the predecessor state and the successor state to determine whether it is a failure state.This method can avoid the polynomial time problem in the case of cyclic expansion.At the same time,the method of parallel computing failure state is presented,which can quickly locate the failure state.At last,the paper gives an abstraction refinement framework.(2)the static abstraction refinement process doesn't refine the abstract model,but a series of abstract models and heuristic algorithms are used to eliminate spurious counterexamples.In this chapter,we give a static abstraction refinement method,which does not refine the abstract model.In this method,a series of abstract models are used as input.The heuristic information is extracted from the original model,and a heuristic search algorithm is used to avoid the search of the whole state space,so that the space and time cost is reduced greatly.(3)a method based on the weights of selected spurious counterexamples is given.The traditional counterexample guided abstraction refinement method does not take into account the weight of counterexamples.The influence of each counterexample in the false path in the abstraction refinement is different,and the counterexample containing the higher weight abstract state is more important than the other counterexamples.Based on this,this paper gives the concept of the key counterexample.Then,by using the method of calculating the node weight in graph theory and combining it with the abstraction technology,this paper analyzes and gives a new algorithm to identify the key counterexample.This paper optimizes the abstraction refinement from the three aspects.In the first part,we use the method of dynamic refinement to eliminate the spurious counterexamples.In the second part,we use the static refinement method,not to refine the abstract model,but to eliminate the false counterexample by a series of abstract models.In the third aspect,the dissertation tries to find a counterexample of more weights to improve the efficiency of model checking.The first and the two aspect is about how to eliminate the counterexample from the dynamic and static methods.The third aspect is about how to choose the effective counterexample.