Research Of Fault Localization Based On Formal Methods

With the rapid development of information technology,the application field of computer hardware and software system is expanding,and their scale and complexity are also increasing.The hardware and software system not only bring convenience to human society,but also bring a lot of immeasurable risk.The correctness and reliability of the hardware and software system are ever increasingly serious.To guarantee the correctness and reliability of software and hardware system,we need to go through the extensive testing and debugging.However,testing and debugging of hardware and software are expensive and require amount of manual intervention.Therefore,it is imperative to develop the more effective and efficient fault location methods for large-scale software and hardware systems.Formal method is an effective method to improve the correctness and reliability of hardware and software systems,which can detect inconsistencies,ambiguities and errors in the early stage.Model checking is a common method for system verification.When the specification to be verified isn't satisfied,the model checker gives a counterexample which shows some defects or errors exist in the system.However,the model checker only shows the existence and does not indicate the cause of the error.At the same time,since the size of the system,the counterexample is becoming more and more long and complex.Therefore,the study of fault location based on model checking is of great significance.The main contributions of this thesis are listed as follows.1)A method for solving the satisfiability problem is proposed by using support vector machine during the bounded model checking.This method makes full use of the advantages of support vector in solving small samples and nonlinear problems.According to the characteristics of the variable value of the satisfiability problem,the solution is regarded as a dichotomies problem.Firstly,the training samples are collected according to the characteristics of each satisfiability problem.Then the variables were classified,eventually the result of variable classification is applied in incomplete algorithm as initialization assignment,and we reduce the number of flip variable values in the solving process.We can also apply the results in the decision process of complete algorithm,reduce the complexity of the search tree.2)Through comparing the counterexample and witress,a nearest witress searching method based on satisfiability and counterexample guided is proposed.When a counterexample has been given by the bounded model checker,the hardware and software systems and their specification are coded into an SAT instances.The counterexample cannot meet the SAT instances while the witress can meet it.Then the SAT instance is transformed into the form of conjunctive normal form.By using an algorithm similar to the DPLL algorithm and the values of the variable in the counterexample to solve the SAT instance,we get an assignment and it is the witress.In order to guarantee the shortest distance between the counterexample and the witress,the alogorithm needs execute many times.Finally,the most appropriate witress was chosen to get the best possible errors.3)A fault location method based on improved genetic algorithm has been proposed.The method is universality,natural concurrency and does not depend on the specific issues.According to the characteristics of the model,a small initialized population is given.There are two conditions need to meet by the witress,so two fitness functions were developed to keep the excellent genetic from the last generation.The directed mutation not only to ensure the diversity of population and avoid the invalid individuals generation,which accelerates the convergence speed and improves the efficiency of the algorithm.Experiments show that the counterexample understanding method which introduced the heuristic information to reduce the state space based on improved genetic algorithm,has fast convergence speed and wide application range.4)A fast algorithm for fault location based on the weakest precondition is proposed.The method starts with the assertions which the program needs to satisfy.We firstly calculate the entire weakest preconditions of the program according to the derivation rules,and then construct the error analysis graph of the whole weakest preconditions of the program;Secondly we exected two simple top-down and down-top labeling process on the error analysis chart.The conflict nodes are the suspects and the corresponding statements are doubtful statements.The experimental results compared with other methods demonstrate that,the error location method based on the weakest pre condition can effectively improve the accuracy of fault location,and can greatly reduce the workload of the debugger.