计算机系统形式化验证中的模型检测方法综述

发布时间：2018-05-28 21:25

  本文选题：形式化方法 + 形式化验证　； 参考：《军事通信技术》2016年02期

【摘要】：随着计算机系统的功能日益强大,对其进行功能和正确性测试与验证的复杂度也越来越大。形式化方法作为对计算机系统进行描述与验证的重要途径,得到学术界普遍的关注与认可。文章主要介绍形式化方法,详细介绍模型检测的检测原理及其主要技术,介绍了几种典型的模型检测工具,并对它们的性能进行比较,同时研究了模型检测中普遍存在的状态爆炸问题及缩减状态方法,最后介绍模型检测的新进展。文章可为模型检测方法研究提供参考和理论支撑。
[Abstract]:With the increasingly powerful functions of computer systems, the complexity of testing and verifying their functions and correctness is increasing. As an important way to describe and verify computer systems, formal methods have received widespread attention and recognition in academic circles. This paper mainly introduces the formal method, introduces the detection principle and main technology of model checking in detail, introduces several typical model checking tools, and compares their performance. At the same time, the problem of state explosion and the method of state reduction are studied. Finally, the new progress of model detection is introduced. This paper can provide reference and theoretical support for the research of model detection method.
【作者单位】： 解放军理工大学指挥信息系统学院研究生1队;解放军理工大学指挥信息系统学院;
【分类号】：TP302.7

【相似文献】

相关期刊论文 前10条

1 戎玫;张广泉;;模型检测新技术研究[J];计算机科学;2003年05期

2 肖健宇;张德运;郑卫斌;;过程提取用于改善程序模型检测的可伸缩性[J];西安交通大学学报;2006年06期

3 袁志斌;徐正权;王能超;;软件模型检测中的抽象[J];计算机科学;2006年07期

4 刘吉锋;孙吉贵;;基于抽象-验证-细化范例的软件模型检测[J];计算机科学;2006年12期

5 化志章;吴传孙;揭安全;薛锦云;;软件模型检测新技术研究[J];微计算机信息;2007年36期

6 王飞明;胡元闯;董荣胜;;模型检测研究进展[J];广西科学院学报;2008年04期

7 邝宏斌;罗贵明;;并行软件模型检测[J];计算机工程;2008年19期

8 何恺铎;顾明;宋晓宇;李力;李江;;面向源代码的软件模型检测及其实现[J];计算机科学;2009年01期

9 林璇;;模型检测方法在入侵检测中的应用研究[J];现代计算机(专业版);2009年02期

10 顾滨兵;;一种软件模型检测方法及其原型系统[J];微计算机应用;2010年11期

相关会议论文 前5条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

相关博士学位论文 前10条

1 奚琪;基于模型检测的二进制代码恶意行为识别技术研究[D];解放军信息工程大学;2014年

2 江华;界程演算模型检测[D];贵州大学;2008年

3 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

4 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

5 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

6 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

7 尹良泽;基于SAT的组合迁移系统模型检测技术研究[D];清华大学;2014年

8 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

9 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

10 黄宏涛;基于懒惰切片的模型检测技术研究[D];哈尔滨工程大学;2012年

相关硕士学位论文 前10条

1 李永亮;基于DNA计算的CTL模型检测方法研究[D];郑州大学;2015年

2 杨树峰;基于统计模型检测的无线传感器网络协议建模与分析[D];郑州大学;2015年

3 张兴兴;基于广义可能性测度的互模拟及CTL不动点语义[D];陕西师范大学;2015年

4 王彬;基于多值模型检测的SaaS应用测试及其自动化研究[D];陕西师范大学;2015年

5 王凯;基于模型检测多反例对软件进行调试[D];电子科技大学;2015年

6 邓楠轶;基于广义可能性测度的模型检测器GPoCheck的设计与实现[D];陕西师范大学;2015年

7 张恒;多值模型检测器的研究与实现[D];陕西师范大学;2015年

8 高毅;不同模型检测下信号并串转换模块功能建模的研究[D];电子科技大学;2014年

9 崔晓爽;基于GSTE模型检测的信号并串转换模块功能验证的研究[D];电子科技大学;2014年

10 许落汀;基于BDDs的离散实时时态逻辑RTCTL*的符号化模型检测及证据生成[D];华侨大学;2015年

，

本文编号：1948245