基于启发式on-the-fly的扩展TGBA模型检测算法  

Heuristic on-the-fly Model Checking Algorithm for Extended TGBA

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

机构地区：[1]同济大学电子与信息工程学院,上海201804 [2]江西理工大学信息工程学院,江西赣州341000

出　　处：《计算机学报》2014年第12期2519-2529,共11页Chinese Journal of Computers

基　　金：江西省教育厅科学技术研究项目(GJJ13412;GJJ14429;GJJ13410);国家科技支撑计划重大项目(2009BAG11B00;2011BAG01B03);国家自然科学基金(61462034;61075002;61273180);山东省自然科学基金(ZR2012FL17)资助

摘　　要：以广义Büchi自动机为研究对象,对其作判空检测能为解决系统的状态空间爆炸问题提供有效途径.但广义Büchi自动机难以适用于安全苛求计算机系统中,只需满足某个可接受条件子集便可作出非空性判断,进而能判断出系统的安全性的情形.文中提出了基于启发式on-the-fly的扩展TGBA模型检测算法,该算法采用ETGBA模型,通过启发式on-the-fly判空检测方法对ETGBA作判空检测时,加强了对不能构成其可接受运行的结点的处理,节省了内存空间,提高了检测效率,从而能较快地作出非空性判断.通过算法的正确性证明及复杂度分析、实验比较与实例研究验证了所提出算法的正确性与实际可行性.与已有算法相比,该算法的通用性更强,当应用于广义Büchi自动机的判空检测时,其时空性能均优于已有算法.The key operation of the automata-theoretic approach for model-checking is an emptiness checking algorithm, which can tell whether a finite state system satisfies its properties. Emptiness checking of generalized Btichi automaton can relieve the problem of state space explosion. However, in some safety-critical computer systems, non-emptiness judgment for safety verified model can be made out by strongly connected components which are accessible from initial state and include some subset of acceptance conditions. It is difficult to apply existing emptiness checking algorithms to analyze and verify the safety of safety-critical computer system. In this paper, we propose a heuristic on-the-fly model checking algorithm for ETGBA （extended transition- based generalized Btichi automaton）. The proposed algorithm adopts an extended model structure for transition-based generalized Btichi automaton, based on the algorithm for on-the-fly emptiness checking, it combines heuristic depth first searching with detecting of strongly connected components to compute accepting runs of ETGBA. The correctness and feasibility of our method have been confirmed by theoretical proofs and experimental results. Compared with the traditional methods, the proposed algorithm has better applicability than existing methods, when emptiness checking is used for generalized Btichi automaton, in most cases, the states space explored can be decreased, so the time and memory consumption for system＇s property verification are reduced in our method.

关 键 词：模型检测 广义Btichi自动机 on-the-fly算法 安全性分析 

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