| 引用本文: | 屈婉霞,李暾,郭阳,等.一种高效的显式模型检验方法.[J].国防科技大学学报,2008,30(4):53-58.[点击复制] |
| QU Wanxia,LI Tun,GUO Yang,et al.An Efficient Explicit Model Checker[J].Journal of National University of Defense Technology,2008,30(4):53-58[点击复制] |
|
| |
|
|
| 本文已被：浏览 6662次 下载 5746次 |
| 一种高效的显式模型检验方法 |
| 屈婉霞, 李暾, 郭阳, 杨晓东 |
|
(国防科技大学 计算机学院，湖南 长沙 410073)
|
| 摘要: |
| 随着软硬件系统规模和功能的不断扩充，状态空间爆炸问题严重影响了模型检验的进一步发展与应用，成为验证大规模系统的瓶颈。在显式模型检验工具Murphi的基础上，针对其可达状态空间组织存在的问题进行改进，提出了基于整型指针与Fibonacci散列的可达状态空间组织方法，实现了一个高效的显式模型检验原型系统，在确保验证正确的同时有效缩短了验证时间，并能在系统规范不可满足的情况下给出反例，有助于系统设计人员快速定位错误。理论分析和实验结果表明了本方法的有效性。 |
| 关键词: 模型检验 显式状态枚举 可达性分析 |
| DOI： |
| 投稿日期：2007-12-13 |
| 基金项目:国家自然科学基金资助项目(60573173，60773025)；新世纪优秀人才支持计划资助项目 |
|
| An Efficient Explicit Model Checker |
| QU Wanxia, LI Tun, GUO Yang, YANG Xiaodong |
|
(College of Computer, National Univ. of Defense Technology, Changsha 410073, China)
|
| Abstract: |
| With the growing increase in software/hardware system scale and function, the further development and application of model checking has been greatly limited by state space explosion, which has been the bottleneck of verifying large industrial designs. Based on the Murphi, an explicit state model checking tool, the problem of organization of reachable state space of model checking was studied, and a novel organization method of reachable state space based on integer pointer and Fibonacci hash was presented. In the approach, an efficient model checking system was suggested. The new approach can effectively shorten verification cycle, and give counter example when the system specification is unsatisfiable. All this greatly helped rapid error location. The analysis and experiment results prove the effectiveness of our method. |
| Keywords: model checking explicit state enumeration reachability analysis |
|
|
|
|
|
