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

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