基于行为时序逻辑TLA的网络协议的描述与验证

发布时间：2017-05-12 03:13

  本文关键词：基于行为时序逻辑TLA的网络协议的描述与验证，由笔耕文化传播整理发布。

【摘要】：形式化验证方法(Formal Verification Method)是对软硬件系统进行分析和验证一种有效的方式。而模型检测(Model Checking)技术是其中一种很重要的有限状态系统自动验证技术,因其简洁和自动化程度高的特征而备受关注。它主要用于分析验证安全认证协议、通信协议、硬件检测、控制系统等方面。模型检测(Model Checking)是一种近年来比较流行的形式化验证方法。目前有基于一阶逻辑、高阶逻辑、时态逻辑、自动机、状态机等模型检测技术。行为时序逻辑TLA(Temporal Logic of Actions)是由Leslie Lamport提出的一种新的逻辑,行为时序逻辑可以在一个程序中同时表达系统模型及系统属性,使得系统形式化更为有效。目前,基于行为时序逻辑的模型检测技术也是模型检测的主流技术之一。它通过公式的形式在一种逻辑下同时表达系统模型与属性。同时它具有自己的时序规约描述语言TLA+和对应的模型检测工具TLC方便对用TLA+描述的并发系统模型进行检测。因此,这种模型检测技术具有重要的研究和利用价值。本文深入研究了模型检测技术、自动机理论和行为时序逻辑TLA,行为时序逻辑的语言TLA+以及它的验证工具TLC的结构及使用方法.在详细介绍网络协议Pastry及其工作原理的基础上,用TLA+对Pastry协议进行了分析建模同时用TLC进行了验证分析,所作的主要工作与创新之处如下:(1)深入研究行为时序逻辑TLA,及其形式化语言TLA+,自动验证工具TLC;(2)选取网络协议pastry,并对其原理及其行为进行了详细研究,分析了Join工作机制。(3)用TLA+语言对pastry协议进行建模及规约描述,通过TLC模型检测工具对规约的系统进行验证。
【关键词】：网络协议 pastry协议 模型检测 TLA TLA+ TLC
【学位授予单位】：贵州大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP306
【目录】：

• 摘要5-6
• ABSTRACT6-8
• 第一章 引言8-12
• 1.1 研究背景及意义8-9
• 1.2 国内外研究现状及存在的问题9-10
• 1.3 论文的主要研究工作及创新10
• 1.4 论文的结构安排10-12
• 第二章 模型检测与自动机理论12-25
• 2.1 形式化方法及模型检测概述12-13
• 2.2 形式化方法过程13-14
• 2.3 自动机理论14-21
• 2.3.1 有限状态自动机15-17
• 2.3.2 Büchi自动机17-19
• 2.3.3 语言判空19-21
• 2.4 模型检测原理、过程方法21-23
• 2.4.1 模型检测原理21-22
• 2.4.2 模型检测的过程22-23
• 2.5 本章小结23-25
• 第三章 行为时序逻辑TLA25-37
• 3.1 概述25
• 3.2 TLA的基本概念25-29
• 3.2.1 符号与语法27-28
• 3.2.2 行为与语义28-29
• 3.3 TLA中的公平性、活性、安全性29-31
• 3.3.1 公平性29-30
• 3.3.2 活性30
• 3.3.5 安全性30-31
• 3.4 TLA+语言31-34
• 3.4.1 TLA+模块31
• 3.4.2 TLA+操作符31-34
• 3.5 TLC模型检测器34-36
• 3.6 本章小结36-37
• 第四章 Pastry协议37-46
• 4.1 P2P网络及Pastry协议简介37-38
• 4.2 Pastry协议节点数据结构38-39
• 4.3 Pastry协议路由39-42
• 4.3.1 路由工作原理及算法描述39-42
• 4.4 Pastry协议的自组织和自适应42-44
• 4.4.1 Join42-44
• 4.4.2 Failure44
• 4.5 本章小结44-46
• 第五章 Pastry协议的规约描述与验证46-60
• 5.1 Pastry协议形式化规约过程分析46-47
• 5.2 Pastry协议的规约描述47-55
• 5.2.1 定义、常量、变量和消息类型47-49
• 5.2.2 协议接.间的行为描述规约49-51
• 5.2.3 协议内部的行为描述规约51-54
• 5.2.4 下一状态关系描述54-55
• 5.3 Pastry协议中的性质描述55
• 5.4 验证结果与分析55-58
• 5.5 结论58-59
• 5.6 本章小结59-60
• 第六章 总结与展望60-62
• 6.1 主要工作总结60
• 6.2 展望60-62
• 致谢62-63
• 参考文献63-67

【相似文献】

中国期刊全文数据库 前10条

1 黄佳;;基于行为时序逻辑的安全协议研究[J];信息通信;2012年04期

2 谢扬光;同步时序逻辑网络的图上作业设计法[J];长春邮电学院学报;1986年02期

3 姜文彬;脉冲型时序逻辑网络设计的解析方法[J];计算机学报;1989年04期

4 姜文彬;脉冲型时序逻辑网络设计（Ⅲ）[J];山东建材学院学报;1995年02期

5 贾国平,郑国梁;用于反应系统的修改时序逻辑[J];软件学报;1997年09期

6 吕娜;;时序逻辑领域的开拓者[J];程序员;2009年12期

7 张春早;;时序逻辑设计的方格图解法[J];湖北机械;1980年04期

8 冯玉琳;林惠民;唐稚松;;时序逻辑程序的证明系统[J];计算机研究与发展;1985年10期

9 姜文彬;脉冲型时序逻辑网络分析[J];电子学报;1986年06期

10 曹立明,施润身;基于时序逻辑的故障预测[J];上海铁道大学学报;1998年12期

中国重要会议论文全文数据库 前3条

1 章超;李彩虹;李廉;;SPIN在同步时序逻辑中的应用[A];2005年全国理论计算机科学学术年会论文集[C];2005年

2 冯荷飞;曹子宁;;交错时序认知逻辑在安全协议中的应用[A];逻辑学及其应用研究——第四届全国逻辑系统、智能科学与信息科学学术会议论文集[C];2008年

3 吴彪;朱立新;赵佳;;基于CPLD的可编程并行接口芯片8255设计与仿真[A];系统仿真技术及其应用（第7卷）——'2005系统仿真技术及其应用学术交流会论文选编[C];2005年

中国博士学位论文全文数据库 前5条

1 刘万伟;扩展时序逻辑的推理及符号化模型检验技术[D];国防科学技术大学;2009年

2 杨琛;打结不变的命题投影时序逻辑与模型检测[D];西安电子科技大学;2010年

3 万良;基于行为时序逻辑TLA的系统、规则与协议检测的研究[D];贵州大学;2009年

4 张南;命题投影时序逻辑的完备公理系统与形式验证[D];西安电子科技大学;2012年

5 赵常智;基于运行时验证的软件监控关键技术研究[D];国防科学技术大学;2011年

中国硕士学位论文全文数据库 前10条

1 张丽;命题投影时序逻辑的判定性和表达性[D];西安电子科技大学;2007年

2 杨琳琳;基于时序逻辑的安全协议验证方法的研究[D];南京航空航天大学;2010年

3 韩冰;线性时序逻辑在失业保险审计中的应用研究[D];哈尔滨工程大学;2010年

4 田聪;命题投影时序逻辑的可判定性[D];西安电子科技大学;2007年

5 林丽秀;时序逻辑转换断言图的研究[D];电子科技大学;2013年

6 赵延珂;基于时序逻辑模型验证的入侵检测方法研究[D];郑州大学;2014年

7 李亚利;基于可能性测度的时序逻辑性质研究[D];陕西师范大学;2013年

8 葛徐骏;基于时序逻辑的双向一致性检测[D];华东师范大学;2015年

9 黄贻望;基于行为时序逻辑模型检测的研究与应用[D];贵州大学;2009年

10 刘照洋;基于行为时序逻辑TLA的网络协议的描述与验证[D];贵州大学;2015年

  本文关键词：基于行为时序逻辑TLA的网络协议的描述与验证，，由笔耕文化传播整理发布。

本文编号：358671