Research And Implementation Of Model Checking Method Based On Interpolation And CEGAR

Software is an indispensable part in the national defense development,economy and people's livelihood.With the rapid development of software technology,the scale of software becomes larger and larger and the complexity of the software has been ever-increasing.Therefore the software security problem is more and more prominent.How to improve the correctness,reliability and security of software has become an urgent problem to be solved.Model checking is an important formal verification technique,which has been successfully applied in the verification of the software and hardware.The idea of model checking is based on exhaustive search of state space and the main challenge is state space explosion.The counterexample guided abstraction refinement is an important way to deal with this challenge.Craig interpolation is used to guide the refinement of the model in abstract model checking.In order to improve the verification efficiency of model checking,this paper proposes a new algorithm based on the Craig interpolation and CEGAR framework.The main contents and innovations of this paper are as follows.1.Two new interpolants,i.e.True and Error interpolants,are proposed to mark whether a program path is safe.True interpolant is used to determine whether each path starting from a certain location is safe and Error interpolant is used to determine whether there is an error path starting from a certain location.2.Using the two interpolants,a path pruning algorithm is proposed to reduce the scale of the searching path,thus improving the efficiency of model checking.For True interpolant,if it is a full interpolant and is implied by the path prefix of the current node,the execution subtrees under this node can be merged.For Error interpolant,if the path prefix of the current node implies an Error interpolant,the path is insecure.3.To accelerate the formation of full interpolant nodes,this paper presents a weight-based optimization algorithm.The main idea is to add a weight attribute for each edge of the program control flow graph which represents the number of branches that have not been traversed in the subsequent control flow graph of the current edge.In the process of traversing the control flow graph,the traversal order of the branches is determined by the weight.This paper analyzes the effect of the algorithm by validating the time and success rate.The experimental result shows that compared with the original algorithm 12% verification time has been saved and the success rate has increased by 4%.This algorithm is very effective.