网络协议工程

7.16 一致性测试工具

7.15.2 基于形式描述语言的测试集生成方法

7.15.1 基于有限状态机的测试集生成方法

7.15 测试集生成方法

7.14 一致性测试系统

7.13 简单测试案例描述

7.12 模块控制

7.11.3 查询和控制操作

7.11.2 基于过程的通信操作

7.11.1 基于消息的通信操作

7.11 通信操作

7.10 程序语句和操作

7.9 测试例

7.8.2 可选步

7.8.1 函数

7.8 函数和可选步

7.7 定时器和操作符

7.6.6 常量和变量

7.6.5 数组

7.6.4 特殊的配置类型

7.6.3 结构化的类型

7.6.2 子类型

7.6.1 基本类型

7.6 TTCN中的数据类型

7.5 基本语言要素

7.4 TTCN概述

7.3 一致性测试方法

7.2.4 一致性测试流程

7.2.3 一致性测试模型

7.2.2 一致性测试级别

7.2.1 一致性测试要求

7.2 一致性测试的概念和方法

7.1 一致性测试概述

第7章 协议一致性测试技术

6.3.3 信道有误码但报文和应答均不丢失的数据链路层协议

6.3.2 信道有误码但应答帧不出错不丢失的数据链路层协议

6.3.1 理想状态下的数据链路层协议

6.3 SPIN的应用

6.2.8 协议描述示例

6.2.7 协议正确性描述语句

6.2.6 超时

6.2.5 控制流

6.2.4 报文通道

6.2.3 进程类型

6.2.2 变量和数据类型

6.2.1 语句的可执行性

6.2 PROMELA语言

6.1 SPIN概述

第6章 协议验证工具

5.4.2 不变性监测系统

5.4.1 不变性证明

5.4 不变性分析

5.3.4 状态爆炸问题

5.3.3 基于Petri网的可达性分析

5.3.2 基于可达性分析的协议错误的检测方法

5.3.1 可达性分析算法

5.3 可达性分析

5.2.2 安全性和活动性

5.2.1 一般性质和特殊性质

5.2 协议性质

5.1 概述

第5章 协议验证技术

4.4 各种形式描述技术的比较

4.3.4 协议描述举例

4.3.3 LOTOS的其他功能

4.3.2 LOTOS的基本概念

4.3.1 LOTOS中的数据类型

4.3 LOTOS语言

4.2.4 ESTELLE在协议描述中的应用举例

4.2.3 ESTELLE语句

4.2.3 模块的说明

4.2.2 模块中的概念

4.2.1 ESTELLE语言概述

4.2 ESTELLE语言

4.1.5 SDL在协议描述中的应用举例

4.1.4 用SDL描述系统、功能块和进程

4.1.3 SDL中的宏定义

4.1.2 SDL中的数据

4.1.1 SDL语言概述

4.1 SDL语言

第4章 协议形式描述语言

3.5.2 CSP在协议描述中的应用

3.5.1 概述

3.5 通信顺序进程

3.4.3 时序逻辑在协议描述中的应用

3.4.2 时序逻辑系统

3.4.1 基本概念

3.4 时序逻辑

3.3.4 Petri网在协议描述中的应用

3.3.3 Petri网的性质

3.3.2 Petri网的扩充

3.3.1 Petri网的基本概念

3.3 PetriNet

3.2.5 扩展的有限状态机(EFSM)

3.2.4 FSM的合并

3.2.3 FSM的错误模型

3.2.2 FSM的简化

3.2.1 FSM的基本概念

3.2 FSM

3.1 概述

第3章 协议形式化描述技术

2.5.2 滑动窗口协议

2.5.1 X-on/X-off协议

2.5 流量控制技术

2.4.4 差错控制与层次的关系

2.4.3 差错控制技术

2.4.2 差错检测技术

2.4.1 差错类型

2.4 差错控制技术

2.3.3 自顶向下的协议设计

2.3.2 分层次的协议设计

2.3.1 协议设计原则

2.3 协议设计方法

2.2.6 协议文本

2.2.5 协议组织

2.2.4 协议元素

2.2.3 协议功能

2.2.2 协议提供的服务

2.2.1 协议的通信环境

2.2 协议设计的基本内容

2.1 协议模型

第2章 协议设计技术

1.2 协议工程

1.1.2 协议的标准化

1.1.1 定义

1.1 协议

第1章 概论

如何阅读、学习本书

前言

版权信息

封面

封面

版权信息

前言

如何阅读、学习本书

第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 一致性测试的概念和方法

7.2.1 一致性测试要求

7.2.2 一致性测试级别

7.2.3 一致性测试模型

7.2.4 一致性测试流程

7.3 一致性测试方法

7.4 TTCN概述

7.5 基本语言要素

7.6 TTCN中的数据类型

7.6.1 基本类型

7.6.2 子类型

7.6.3 结构化的类型

7.6.4 特殊的配置类型

7.6.5 数组

7.6.6 常量和变量

7.7 定时器和操作符

7.8 函数和可选步

7.8.1 函数

7.8.2 可选步

7.9 测试例

7.10 程序语句和操作

7.11 通信操作

7.11.1 基于消息的通信操作

7.11.2 基于过程的通信操作

7.11.3 查询和控制操作

7.12 模块控制

7.13 简单测试案例描述

7.14 一致性测试系统

7.15 测试集生成方法

7.15.1 基于有限状态机的测试集生成方法

7.15.2 基于形式描述语言的测试集生成方法

7.16 一致性测试工具