基于层次单元划分的软件模型检测技术  

Software model checking based on hierarchical unit partition

作　　者：陈晨[1] 陈永生[1] 

机构地区：[1]同济大学电子与信息工程学院,上海201804

出　　处：《计算机应用》2008年第8期2109-2112,共4页journal of Computer Applications

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]