文献类型：期刊文章

作　　者：李兴锋[1] 张新常[2,3] 杨美红[2,3] 阎保平[1]

机构地区：[1]中国科学院计算机网络信息中心,北京100190 [2]山东省科学院计算中心,济南250014 [3]山东省计算机网络重点实验室,济南250014

出　　处：《电子与信息学报》

基　　金：国家973计划项目(2009CB320502);国家自然科学基金(61070039);国家863计划项目(2009AA01Z145);山东省科学院院博士基金(2010-12)资助课题

年　　份：2011

卷　　号：33

期　　号：4

起止页码：902-907

语　　种：中文

收录情况：BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI、IC、JST、RCCSE、SCOPUS、WOS、ZGKJHX、核心刊

摘　　要：该文针对模型检测过程中所存在的状态爆炸问题,提出了一种基于模型检测工具SPIN的模块化模型检测方法。所提出的方法能够将指定的抽象模型分解成若干的模块,并对这些验证复杂度相对低的模块执行模型检测,以替代对原模型的模型检测。所提方法所用的分解过程保留了原模型所有的语义,同时不增加额外的语义,从而使得验证所有模块等同于验证原模型。理论和实验分析结果显示了所提方法的有效性。

关 键 词：模型检测  扩展有限状态自动机  状态爆炸  

分 类 号：TP393]