基于SPIN的模块化模型检测方法研究

• 作者: 张新常 李兴锋 杨美红 阎保平
• 来源期刊: 电子与信息学报
• 学科: 工学
• 关键词: 模型检测 扩展有限状态自动机 状态爆炸
• 年，卷（期）: 2011,（4）
• 所属期刊栏目: 论文
• 页码范围: 902-907
• 分类号: TP393
• 字数: 6230字
• 语种: 中文
• DOI: 10.3724/SP.J.1146.2010.00751

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	阎保平	中国科学院计算机网络信息中心	162	2464	23.0	43.0
2	杨美红	山东省科学院计算中心	8	60	5.0	7.0
4	李兴锋	中国科学院计算机网络信息中心	1	18	1.0	1.0
5	张新常	山东省科学院计算中心	2	23	2.0	2.0