基于启发式NDFS的模型检测新算法

摘要：

以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法.

关键词：模型检测、启发式NDFS、安全性验证、on-the-fly算法、Büchi自动机

所属期刊栏目：33

分类号：TP301(计算技术、计算机技术)

资助基金：国家科技支撑计划重大项目2009BAG11B00,2011BAG01B03;国家自然科学基金项目60674004,61075002

在线出版日期：2012-11-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1740-1746