基于行为时序逻辑模型检测的研究与应用

发布时间：2021-09-07 12:08

　　模型检测是一种基于形式化方法的自动分析和验证技术,问题的关键是状态空间爆炸的解决。Lesilie Lamport提出行为时序逻辑（TLA）理论体系,运用TLA对软件或协议进行建模,它能在一种语言中同时表达程序与属性,在理论和实际应用中,这种模型检测技术具有一定研究价值。本文在详细介绍行为时序逻辑基本概念的基础上,分析了使用行为时序逻辑基本理论对并发系统的建模,运用TLA+规约语言与检测工具对并发系统和网络安全协议进行简要分析与检测,所作的主要工作与创新之处如下:1、在行为时序逻辑（Temporal Logic of Action）的基础上严格定义了行为路径对行动的强弱公平性,并详细证明了并发系统中行为对行动的强弱公平性,介绍TLA语法与语义,并分析TLA的逻辑推理规则,以简单程序实例分析和证明并发系统所具有的不变性,对程序的不同TLA时序公式之间等价性进行分析;2、TLA+是基于TLA的描述并发系统的规约语言,阐述了使用TLA+语言描述并发系统的规约方法,分析检测工具TLC的结构组成、各命令参数的功能及检测原理及要求,研究了协议的分析、建模及检测流程;3、基于TLA的网络协议与并发系统... 

【文章来源】：贵州大学贵州省 211工程院校

【文章页数】：68 页

【学位级别】：硕士

【部分图文】：

图4一1时钟系统检测

用Generato:进行随机模拟。在dos命令符下键入 javatle.GeneratorHourCloek.tla，运行类Generator模块，如下图是简单的时钊，规约系统检测:图4一1时钟系统检测结果显示:没有检测出错误，生成24个状态，12个可区分状态，计算状态深度为1。对时钟系统描述文件进行随机模拟，dos命令符下键入 javatlc.GeneratorHourCloek.tla，运行类Generator模块，如下图所示:图4一2时序系统随机模拟生成默认十条状态数为10的运行轨迹文件，其中两条轨迹分别如下所示: HourCloekZtraeel:图4一3时序系统轨迹(l)

用Generato:进行随机模拟。在dos命令符下键入 javatle.GeneratorHourCloek.tla，运行类Generator模块，如下图是简单的时钊，规约系统检测:图4一1时钟系统检测结果显示:没有检测出错误，生成24个状态，12个可区分状态，计算状态深度为1。对时钟系统描述文件进行随机模拟，dos命令符下键入 javatlc.GeneratorHourCloek.tla，运行类Generator模块，如下图所示:图4一2时序系统随机模拟生成默认十条状态数为10的运行轨迹文件，其中两条轨迹分别如下所示: HourCloekZtraeel:图4一3时序系统轨迹(l)

【参考文献】：
期刊论文
[1]安全协议形式化混合分析技术的研究与应用[J]. 付宇,马自堂,王惠芳.  计算机工程. 2006(17)
[2]基于SMV的网络协议形式化分析与验证[J]. 文静华,余滨,张梅,李祥.  计算机工程. 2006(15)
[3]基于TLA+的BRP协议规约及验证[J]. 陈立前,王戟,陈火旺.  计算机工程与科学. 2006(01)
[4]密码协议的Promela语言建模及分析[J]. 龙士工,王巧丽,李祥.  计算机应用. 2005(07)
[5]一种电子商务协议原子性的模型检验分析方法[J]. 董荣胜,郭云川,古天龙.  计算机科学. 2005(04)
[6]密码协议的符号模型检测及分析[J]. 龙士工,罗文俊,李祥.  计算机应用. 2005(01)
[7]基于有穷自动机模型的电子商务支付协议公平性研究[J]. 谢晓尧,张焕国.  计算机应用. 2004(06)
[8]模型检测:理论、方法与应用[J]. 林惠民,张文辉.  电子学报. 2002(S1)
[9]基于时序逻辑的加密协议分析[J]. 肖德琴,周权,张焕国,刘才兴.  计算机学报. 2002(10)
[10]Needham-Schroeder公钥协议的模型检测分析[J]. 张玉清,王磊,肖国镇,吴建平.  软件学报. 2000(10)

博士论文
[1]界程演算模型检测[D]. 江华.贵州大学 2008

硕士论文
[1]SPIN模型检测的研究与应用[D]. 王巧丽.贵州大学 2006



本文编号：3389521