一种高效的显式模型检验方法

• 作者: 屈婉霞 李暾 杨晓东 郭阳
• 来源期刊: 国防科技大学学报
• 学科: 工学
• 关键词: 模型检验 显式状态枚举 可达性分析
• 年，卷（期）: 2008,（4）
• 所属期刊栏目: 电子工程·计算机工程
• 页码范围: 53-58
• 页数: 6页
• 分类号: TP391.72
• 字数: 4436字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2486.2008.04.011

摘要

随着软硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.在显式模型检验工具Murphi的基础上,针对其可达状态空间组织存在的问题进行改进,提出了基于整型指针与Fibonacci散列的可达状态空间组织方法,实现了一个高效的显式模型检验原型系统,在确保验证正确的同时有效缩短了验证时间,并能在系统规范不可满足的情况下给出反例,有助于系统设计人员快速定位错误.理论分析和实验结果表明了本方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭阳	国防科技大学计算机学院	50	449	9.0	20.0
2	李暾	国防科技大学计算机学院	19	186	5.0	13.0
3	杨晓东	国防科技大学计算机学院	23	82	5.0	8.0
4	屈婉霞	国防科技大学计算机学院	11	25	3.0	4.0