Research On Abstraction-refinement Method Of Software Model Checking

Software model checking is an important technique that uses formal methods to verify the reliability of target software.According to the direction it uses to guide the approximation,methods of software model checking could be classified into two categories: over-approximation and under-approximation.The topic of this dissertation focuses on a special kind of methods called abstraction-refinement methods which belong to a mixed approach of both.In general,mixed approach could covers overapproximation and under-approximation to get better properties.For a long time,exploring and researching state space of program requests either over-approximation methods or under-approximation methods.They work separately with individual algorithm,since they rely on different program state space model.The differences between these kinds of algorithms are also quite large,since they couple with their underlying state spaces.These inner differences causing gaps between different categories of software model checking methods that leads to difficulties of mutual references in algorithm and reuse of results of different methods.Recent years,research on the combination of methods of different categories has raised.It mixes overapproximation and under-approximation methods by designing merging operation of states with different abstraction.Through it produces lots of optimized results,the exploitation of mixing is still shallow.The deep reason why software model checking methods are not deeply merged is the lack of a unified abstract program state space model that describes structure information of the program.Current program state space models are built on top of different branches of logic theories.The logic theories formulate state and reasoning systems of a program state model.Logic formula is a representation of concrete state and describes individual state.It contains not enough information to illustrate a global status of the target program.In this dissertation,it gives a history of software model checking research at first.Our work is built upon previous work and the contribution of related researchers.The detailed research of this dissertation shows below:(1)The first part of this work is grown on the method of under-approximation.It analyses the obstacle of bounded model checking method when dealing with common input programs.This obstacle lays in the inconsistent distance of program state space and program execution flow.The consequence of the inconsistency is the bias between reached states and target states,when traversing program state space with bounded model checking method.This bias causes redundant execution on state space.If this situation occurs often,it will impact the total performance.To solve this problem,this dissertation works out with a novel method that measures program execution flow in a new way.The new measurement could guide the direction of traversal on target program state space.It makes reached states more consistent with the target states.A bunch of experiments were designed to prove this method improved the performance of original bounded model checking method.Through the research of under-approximation method,original bounded model checking method get improved and the existence of two directions in common program state space is revealed.(2)This part of research focuses on a widely used abstraction method called predicate abstraction.In this section,this method gets analyzed and the redundant traversal when processing with loop structure of the target program is found.Then a solution equipped with k-induction to generate loop invariant is proposed.This solution can bypass the irrelevant loop structure with a proper loop invariant.The improvement also decouples predicate abstraction from main algorithm and makes it modular.At the same time,k-induction is lifted up to abstract state space from concrete state space.At last,these two mechanisms are combined into a novel method.With experiments,the validity of this method is proved and no significant impact on performance is brought in.The research on over-approximation method gives an improvement on loop program checking and a potential way of modulating general abstraction-refinement algorithms is found.(3)After these researches upon,it is highly doubted that abstraction-refinement methods have unified structure of algorithm.So,it's reasonable to dig this deeper.In this part of research,the common properties of ordinary abstraction-refinement methods have been analyzed.Moreover,ordinary under-approximation and over-approximation methods are decoupled.Then a unified modular abstraction-refinement algorithm framework is established.This method has a more powerful flexibility and universalism.Classic model checking methods can be modulated to be the sub-methods this framework.The experiments show that this framework doesn't add extra impact on performance.(4)At the last of this dissertation,the novel unified state space model and its properties are researched.This part of research establishes a global view of state space model with the structure information of the corresponding program.Through this research,the duality property of general program state space is found.Using this property as the basis,the orthogonal property of program state model gets established.This property is used to explain the effectiveness of abstraction-refinement methods.Finally,the unified state space model is mapped to a metric space and the property of uncertainty is derived.With this property,the boundary of performance of software model checking can be determined.