基于μ-演算的局部模型检测算法设计
发布时间：2017-06-26 18:02
本文关键词：基于μ-演算的局部模型检测算法设计，，由笔耕文化传播整理发布。
【摘要】：随着计算机软件系统、硬件系统的发展,系统也变得越来越复杂,因此设法保证系统的正确性和可靠性变得越来越重要。为此,许多学者投入到该问题的研究中,并提出了很多理论与方法,模型检测因高度自动化而引起了学者的关注。模型检测是一种形式化验证技术。其过程就是通过对系统建立模型,然后验证该模型是否满足给定的性质。在模型检测常用的逻辑中,命题μ-演算吸引了很多学者的兴趣,它是由Kozen提出的,是个表达能力很强的逻辑语言,其较强的表达能力主要来自于最大不动点算子和最小不动点算子的交替嵌套。由于命题μ-演算有着较强的表达能力,因此其它一些逻辑验证都可以转换为命题μ-演算来验证,而且验证效率也较高。模型检测需要对系统状态空间进行穷举搜索,验证并发系统时,其状态数是呈指数增长的。目前已经有许多关于命题μ-演算的模型检测算法,这些算法可以分为全局模型检测算法和局部模型检测算法。对于命题μ-演算,目前已知的最好的局部模型检测算法的时间复杂度与交替嵌套深度d呈指数关系,其复杂度较高,本文将对其不动点交替嵌套迭代过程进行分析,提出时间复杂度较低的局部模型检测算法。本文从命题μ-演算出发,研究不动点交替嵌套迭代的中间结果之间的偏序关系,设计高效的局部模型检测算法,并对算法的复杂度进行研究分析。本文主要分为三个部分:第一部分主要分析基于命题μ-演算的局部模型检测算法,对其不动点交替嵌套迭代过程进行分析,然后从三支决策的角度改进算法。第二部分主要分析不动点交替嵌套迭代过程的中间结果之间的一组偏序关系,并根据该关系设计了一个局部模型检测算法。第三部分主要开发设计了模型检测器MuFPAL-MC的词法语法分析器模块,并阐述了模型检测器MuFPAL-MC的研究框架。
【关键词】：局部模型检测 命题μ-演算 复杂度 不动点
【学位授予单位】：闽南师范大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：O141.1
【目录】：
- 摘要5-6
- Abstract6-10
- 第1章 绪论10-18
- 1.1 研究背景及意义10-13
- 1.2 国内外研究现状13-15
- 1.3 主要工作和结构安排15-18
- 1.3.1 主要工作16
- 1.3.2 结构安排16-18
- 第2章 基础知识18-26
- 2.1 命题 μ-演算18-20
- 2.2 分区依赖图20-21
- 2.3 界程演算21-23
- 2.4 界程逻辑23-25
- 2.5 三支决策25-26
- 第3章 三支决策视角的局部模型检测26-36
- 3.1 m -演算局部模型检测过程分析26-30
- 3.2 三支决策视角的模型检测算法30-32
- 3.3 算法的对比分析32-34
- 3.4 本章小结34-36
- 第4章 基于一组偏序关系的局部模型检测36-50
- 4.1 算法分析36-43
- 4.2 算法设计43-45
- 4.3 复杂度分析45-49
- 4.3.1 时间复杂度45-48
- 4.3.2 空间复杂度48
- 4.3.3 复杂度对比48-49
- 4.4 本章小结49-50
- 第5章 模型检测器MuFPAL-MC的词法语法分析器的开发设计50-66
- 5.1 MuFPAL-MC模型检测器概述50-58
- 5.1.1 需求分析50-53
- 5.1.2 总体结构53-54
- 5.1.3 界程演算的描述方式54-55
- 5.1.4 界程逻辑公式的描述方式55-57
- 5.1.5 系统内部模块57-58
- 5.2 词法分析器58-60
- 5.3 语法分析器60-62
- 5.4 简单实例测试62-63
- 5.5 本章小结63-66
- 第6章 总结和展望66-68
- 6.1 总结66
- 6.2 展望66-68
- 参考文献68-78
- 致谢78-80
- 第I条 攻读学位期间取得的科研成果80
【相似文献】
中国期刊全文数据库 前10条
1 陈清亮;朱可宜;;多智能体协同的认知规范模型检测算法[J];中山大学学报(自然科学版);2009年01期
2 周从华;邢支虎;刘志锋;王昌达;;马尔可夫决策过程的限界模型检测[J];计算机学报;2013年12期
3 吉猛;胡克瑾;;基于模型检测的电子商务鉴证技术[J];陕西师范大学学报(自然科学版);2006年04期
4 宁正元;胡山立;赖贤伟;;交互时态信念逻辑及其模型检测[J];南京大学学报(自然科学版);2008年02期
5 王曦;徐中伟;梅萌;;基于模型检测的软件安全性验证方法[J];武汉大学学报(理学版);2010年02期
6 王晶;张广泉;;基于概率时间自动机的模型检测反例表示研究[J];苏州大学学报(自然科学版);2011年02期
7 高妍妍;李曦;周学海;;L4进程间通信机制的模型检测方法[J];中国科学院研究生院学报;2011年06期
8 王扣武;张s
本文编号：487032
本文链接：https://www.wllwen.com/kejilunwen/yysx/487032.html
