更新时间：2018-12-27 12:23:32
封面
版权信息
前言
如何阅读、学习本书
第1章 概论
1.1 协议
1.1.1 定义
1.1.2 协议的标准化
1.2 协议工程
第2章 协议设计技术
2.1 协议模型
2.2 协议设计的基本内容
2.2.1 协议的通信环境
2.2.2 协议提供的服务
2.2.3 协议功能
2.2.4 协议元素
2.2.5 协议组织
2.2.6 协议文本
2.3 协议设计方法
2.3.1 协议设计原则
2.3.2 分层次的协议设计
2.3.3 自顶向下的协议设计
2.4 差错控制技术
2.4.1 差错类型
2.4.2 差错检测技术
2.4.3 差错控制技术
2.4.4 差错控制与层次的关系
2.5 流量控制技术
2.5.1 X-on/X-off协议
2.5.2 滑动窗口协议
第3章 协议形式化描述技术
3.1 概述
3.2 FSM
3.2.1 FSM的基本概念
3.2.2 FSM的简化
3.2.3 FSM的错误模型
3.2.4 FSM的合并
3.2.5 扩展的有限状态机(EFSM)
3.3 PetriNet
3.3.1 Petri网的基本概念
3.3.2 Petri网的扩充
3.3.3 Petri网的性质
3.3.4 Petri网在协议描述中的应用
3.4 时序逻辑
3.4.1 基本概念
3.4.2 时序逻辑系统
3.4.3 时序逻辑在协议描述中的应用
3.5 通信顺序进程
3.5.1 概述
3.5.2 CSP在协议描述中的应用
第4章 协议形式描述语言
4.1 SDL语言
4.1.1 SDL语言概述
4.1.2 SDL中的数据
4.1.3 SDL中的宏定义
4.1.4 用SDL描述系统、功能块和进程
4.1.5 SDL在协议描述中的应用举例
4.2 ESTELLE语言
4.2.1 ESTELLE语言概述
4.2.2 模块中的概念
4.2.3 模块的说明
4.2.3 ESTELLE语句
4.2.4 ESTELLE在协议描述中的应用举例
4.3 LOTOS语言
4.3.1 LOTOS中的数据类型
4.3.2 LOTOS的基本概念
4.3.3 LOTOS的其他功能
4.3.4 协议描述举例
4.4 各种形式描述技术的比较
第5章 协议验证技术
5.1 概述
5.2 协议性质
5.2.1 一般性质和特殊性质
5.2.2 安全性和活动性
5.3 可达性分析
5.3.1 可达性分析算法
5.3.2 基于可达性分析的协议错误的检测方法
5.3.3 基于Petri网的可达性分析
5.3.4 状态爆炸问题
5.4 不变性分析
5.4.1 不变性证明
5.4.2 不变性监测系统
第6章 协议验证工具
6.1 SPIN概述
6.2 PROMELA语言
6.2.1 语句的可执行性
6.2.2 变量和数据类型
6.2.3 进程类型
6.2.4 报文通道
6.2.5 控制流
6.2.6 超时
6.2.7 协议正确性描述语句
6.2.8 协议描述示例
6.3 SPIN的应用
6.3.1 理想状态下的数据链路层协议
6.3.2 信道有误码但应答帧不出错不丢失的数据链路层协议
6.3.3 信道有误码但报文和应答均不丢失的数据链路层协议
第7章 协议一致性测试技术
7.1 一致性测试概述
7.2 一致性测试的概念和方法
