通信协议验证中形式化描述方法集成理论的研究

摘要

协议是计算机网络和通信的核心.研究形式化的协议理论对保证网络和通信的质量、网络和信息安全具有十分重要的理论意义和应用价值.该文提出了一种形式化描述方法集成的方法,并为此提供了一致的形式化语义基础.该论文的主要工作包括:1.提供形式化描述语言集成的基本理论依据 该文通过收集、整理,总结出形式化描述语言的一般性定义,并从该定义出发,对形式化描述语言进行了认真地剖析和研究,了解各种形式化描述语言之间产生差异的根源,并引入可以将被描述对象划分成等价类的语义抽象函数,将其作为把不同形式化描述语言联系起来的工具,为形式化描述方法的集成提供基本的理论依据.2.提出一种形式化描述方法集成的方法 形式化描述方法的集成主要有两类方式:集成两种或多种形式化描述方法形成一种新的形式化描述方法;将一种或多种形式化描述方法与一种或多种半形式化方法集成.该文主要研究第一类方式,并且提出了一个独立各种具体的形式化描述方法的集成方法.3.确立一致的形式化语义域基础 一致的形式化语义基础是该文提出的形式化描述方法的集成方法的基石.任何特定对象的语义都是由计算这个对象的属性得到.所谓一致的形式化基础,就是通过对系统属性的划分,对系统的各种属性概念进行形式化描述和定义,形成联系各种形式化描述语言的语义基础,进而形成一个形式化的框架,为各种形式化描述语言的比较、集成提供理论依据.复杂通信协议系统的各种属性总的来说可以被划分为两类:系统的行为属性和系统的结构化属性.为了将通信协议系统各种属性特征抽象出来,我们分别在不同的抽象层次上给出了四种行为形式化模型和两种结构形式化模型.4.Petri网和Z语言的集成 应用该文提出的形式化描述方法的集成方法,我们集成了Petri网和Z语言这两种目前已经相当成熟的形式化描述方法,形成一种新的、集成的形式化描述方法PetriZ网,并给出了它的形式化定义.PetriZ网一方面可以看作是Petri网在数据和函数定义等系统结构方面的扩展;另一方面,PetriZ网也是Z语言在并发技术方面的一种扩展.使用PetriZ网,我们可以对复杂的通信协议系统的各方面的属性进行比较全面地描述和分析.该文还应用PetriZ网对RADIUS协议系统进行了描述,并在此描述的基础上对RADIUS协议系统进行了可达性分析和不变性证明.

目录

文摘

英文文摘

第一章绪论

1.1研究背景

1.2研究现状

1.2.1协议验证技术

1.2.1形式描述方法及其集成

1.3研究目的

1.4研究内容和研究方案

1.5论文安排

第二章通信协议及其验证方法

2.1通信协议及其构成

2.2通信协议验证

2.2.1通信网络协议工程

2.2.2通信协议验证

2.3协议的性质

2.3.1活动性(Liveness)

2.3.2安全性(Safety)

2.3.3活动性与安全性的关系

2.3.4一致性(Consistency)

2.3.5完备性(Completeness)

2.3.6其他性质

2.3.6协议属性的形式化描述

2.4协议验证的方法

2.4.1逻辑证明(Logic proof)

2.4.2可达性分析(Reachability analysis)

2.4.3模拟(simulation)技术

2.4.4协议验证中的形式化描述方法

2.5小结

第三章形式化描述方法

3.1概述

3.2形式化描述方法

3.3形式化描述方法的组成

3.3.1形式化描述语言

3.3.2形式化证明

3.3.3抽象

3.3.4动态描述(仿真)

3.4关于形式化方法的争议

3.5形式化描述语言的一般性定义

3.5.1语法域

3.5.2语义域

3.5.3映射关系

3.5.4描述的性质

3.5.5形式化逻辑证明

3.6小结

第四章形式化描述方法的集成

4.1概述

4.1.1形式化描述方法的集成研究的原因

4.1.2形式化描述方法集成的方式

4.1.3形式化描述方法集成的难点

4.2形式化描述方法的分类

4.3各类形式化描述方法的比较

4.3.1自动贩卖机系统

4.3.2 Petri网

4.3.3 LOTOS

4.3.4关系语言

4.3.4 Z语言

4.4形式化描述方法集成的方法

4.4.1形式化描述方法集成

4.4.2形式化描述语言集成

4.4.3具体集成步骤

4.4.4形式化描述语言的翻译函数

4.4.5谓词描述和验算算子的集成

4.4.6相关工作与重要意义

4.5小结

第五章一致的形式化语义基础

5.1概述

5.2行为概念的形式化

5.2.1抽象事件模型

5.2.2输入/输出模型

5.2.3内部/外部模型

5.2.4状态模型

5.2.5相关形式化描述方法的比较

5.3结构化概念的形式化

5.3.1交互作用点模型

5.3.2分层模型

5.3.3相关形式化描述方法的比较

5.4小结

第六章Petri网和Z语言的集成

6.1概述

6.2 RADIUS协议

6.2.1基本工作原理

6.2.2数据包格式

6.2.3协议分析

6.3 PetriZ网

6.3.1 PetriZ网的形式化定义

6.3.2 PetriZ网的主要特点

6.3.3系统状态

6.3.4系统状态的变迁

6.3.5 PetriZ网中的变量

6.3.6 RADIUS协议的PetriZ网描述

6.4并发路径选择生成可达性分析

6.4.1并发路径

6.4.2可达性分析

6.4.3 RADIUS协议的可达性分析

6.5不变性证明

6.5.1不变性证明方法

6.5.2 RADIUS协议的不变性证明

6.6相关工作

6.6.1与Petri的比较

6.6.2与Z语言的比较

6.6.3与LOTOS的比较

6.6.4适用范围

6.7小结

第七章结束语

7.1主要研究工作

7.1.1对通信协议及其验证方法的分析和研究

7.1.2形式化描述方法的研究

7.1.3形式化描述方法的集成方法

7.2研究中的创新点

7.2.1形式化描述语言集成的基本理论基础

7.2.2形式化描述方法的集成方法

7.2.3 PetriZ网

7.3进一步的工作

参考文献

在读博士期间发表的论文

读博士期间参加的科研项目

致谢