一种高效的显式模型检验方法
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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


An Efficient Explicit Model Checker
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

屈婉霞,李暾,郭阳,等.一种高效的显式模型检验方法[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.

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2007-12-13
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2012-12-07
  • 出版日期:
文章二维码