| 基于SPIN的模块化模型检测方法研究 |
| |
| 引用本文： | 李兴锋, 张新常, 杨美红, 阎保平. 基于SPIN的模块化模型检测方法研究[J]. 电子与信息学报, 2011, 33(4): 902-907. doi: 10.3724/SP.J.1146.2010.00751 |
| |
| 作者姓名： | 李兴锋 张新常 杨美红 阎保平 |
| |
| 作者单位： | 中国科学院计算机网络信息中心;山东省科学院计算中心;山东省计算机网络重点实验室; |
| |
| 基金项目： | 国家973计划项目(2009CB320502); 国家自然科学基金(61070039); 国家863计划项目(2009AA01Z145); 山东省科学院院博士基金(2010-12)资助课题 |
| |
| 摘 要： | 该文针对模型检测过程中所存在的状态爆炸问题，提出了一种基于模型检测工具SPIN的模块化模型检测方法。所提出的方法能够将指定的抽象模型分解成若干的模块，并对这些验证复杂度相对低的模块执行模型检测，以替代对原模型的模型检测。所提方法所用的分解过程保留了原模型所有的语义，同时不增加额外的语义，从而使得验证所有模块等同于验证原模型。理论和实验分析结果显示了所提方法的有效性。
|
| 关 键 词： | 模型检测 扩展有限状态自动机 状态爆炸 |
| 收稿时间： | 2010-07-15 |
| 修稿时间： | 2010-11-02 |
Study on Modularized Model Checking Method Based on SPIN |
| |
| Li Xing-Feng, Zhang Xin-Chang, Yang Mei-Hong, Yan Bao-Ping. Study on Modularized Model Checking Method Based on SPIN[J]. Journal of Electronics & Information Technology, 2011, 33(4): 902-907. doi: 10.3724/SP.J.1146.2010.00751 |
| |
| Authors: | Li Xing-feng Zhang Xin-chang Yang Mei-hong Yan Bao-ping |
| |
| Abstract: | To address the state explosion problem in the procedure of model checking,this paper proposes a SPIN-based modularized model checking method.The proposed method divides the original abstraction model into some modules,and verifies all the divided modules,instead of verifying the original model.In the dividing process,the semantic of original model can be completely included in the modules,and no semantic is added in the process.Consequently,the original model passes the verification of model checking if and... |
| |
| Keywords: | Model checking Extended Finite State Machine(EFSM) State explosion |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《电子与信息学报》浏览原始摘要信息 |
|
点击此处可从《电子与信息学报》下载全文 |
