摘要:该文针对模型检测过程中所存在的状态爆炸问题,提出了一种基于模型检测工具SPIN的模块化模型检测方法。所提出的方法能够将指定的抽象模型分解成若干的模块,并对这些验证复杂度相对低的模块执行模型检测,以替代对原模型的模型检测。所提方法所用的分解过程保留了原模型所有的语义,同时不增加额外的语义,从而使得验证所有模块等同于验证原模型。理论和实验分析结果显示了所提方法的有效性。
关键词:模型检测 扩展有限状态自动机 状态爆炸
单位:中国科学院计算机网络信息中心 北京100190 山东省科学院计算中心 济南250014 山东省计算机网络重点实验室 济南250014
注:因版权方要求,不能公开全文,如需全文,请咨询杂志社