| 一种高效的显式模型检验方法 |
| |
| 作者姓名： | 屈婉霞 李暾 郭阳 杨晓东 |
| |
| 作者单位： | 国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073;国防科技大学,计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金,教育部跨世纪优秀人才培养计划 |
| |
| 摘 要： | 随着软硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.在显式模型检验工具Murphi的基础上,针对其可达状态空间组织存在的问题进行改进,提出了基于整型指针与Fibonacci散列的可达状态空间组织方法,实现了一个高效的显式模型检验原型系统,在确保验证正确的同时有效缩短了验证时间,并能在系统规范不可满足的情况下给出反例,有助于系统设计人员快速定位错误.理论分析和实验结果表明了本方法的有效性.
|
| 关 键 词： | 模型检验 显式状态枚举 可达性分析 |
| 收稿时间： | 2007-12-13 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载全文 |
|
