基于多值可能性的模型检测器MvChecker的设计与实现

发布时间：2021-03-21 21:27

　　现代计算机技术已经时时刻刻伴随着我们的生活,随着现代计算机软件和硬件的设计越来越复杂,对软件和硬件的测试也变得越来越复杂,不仅需要消耗大量的人力物力成本,而且使用传统的检测技术也有一定的局限性,对于生活中真实存在的一些不确定性因素,存在着一定的检测缺陷,从而导致检测失败。1981年,Clarke和Emerson以及Quielle和Sifakis提出了模型检测的理论,作为一种形式化的自动验证技术,为我们解决这些检测问题提供了一个很好的解决方案。对比传统的检测技术,模型检测技术有着一系列的优势,比如可以在系统实现之前对系统进行验证,提前发现问题,节约检测成本等等,这些检测一般会使用基于模型检测理论实现的模型检测器去进行验证,传统的模型检测器大多是基于一些经典的理论而实现的,随着我们研究的深入,我们发现现实生活中有着大量的不确定信息,这样使用传统理论实现的模型检测器无法解决这些问题。而多值模型检测理论的出现,利用在格上构建不确定信息,结合多值计算树逻辑,通过构建的多值可能性Kripke结构模型,有效的解决了这些问题。同时为了实现模型检测技术的自动化验证的特性的优势,本文基于多值可能性的多值计... 

【文章来源】：陕西师范大学陕西省 211工程院校 教育部直属院校

【文章页数】：58 页

【学位级别】：硕士

【部分图文】：

图２．１模型检测流程图??Ｆｉｇ．?２．１?Ｍｏｄｅｌ?Ｃｈｅｃｋｉｎｇ?Ｆｌｏｗ?Ｃｈａｒｔ??

图２．２?—个简单Ｋｒｉｐｋｅ结构??Ｆｉｇ．?２．２?Ａ?Ｓｉｍｐｌｅ?Ｋｒｉｐｋｅ?Ｓｔｒｕｃｔｕｒｅ??．［ｕ］

图３．１?—个简单多值Ｋｒｉｐｋｅ结构??

【参考文献】：
期刊论文
[1]不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 范艳焕,李永明,潘海玉.  电子学报. 2018(01)
[2]基于决策过程的广义可能性计算树逻辑模型检测[J]. 马占有,李永明.  中国科学:信息科学. 2016(11)
[3]随机模型检验研究[J]. 刘阳,李宣东,马艳,王林章.  计算机学报. 2015(11)
[4]可能LTL模型检测的两种方法[J]. 李永明.  陕西师范大学学报(自然科学版). 2014(06)
[5]可能性测度下计算树逻辑的若干性质[J]. 李亚利,李永明.  陕西师范大学学报(自然科学版). 2013(06)
[6]基于可能性测度的计算树逻辑CTL*与可能性互模拟[J]. 邓辉,薛艳,李亚利,李永明.  计算机科学. 2012(10)
[7]概率计算树逻辑的限界模型检测[J]. 周从华,刘志锋,王昌达.  软件学报. 2012(07)
[8]基于可能性测度的计算树逻辑[J]. 薛艳,雷红轩,李永明.  计算机工程与科学. 2011(09)
[9]使用局部建模的微处理器测试程序自动生成方法[J]. 张良,易江芳,佟冬,程旭,王克义.  电子学报. 2011(07)
[10]龙芯2号微处理器浮点除法功能部件的形式验证[J]. 陈云霁,马麟,沈海华,胡伟武.  计算机研究与发展. 2006(10)



本文编号：3093567