Research On A New Method Of Large Scale Model Checking Based On External Memory

Model checking is kind of technology which can verify the property of a system automatically. In recent years, model checking received extensive attention for its simplicity and without too much manual intervention. However, the current model checking techniques are mainly designed in validation level to judge whether the system has counterexample or not, namely, finding at most one counterexapmle per time.If we take consideration of the above question further, means we need to debug the system efficiently after the system was verified has counterexample. But, in general, a set of counterexamples even all counterexamples are need in debugging a large scale system. What’s more, the current model checking algorithm can not find a set of counterexamples for those large scale systems. Therefore, in this thesis, we aim at the above problems in large scale system verification and proposed the idea of finding mitiple counterexamples for large scale systems. And then, we analyzed and studied the main technique(finding accepting cycles) in finding multiple counterexamples.In this thesis, firstly, we summarize the development status of model checking, and come to conclusion that the current model checking technique can not find multiple counterexamples for large scale systems. Secondly, we introduce the basic theory of knowledge involved in model checking. Thirdly, we solve the state space explosion problem in large scale model checking using external memory. And then, we analyze and propose the new algorithm in detail. The algorithm is based on depth first search and starts from the initial state, and can find out all the elementary accepting cycles in linear I/O complexity. On the whole, the algorithm first searches for the strongly connected components(called SCC) which contain at least one accepting state(called Accept-SCC), and then find all the elementary accepting cycles contained in each Accept-SCC. To find an Accept-SCC first, we will enumerate much fewer redundant paths which are not components of any accepting cycles. Moreover, if a system has no Accept-SCC, meaning there is no counterexample, the algorithm will terminate early. In finding elementary accepting cycles in an Accept-SCC, we put forward to calculate the small Accept-SCC first in order to reduce the number of I/O access to the external memory.In the experiment, with the help of the famous open source model checking tool Spin, we embed the algorithm in Spin successfully. And then, we select the typical benchmarks in model checking field to do comparison experiments with the DAC and MAP algorithms mentioned in this thesis. The result of the experiments not only proves our algorithm can find out multiple counterexamples for large scale system but also shows the efficiency of our algorithm in the average time to find one counterexample is better than DAC and MAP. What’s more, the experiment in the end shows that the model checker Spin can’t finish to check a large scale benchmark which has no counterexamples.