期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

模型检测技术的发展研究

原文传递
导出
摘要 模型检测(model checking)是一种能够自动验证有限状态并发系统的技术。该文从模型检测技术的背景入手,先阐述了模型检测技术基本原理及其相关过程。而后介绍了阻碍模型检测技术发展的状态爆炸问题,再者对Nu SMV、SPIN和UPPAAL等模型检测工具进行了介绍与比较。最后总结了模型检测技术在新的领域、工具研制、算法研究和与其他技术相结合等几个方面的研究进展,可为今后进一步对计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中提供借鉴。
作者 杨茜茜
机构地区 西南交通大学
出处 《科学家》 2016年第10期19-19,22,共2页 Scientist
关键词 模型检测技术 形式化验证 状态爆炸 状态约简 研究进展
分类号 TP311.53 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献1

二级参考文献20

  • 1Clarke E M, Emerson E A, Sistla A P. Automatic verifi- cation of finite - state concurrent systems using temporal logic specifications [ J ]. ACM Transactions on Program- ming Languages and Systems ( TOPLAS ), 1986, 8 ( 2 ) : 244 - 263. 被引量：1
  • 2Clarke Edmund M. The Birth of Model Checking [ A ]. Symposium 25 Years of Model Checking [ C ]. Berlin : Springer Heidelberg, 2008 : 1 - 26. 被引量：1
  • 3Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: 1020 states and beyond[ J]. Information and computation, 1992, 98(2) : 142 - 170. 被引量：1
  • 4Bryant R E. Graph- based algorithms for Boolean func- tion manipulation [ J ]. IEEE Transactions on Computers, 1986, 100(8) : 677 -691. 被引量：1
  • 5Clarke E M, Grumberg O,Peled D. Model Checking[ M ]. Cambridge : The MIT Press, 1999 : 1 - 201. 被引量：1
  • 6Clarke E M, Grumberg O, Long D E. Model checking and abstraction [ J ]. ACM Transactions on Programming Languages and Systems (TOPLAS) , 1994, 16(5): 1512 - 1542. 被引量：1
  • 7Holzmann G J. The model checker SPIN [ J ]. IEEE Trans- actions on Software Engineering, 1997, 23 ( 5 ) : 279 - 295. 被引量：1
  • 8Cimatti A, Clarke E, Giunchiglia F, et al. NuSMV: a new symbolic model checker[ J]. International Journal on Software Tools for Technology Transfer, 2000, 2(4) : 410 - 425. 被引量：1
  • 9Bengtsson J, Larsen K, Larsson F, et al. UPPAAL-a tool suite for automatic verification of real - time systems [ M ]. Springer Berlin Heidelberg, 1996 : 1 - 204. 被引量：1
  • 10Sun J, Liu Y, Dong J S, et al. PAT: Towards flexible verification under fairness [ A 1. Computer Aided Verifica- tion Springer Berlin Heidelberg, 2009:709 -714. 被引量：1

共引文献3

科学家
2016年 第10期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部