Debugging The Software Based On The Muti-counterexample From Model Checker

Nowadays, model checking has been widely used in verifying the properties of software. Model checking technique has a high degree of automation, when the designed system doesn’t satisfy a specification, model checking tool would return an error trace(a counterexample) at the source level as a witness to the violation. Through the analysis of counterexample we can obtain the cause why it violates the property, and these actions provide an important clue to revise system.Owing to the advantages of model checking, applying model checking to fault localization has become a focus. However, for the sake of complex system’s counterexample may be usually very long and difficult to understand, u sers have to spend considerable time inspecting a counterexample to understand the cause of the error. Model checker is able to generate all counterexamples, so we’d like to make use of multiple counterexamples to find the error, other than only using a counterexample at a time. In this paper, we propose an extension to the distance metric and Tarantula based approach to error explanation and fault localization.In previous methods, a single counterexample has been used to find errors, the choice of counterexample is without clue and usually not a good choice to complete fault localization. We know that only a single counterexample may not help in finding bugs, these methods that just catch only one point in single counterexample have to waste a lot of time in trying many different single counterexamples result from uncertain information. But multiple counterexamples will give a clear clue for fault localization. In our method, according to a set of counterexamples and successful executions and taking advantage of distance metric and Tarantula technique, we will find a counterexample and its most valuable successful execution, this counterexample is the best choice that most likely to find errors and give exact information for which predicate includes bugs, comparing the two executions help us find the cause of bugs. With Tarantula technique, our method would present a probabilistic rank of suspicious codes which are likely to be faulty, and these information always give us ability to obtain a most valuable counterexample.Usually, the codes are too many to find the error, so we also offers a method to localize the fault via employing the distance metric in a small part of the codes, rather than a whole trace, thus to improve the efficiency and accuracy. Distance metric provides technology to search for a most valuable successful execution matching the chosen counterexample. We integrate both techniques to increase the ability of finding the bugs quickly, and at the same time, by doing this we can also make a progress in the degree of accuracy. Also, there are a number of interesting avenues for future research to improve.