Fault Location Of Counterexamples Based On Model Checking

With the development of computer and network technology, multithreaded program system has been widely used. Basically all network communication system is a multithreaded system. It is well known that uncertainty of execution between the threads in the program, resulting in a number of program failure. The traditional fault debugging method, need to interrupt several times in the form of execution of the program to get more the information, and then through analysing statement step by step to fault debug. This process is entirely dependent on handwork with a lot of time and energy. It’s very inefficient. Therefore, the research of a fault location method for automatic or semi-automatic is very significant.Model checking is a verification technology based on formal methods. Because of the automation and completion, it was widely used in the industrials, such as hardware, software and protocol. Model checking has the advantages of automation and static, that can help us to locate fault for multithreaded program without the need for executing program again and again and realizing the automated detection of program failure. We can use it to fault detection for multithreaded programs. The fault localization based on model checking technology is mostly based on a single example, but a single counterexample often fail to give users detailed information to locate the fault. In order to enable users to obtain enough information to locate the fault, we will use multiple counterexample to locate fault for multithreaded program. We propose an algorithm and fault location method based on the reference series model. We can effectively detect and locate the bug of data race, deadlock and improper order procedure in multithreaded program through our algorithm.The research in this thesis is divided into three parts. The First part is counterexamples path information collection. We use model checking technology to simulate and verify the multithreaded program, and then collecting counterexamples which not satisfy the specification of the system, and then turn the counterexamples information to the references. Part two is the reference sequence model detection. We define the reference sequence model based on the reason that resulting the fault of multithreaded program, and present a detection algorithm based on the reference sequence model. Third part is fault location. We using a static method for probabilitycalculation of the failure sequence, rank probability of the failure. Finally, we implemented the fault location tool, Detector, based on the algorithm, achieving the effect of automatic fault location. Through the experiment of our method, the effect showed our method has greatly improving the efficiency of fault location.