Model Checking Method Based On Memory And State Management

Model checking is an automated formal verification technology, mainly used fordetection of hardware and software design models, in which model specification isgiven by the temporal logic formula. Model checking takes the model described by theuser as input, and then found if the assumption of the model which the user asserts isvalid or not. If not, it can produce a counter-example of the running trajectory.Due to the existence of sate space explosion problem, there is no enough memoryto hold all the states of some system needed to be verified. This is the bottleneck inlarge-scale concurrent system verification.on-the-fly model checking，Applying automata theory to model checking, in manycases may not be needed to construct the entire system state space. This is becausewhile checking the emptiness of the language accepted by both automata, the state ofsystem automata A is constructed only when needed.The advantage of on-the-fly model checking, when detecting the language acceptedby system automata A and property automaton Sis that some state of A would never begenerated at all. Another advantage is that, before completing the delivery construct ofthe two automata, we may have found a counter-example. Once you find a counterexample, there is no need to continue to construct the product automaton.During on-the-fly model checking, product automaton’s statesare generateddynamically by the double depth first research algorithm。We analyze the memory usageof the double depth-first algorithm in the checking process.In the process, two stacks areneeded to conduct the search progress.If the system is large, searching path may be verylong, whichmeans that there are a lot of states are stored in stacks.By using database, we can store states that temporally not needed in to externalmemory, and then reduced the memory needed.Therefore we increased the ability ofspin in model checking.We present two ways to utilize the database：a static state and memory managementmethod and a dynamic state and memory management method.When use the strategydescribed above, memory thrashing may be occur during transferring states between memory and disk. We provide memory state management strategies to solve thisproblem.We implement our algorithm on the basis of SPIN, motivated by utilizing datastructure, states manipulating strategy and input and output methods of SPIN.In the last,we analysis the result of experiments we do, to find out the practical effect of thedynamic management of memory in t the algorithm. Besides, we give theadvantage inthe actual operation of the algorithm and future work.