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

An Efficient Explicit Model Checker

作　　者：屈婉霞[1] 李暾[1] 郭阳[1] 杨晓东[1] 

机构地区：[1]国防科技大学计算机学院,湖南长沙410073

出　　处：《国防科技大学学报》2008年第4期53-58,共6页Journal of National University of Defense Technology

基　　金：国家自然科学基金资助项目(60573173;60773025);新世纪优秀人才支持计划资助项目

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

关 键 词：模型检验 显式状态枚举 可达性分析 

分 类 号：TP391.72[自动化与计算机技术—计算机应用技术]