| As a method of formal verification,model checking has been rapidly developed and widely used.One of the basic problems of model checking is state explosion problem.There are many solutions to this problem,and counterexample-guided abstraction refinement is widely used.The counterexample-guided abstraction refinement algorithm can effectively alleviate the state explosion problem in a certain extent,but there are still the following two problems: one is that many types of errors are very difficult to detect if the program is not executed,such as the functional correctness of the loopholes,the other is that all the branches in the construction of the system model are reachable by default in abstract technology,the fake counterexample path is refined until a counterexample path is found.while dynamic execution can effectively avoid unnecessary refinement.Based on this,the new algorithm is introduced-counterexample guided abstract dynamic execution refinement.The new algorithm adds dynamic execution to counterexample guided abstraction refinement algorithm.During the construction of the abstarct model,it can automatically switch between abstract detection and dynamic execution according to the branch node type.All the branch nodes in the program are divided into deterministic branch node and non deterministic branch node.During the construction,when a deterministic branch node is encountered,the new algorithm get uniquely determining successor by dynamic execution,when the non deterministic branch is encountered,the abstract detection is performed to expand all branches’ successor.In particular,in order to take advantage of the dynamic execution effectively,the program is divided into deterministic program and non deterministic program before model checking,If it is a deterministic program,you can directly detect the correctness of the system through dynamic execution without the building of system model.CPAChecker is a reliable tool for software model checking tool,including predicate detection,explicit analysis and other detection methods.The predicate detection method uses counterexample guided abstraction refinement algorithm,and the abstraction technique uses predicate abstraction.The new algorithm is implemented on the basis ofCPAChecker predicate detection method.Abstract detection technology could effectively control the size of the model,and the adding of dynamic execution can reduce the misjudgment caused by abstraction method,on the other hand it guides the system to construct a more accurate model,which can avoid unnecessary refinement.Through the analysis of the experimental data,the new algorithm can greatly improve the efficiency and accuracy of the traditional counterexample guided predicate refinement algorithm. |
