第1章 概论 1
1.1 协议 1
1.1.1 定义 1
1.1.2 协议的标准化 2
1.2 协议工程 5
第2章 协议设计技术 10
2.1 协议模型 10
2.2 协议设计的基本内容 11
2.2.1 协议的通信环境 11
2.2.2 协议提供的服务 13
2.2.3 协议功能 13
2.2.4 协议元素 16
2.2.5 协议组织 19
2.2.6 协议文本 20
2.3 协议设计方法 21
2.3.1 协议设计原则 21
2.3.2 分层次的协议设计 22
2.3.3 自顶向下的协议设计 23
2.4 差错控制技术 24
2.4.1 差错类型 24
2.4.2 差错检测技术 25
2.4.3 差错控制技术 32
2.4.4 差错控制与层次的关系 38
2.5 流量控制技术 40
2.5.1 X-on/X-off协议 41
2.5.2 滑动窗口协议 41
第3章 协议形式化描述技术 48
3.1 概述 48
3.2 FSM 49
3.2.1 FSM的基本概念 49
3.2.2 FSM的简化 52
3.2.3 FSM的错误模型 53
3.2.4 FSM的合并 54
3.2.5 扩展的有限状态机（EFSM） 54
3.3 PetriNet 55
3.3.1 Petri网的基本概念 55
3.3.2 Petri网的扩充 57
3.3.3 Petri网的性质 58
3.3.4 Petri网在协议描述中的应用 61
3.4 时序逻辑 63
3.4.1 基本概念 64
3.4.2 时序逻辑系统 65
3.4.3 时序逻辑在协议描述中的应用 67
3.5 通信顺序进程 70
3.5.1 概述 70
3.5.2 CSP在协议描述中的应用 73
第4章 协议形式描述语言 77
4.1 SDL语言 77
4.1.1 SDL语言概述 77
4.1.2 SDL中的数据 79
4.1.3 SDL中的宏定义 83
4.1.4 用SDL描述系统、功能块和进程 84
4.1.5 SDL在协议描述中的应用举例 88
4.2 ESTELLE语言 90
4.2.1 ESTELLE语言概述 90
4.2.2 模块中的概念 91
4.2.3 模块的说明 93
4.2.3 ESTELLE语句 96
4.2.4 ESTELLE在协议描述中的应用举例 99
4.3 LOTOS语言 103
4.3.1 LOTOS中的数据类型 103
4.3.2 LOTOS的基本概念 105
4.3.3 LOTOS的其他功能 108
4.3.4 协议描述举例 109
4.4 各种形式描述技术的比较 111
第5章 协议验证技术 115
5.1 概述 115
5.2 协议性质 118
5.2.1 一般性质和特殊性质 118
5.2.2 安全性和活动性 120
5.3 可达性分析 121
5.3.1 可达性分析算法 122
5.3.2 基于可达性分析的协议错误的检测方法 124
5.3.3 基于Petri网的可达性分析 125
5.3.4 状态爆炸问题 126
5.4 不变性分析 127
5.4.1 不变性证明 127
5.4.2 不变性监测系统 130
第6章 协议验证工具 135
6.1 SPIN概述 135
6.2 PROMELA语言 136
6.2.1 语句的可执行性 136
6.2.2 变量和数据类型 137
6.2.3 进程类型 138
6.2.4 报文通道 140
6.2.5 控制流 143
6.2.6 超时 145
6.2.7 协议正确性描述语句 146
6.2.8 协议描述示例 150
6.3 SPIN的应用 152
6.3.1 理想状态下的数据链路层协议 152
6.3.2 信道有误码但应答帧不出错不丢失的数据链路层协议 155
6.3.3 信道有误码但报文和应答均不丢失的数据链路层协议 159
第7章 协议一致性测试技术 165
7.1 一致性测试概述 165
7.2 一致性测试的概念和方法 167
7.2.1 一致性测试要求 167
7.2.2 一致性测试级别 168
7.2.3 一致性测试模型 170
7.2.4 一致性测试流程 172
7.3 一致性测试方法 174
7.4 TTCN概述 177
7.5 基本语言要素 182
7.6 TTCN中的数据类型 184
7.6.1 基本类型 185
7.6.2 子类型 186
7.6.3 结构化的类型 187
7.6.4 特殊的配置类型 193
7.6.5 数组 196
7.6.6 常量和变量 197
7.7 定时器和操作符 198
7.8 函数和可选步 200
7.8.1 函数 200
7.8.2 可选步 203
7.9 测试例 206
7.10 程序语句和操作 210
7.11 通信操作 218
7.11.1 基于消息的通信操作 219
7.11.2 基于过程的通信操作 221
7.11.3 查询和控制操作 226
7.12 模块控制 228
7.13 简单测试案例描述 230
7.14 一致性测试系统 233
7.15 测试集生成方法 235
7.15.1 基于有限状态机的测试集生成方法 235
7.15.2 基于形式描述语言的测试集生成方法 240
7.16 一致性测试工具 241
附录A 英文缩略词 245