Explicit Model Checking Based on Integer Pointer and Fibonacci Hash

As the size of the formal model grows, the reachable state space grows exponentially thereby creating state space explosion problem. To alleviate the efficiency and memory bottleneck of explicit model checking, we present a technique that efficiently organizes the reachable state space, and implement an efficient explicit model checking system. The new method could not only effectively shorten verification cycle, but also generates counter example in cases system specification is unsatisfiable, which helps system designer to locate error rapidly. Experiments on some real-world models are conducted. Analysis and experiment results prove the effectiveness of our method.