关键词: 形式化方法，模型检测，状态空间爆炸，状态和内存管理

Abstract: Abstract The model checking is one of main formalization methods. However there is the problem about state explosion and insufficient memory, which is bottleneck of verification of large scale systems. hhough many researchers have done amount of work, the problem has not been settled well yet. The paper, based on the investigation of the management for fixed memory and state, presented a new approach of model checking, which avoids the problem that model checking can not proceed because of insufficient memory.

Key words: Formal method, Model checking, State explosion, Management of state and memory