基于时序逻辑的定量模型检测算法研究

发布时间：2021-07-08 05:33

　　随着软硬件系统的日益复杂,保证系统的安全性至关重要。模型检测是自动验证系统正确性的有效技术,目前已经广泛应用于计算机软硬件系统,通信协议,安全协议等方面的分析与验证中。针对包含非确定性信息、不完备信息的并发系统的形式化验证问题,本文研究了两种定量模型检测算法。（1）基于可能性理论,模糊逻辑等理论,研究了基于广义可能性决策过程的μ-演算模型检测算法。首先引入广义可能性决策过程作为系统模型,接着对经典的命题μ-演算进行改进和扩展,给出广义可能性μ-演算的概念,用于描述非确定系统的属性特征。然后提出广义可能性μ-演算模型检测算法,并将模型检测问题简化为模糊矩阵运算,最后通过具体的实例进行了分析与验证。与经典的μ-演算相比,广义可能性μ-演算具有更强的表达力,能够刻画不确定系统的属性特征,模型检测算法能够给出系统满足属性的可能性程度,研究成果扩大了广义可能性测度在模型检测中的应用范围。（2）在格理论,多值逻辑的基础上,研究了基于多值Kripke结构的多值μ-演算模型检测算法,将多值Kripke结构作为系统模型,对经典μ-演算语言进行扩展,用于描述多值系统的属性,提出了多值μ-演算模型检测算法,... 

【文章来源】：北方民族大学宁夏回族自治区

【文章页数】：60 页

【学位级别】：硕士

【部分图文】：

多值模型检测器Chek的图形界面

【参考文献】：
期刊论文
[1]具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 袁申,魏杰林,李永明.  计算机工程与科学. 2019(01)
[2]形式化方法概貌[J]. 王戟,詹乃军,冯新宇,刘志明.  软件学报. 2019(01)
[3]可能性测度下的CTL符号化模型检测[J]. 雷丽晖,郭越,张延波.  计算机工程与科学. 2018(11)
[4]具有DP的广义可能性模糊时态CTL模型检测[J]. 魏杰林,袁申,李永明,梁常建.  计算机科学与探索. 2019(10)
[5]不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 范艳焕,李永明,潘海玉.  电子学报. 2018(01)
[6]具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 梁常建,李永明.  电子学报. 2017(12)
[7]广义可能性计算树逻辑的模型检测问题[J]. 梁常建,李永明.  电子学报. 2017(11)
[8]基于决策过程的广义可能性计算树逻辑模型检测[J]. 马占有,李永明.  中国科学:信息科学. 2016(11)
[9]广义可能性决策过程的计算树逻辑模型检测[J]. 马占有,李永明.  计算机工程与科学. 2015(11)
[10]随机模型检验研究[J]. 刘阳,李宣东,马艳,王林章.  计算机学报. 2015(11)

博士论文
[1]基于决策过程的广义可能性时态逻辑模型检测[D]. 马占有.陕西师范大学 2017
[2]状态转换系统的格值量化验证方法研究[D]. 潘海玉.华东师范大学 2012

硕士论文
[1]可能性测度下并发系统的符号化模型检测研究与实现[D]. 张延波.陕西师范大学 2018
[2]基于μ演算的认知难题符号化模型检测[D]. 杨志刚.华侨大学 2017
[3]基于可能性测度的计算树逻辑和Kripke结构决策过程[D]. 薛艳.陕西师范大学 2012



本文编号：3270958