Network protocol engineering

　　第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