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

A Novel Model Checking Algorithm Based on Heuristic NDFS

作　　者：王曦[1] 徐中伟[1] 

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

出　　处：《小型微型计算机系统》2012年第8期1740-1746,共7页Journal of Chinese Computer Systems

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

摘　　要：以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法.This paper proposed a novel model checking algorithm based on heuristic nested depth-first searches for generalized büchi automata.It is combined on-the-fly algorithm with heuristic nested depth first search to compute accepting runs of generalized büchi automata,which is transition-based generalized büchi automaton with multiple acceptance conditions.The proposed algorithm is correct and feasible by proving from theory and experiments.Compared to the traditional ways,while transition-based generalized Büchi automaton is not empty,our new method can decrease the states space to be explored for generalized büchi automata′s emptiness checking and decline the time for system′s property verification,besides,it can product corresponding counterexample for system model′s safety verification.It is a kind of effectual method to relieve the problem for state space explosion of formal verification methods,and it is a feasible and novel method for safety verification of safety critical system.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]