The Search Of Parallel And Complete Model Checking Technology

Model checking is a kind of technology which can automaticly check the propertyof a system. It widely attracted people’s attention since it was proposed, and more andmore algorithms and technologies about model checking have been raised. However, allof them only can find out one counterexample at most in one time and then they quit thesearching. So, there is not an algorithm can search out all the counterexamples of asystem. Therefore, this thesis aims at this problem, and then proposes a ‘parallel andcomplete model checking’ algorithm which can find out all the counterexamples ofsystem after running the altorithm only once.In this thesis, it introduces the basic knowledge of model checking technology andsummarizes the development status of it at first. Then, it describes the parallel andcomplete model checking algorithm in detail. This algorithm can search out all thecounterexamples in linear complexity. It bases on the depth-first-search to search thestate space of system. The procecedure of searching is that, it parallel starts fromaccepting states of system to find out all the accepting cycles, then it parallel starts frominitial states to find out all the paths to accepting states. Finally, it uses the searchingpaths to construct the counterexamples. In the algorithm, I employ the paralleltechnology to accelerate the searching and use the hash function to speed up thecomparison. If a checking system with a huge scale, the algorithm will employ disks tostore the states. If the checked system without accepting cycles, the algorithm willterminate immediately, because this kind of situation means that there is nocounterexamples in system. It can shorten the search time.In the thesis, I not only prove the correctness of ‘parallel and complete modelchecking algorithm’ from three aspects, but also analyze the time complexity of it fromtwo sides. At the same time, I compare mine to others which show the outperformanceof mine. Then, I realized the algorithm on SPIN which is a model checking tool. Finally,I use the experiment to prove my algorithm could find out all the counterexamples ofchecked system. I compare my algorithm’s outcomes to SPINs’, which show myalgorithm not only can find out all the counterexamples of checked system, but also has higher search efficiency for checking the system without counterexamples. At the sametime, the experiments’ outcome shows the complexity of the parallel and completemodel checking algorithm is approximately linear with the number of states of system.