Abstract: This paper reviewed some prevalent trends in this domain in recent years, then proposed a software model checking scenario, which was based on hierarchical unit partition and heuristic search. It has three phases, which are preprocess, unit partition and state space search. There is on-the-fly method in this scenario to improve the performance of model checking. Experiments prove that this model checking scenario works well on solving state explosion problem.

Key words: Software Model Checking, Hierarchical unit partition, Heuristic search

摘要： 通过对近年来软件模型检测领域流行的几种技术进行综述，提出了一种基于层次单元划分，使用引导式搜索方式的软件模型检测方案。本方案分为预处理、单元划分、状态空间搜索三个阶段，其中使用on-the-fly技术提高了搜索性能。实验证明，该方案在解决状态爆炸问题上有较好的效果。

关键词: 软件模型检测, 层次单元划分, 引导式搜索