吴礼发编著的这本《网络协议工程》以协议工程活动所涉及的各种技术为主线，主要内容包括：协议工程概论、协议设计技术、协议形式化描述技术、协议形式描述语言、协议验证技术、协议验证工具、协议一致性测试技术等。各章均附有讨论题、思考题及参考文献。

网络协议是计算机网络及数据通信的核心，开发正确、有效的网络协议一直是人们追求的目标，网络协议工程正是实现这一目标的重要途径。目前的网络类书籍一般以介绍现有协议为主，而吴礼发编著的这本《网络协议工程》的主要目的则是介绍如何设计开发协议，是协议开发的指南，书中介绍的协议设计与分析方法是从作者十多年教学和工程实践中总结出来的，有较强的实用价值。本书以协议工程活动所涉及的各种技术为主线，主要内容包括：协议工程概论、协议设计技术、协议形式化描述技术、协议形式描述语言、协议验证技术、协议验证工具、协议一致性测试技术等。各章均附有讨论题、思考题及参考文献。

《网络协议工程》可作为网络工程、计算机、通信工程等专业高年级本科生和研究生的网络协议工程、协议设计与分析、通信软件开发等课程的教材，也可作为网络研究和开发人员的自学教材和参考书。

第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