Gi Hwon Kwon

The KIPS Transactions:PartD, Vol. 11, No. 6, pp. 1295-1300, Oct. 2004
10.3745/KIPSTD.2004.11.6.1295,   PDF Download:

Abstract

Although model checking has gained its popularity as one of the most effective approaches to the formal verification, it has to deal with the state explosion problem to be widely used in industry. In order to mitigate the problem, this paper proposes an abstraction technique to obtain a reduced model M' from a given original model M. Our technique identifies the set of necessary variables for model checking and projects the state space onto them. The abstract model M' is smaller in both size and behavior than the original model M, written M'≤M. Since the result of reachability analysis with M' is preserved in M, we can do reachability analysis with model checking using M' instead of M. The abstraction technique is applied to Push Push games, and two model checkers-Cadence SMV and NuSMV-are used to solve the games. As a result, most of unsolved games with the usual model checking are solved with the abstraction technique. In addition, abstraction shows that there is much of time and space improvement. With Cadence SMV, there is 87% time improvement and 79% space one. And there is 83% time improvement and 56% space one with NuSMV.

Statistics
Cite this article