Research On On-the-Fly And Dynamic Software Model Checking

Software trustworthiness has received great attention from the software engineering community.This is mainly due to several factors,including the large-scaled software system,the complexity of the inner structure of software,as well as the diversity of the application areas.In the different phases of software development,software trustworthiness appears various properties including correctness,dependability and security etc,and it synthesizes these properties.How to verify software trustworthiness is the key research field of trustworthy software,in which it is an extremely important research direction to exploit model checking for the temporal correctness verification of software.Software model checking is the algorithmic analysis of software to prove desired properties of their executions,and with the high level of automation it can return a counterexample when a software system violates a desired property.Besides,the state space of a software system model can be exponentially larger than the description of the program,such as the numbers of variables or concurrent components.Due to the exhaustive search in state space of a system model,model checking could fail to complete the verification at the desired time and memory costs.In a nutshell,this problem is known as state space explosion.Controlling state space explosion has therefore been a major direction of research in software model checking.State space explosion exists not only in the system-model-oriented static model checking approaches but also in the program-execution-based dynamic model checking approaches.In LTL(Linear Temporal Logic)static model checking,on-the-fly automata-theoretic LTL model checking is an effective approach to ameliorate the state explosion problem.It firstly translates an LTL property into an ?-automaton equivalent to the negation of the LTL formula.Then,the LTL model-checking problem is reduced to checking the emptiness of an?-automaton,i.e.the product of the system and an automaton for the negated formula.At the same time,on-the-fly emptiness check can return a counterexample for nonempty product automata,without ever constructing the complete state space.There are generally two kinds of co-automata with respect to LTL translation such as B(?)chi automaton and generalized B(?)chi automaton.Moreover,emptiness checks can be divided into two computation styles such as sequential and parallel algorithms.In these kinds of emptiness checks,there are many significant challenges to research.In dynamic model checking field of concurrent software,the interleaving explosion of concurrent threads brings about the execution state explosion.Stateful dynamic partial order reduction can effectively reduce the number of interleavings,however the effectiveness of this approach need be further improved.This thesis has researched four software model checking methods,including three emptiness checks from on-the-fly automata-theoretic LTL model checking and stateful dynamic partial order reduction from dynamic model checking,respectively.To solve their problems in four software model checking methods,the major contents are summarized as follows:(1)NDFS(Nested Depth-First Search)emptiness checks for B(?)chi automata often return the counterexamples unnecessarily lengthy,which hamper the error explanation and are apt to cost more time and memory.To solve this problem,an on-the-fly depth bounded emptiness check for Biichi automata is presented,which exploits the depth bounded reduction strategy to restrict an NDFS process to exhaustively explore the bounded product spaces.First,depth bounded reduction strategy sets the state minimum depth of product B(?)chi automaton as the bounding parameter.Then,it incrementally and soundly computes the bounded sets of product states.Moreover,the proposed emptiness check constrains the NDFS to exhaustively traverse the corresponding bounded product spaces in order to find counterexamples.The empirical results indicate that when a product automaton is nonempty,the proposed method can definitely and efficiently returns shorter counterexamples and keep at the same time and memory cost as the other emptiness check algorithms.(2)The SCC(Strongly Connected Components)based emptiness checks completely combined with bitstate hashing for generalized B(?)chi automata have no full consideration to the terminal condition of SCC mergence.To remedy the disadvantage and avoid the time and space cost,an on-the-fly bitstate hashing terminal SCC emptiness check for generalized B(?)chi automata is presented.First,the terminal SCC definition is formulated.Second,bitstate hashing technique is employed in terms of terminal SCCs fully explored.This correctness of the method is theoretically proved.The experimental results demonstrate that the method can successfully tackle any terminal condition of SCC mergence and decrease the memory cost.Furthermore,a composite heuristic is incorporated into the method so that an on-the-fly bitstate hashing terminal SCC heuristic emptiness check for generalized B(?)chi automata is also presented.According to the composite heuristic,any successor transitions of every state of a product automaton are divided into four levels.Therefore,whenever a transition is required to choose from all successor transitions of the current state to traverse the product space,the method choices a transition with the highest level.The empirical results show that the method further decreases the time and space consumption of emptiness check for generalized B(?)chi automata,and compared with other traditional methods,it outperforms them in terms of effectiveness.(3)For an on-the-fly parallel emptiness check with map(maximum accepting predecessor)propagation,there is a scenario where no accepting cycle is on-the-fly identified by its map propagation,i.e.all map values of an accepting cycle are out of the cycle.To solve the problem,a parallel emptiness check propagating map and nap(newly discovered accepting predecessors)is presented.In initial traversal phase of the state space of a product automaton,the proposed method propagates the map and nap values simultaneously.The map value is the same as the counterpart of the original method,and the nap value tracks the local traversal characteristic of the parallel emptiness check.The empirical results indicate that the early termination ratio of this proposed method is higher than that of the original method in terms of on-the-flyness,so under the above scenario the proposed method could discover an accepting cycle using nap propagation,and this method improves the time and memory effectiveness of parallel emptiness check.(4)When stateless or stateful dynamic partial order reduction verifies concurrent multithreaded programs,the computation of a candidate set is the key step for the refinement of a backtrack set.However,the cost to a candidate set actually exceeds the demand of the refinement of a backtrack set.To solve the problem,a stateful dynamic partial order reduction shrinking the candidates for backtrack sets is presented.The second condition of shrinking candidate backtrack set is that the first enabled transition after the given backtrack point has happens-before relation with the next transition,then there is at most only one enabled transition satisfying it in current interleaving,so shrinking candidate backtrack set removes the redundant transitions from the original candidate set.Consequently,this presented method uses the shrinking candidate set to refine backtrack set and efficiently conducts stateful dynamic partial order reduction.The empirical results show that the proposed method reduces the number of transitions explored,speeds up the refinement process and increases the efficiency of dynamic model checking.