基于矩阵半张量积模型检测算法的研究与实现

发布时间：2017-05-28 12:02

  本文关键词：基于矩阵半张量积模型检测算法的研究与实现，由笔耕文化传播整理发布。

【摘要】：在计算机科学迅猛发展的今天,云计算、物联网、移动互联网成了时代的标志,这些软件技术的高速发展对自身验证的可靠性和硬件性能提出了挑战,对于硬件的性能要求最终落到了硬件集成电路的可靠性上面。然而,在硬件发展的历程中,验证集成芯片的正确性和可靠性一直是一个瓶颈。在验证领域使用最多的是基于模拟的验证方式,这种检验方式存在其不可弥补的缺点,即它只能证明系统有错,而不能证明系统设计的正确性。而在软件方面,对于可靠性的验证还处于没有形成特定规范的阶段。所以无论是针对软件还是硬件,对其可靠性的验证都是有实质意义的。本文主要以半张量积为数学理论,研究一种基于半张量积的模型检测算法。算法主要分为三个部分:被验证系统的数学建模、被验证系统需要满足的属性描述和模型检测算法。针对被验证系统数学建模,首先根据被验证系统的原子集合,固定原子公式顺序,考查原子公式的取值,确定原子公式在系统状态的取值情况,定义系统状态的布尔编码表示。然后使用矩阵半张量积的逻辑抽象方法对系统状态向量化,得到系统的状态向量。根据规定系统状态的顺序,利用图论的邻接矩阵定义被验证系统的结构矩阵。最后使用向量乘法描述系统运行状态,并给出模型检测算法的正确性和有穷性的数学证明。本算法对被检测的属性的描述采用分支时态逻辑的计算树逻辑,因此分析了计算树逻辑(Computation Tree Logic,CTL)的适当集,选取相应的适当集对任意CTL公式进行标准化描述。针对CTL的适当集的原子语义EX、EG和EU分别给出了验证算法描述,再被验证系统需要满足的属性描述对任意CTL公式表示进行属性的复合语义验证算法设计方案。论文最后给出了基于半张量积的模型检测算法的应用实例分析,实现了从属性分析、模型建立到最后的验证,并完成了实例的验证工作。从应用实例表明,本算法不仅可以应用于软件系统和硬件系统的验证,还可以拓展到布尔网络分析等其他研究领域。
【关键词】：形式化验证 Kripke结构 模型检验 验证算法
【学位授予单位】：电子科技大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP302.7
【目录】：

• 摘要5-6
• Abstract6-9
• 第一章 绪论9-14
• 1.1 研究目的和意义9-10
• 1.2 国内外相关研究现状10-12
• 1.3 主要研究内容12-13
• 1.4 章节安排13-14
• 第二章 相关知识背景14-28
• 2.1 集成电路的设计与验证14-22
• 2.1.1 集成电路的设计层次14-17
• 2.1.2 模拟验证和形式化验证17-22
• 2.2 时态逻辑分类22-23
• 2.2.1 线性时态逻辑的表示方法22
• 2.2.2 计算树逻辑的表示和意义22-23
• 2.3 矩阵的半张量积23-27
• 2.3.1 矩阵半张量积的定义23-26
• 2.3.2 半张量积的伪交换性26-27
• 2.4 本章小节27-28
• 第三章 系统建模与结构矩阵求解28-39
• 3.1 系统建模28-33
• 3.1.1 Kripke结构模型28-29
• 3.1.2 布尔逻辑的矩阵表示29-31
• 3.1.3 系统模型的矩阵化31-33
• 3.2 系统结构矩阵定义与求解33-38
• 3.2.1 Kripke状态向量求解方法33-34
• 3.2.2 Kripke结构矩阵快速求解34-38
• 3.3 本章小结38-39
• 第四章 模型检测算法实现39-54
• 4.1 符号模型检测算法39-41
• 4.1.1 符号模型检测标记算法39-40
• 4.1.2 二叉判断图的算法40-41
• 4.2 属性的描述及分析41-44
• 4.2.1 属性描述方法的选取41
• 4.2.2 使用时态逻辑描述规范41-43
• 4.2.3 时态逻辑等价性与规范化43-44
• 4.3 模型检测算法的数学论证44-48
• 4.3.1 模型状态转移的实现44-46
• 4.3.2 n步转移关系的表示46-48
• 4.3.3 Kripke结构网络直径和意义48
• 4.4 基于半张量积的验证算法48-53
• 4.4.1 EX的设计与实现48-50
• 4.4.2 EG的设计与实现50-51
• 4.4.3 EU的设计与实现51-52
• 4.4.4 属性的复合验证设计与实现52-53
• 4.5 本章小结53-54
• 第五章 模型检测算法应用实例分析54-71
• 5.1 系统的验证实例分析54-60
• 5.1.1 例子分析54
• 5.1.2 属性的分析和描述54-56
• 5.1.3 建立模型与求解56-58
• 5.1.4 验证过程实现58-59
• 5.1.5 试验环境与数据结果59-60
• 5.2 模型检测算法的扩展应用分析60-69
• 5.2.1 布尔网络传统的矩阵形式60-63
• 5.2.2 布尔网络结构矩阵的新求法63-65
• 5.2.3 布尔网络与kripke的关系65-67
• 5.2.4 用新方法求解布尔网络拓扑问题67-69
• 5.3 本章小结69-71
• 第六章 总结与展望71-73
• 6.1 全文总结71
• 6.2 下一步工作及展望71-73
• 致谢73-74
• 参考文献74-77
• 攻读硕士学位期间取得的成果77-78

【相似文献】

中国期刊全文数据库 前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];贵州大学;2008年

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

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

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

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

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

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

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

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

10 刘金卓;基于符号化模型检测的软件演化过程模型验证[D];云南大学;2013年

中国硕士学位论文全文数据库 前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年

  本文关键词：基于矩阵半张量积模型检测算法的研究与实现，由笔耕文化传播整理发布。

，

本文编号：402565