出版日期：2003 年6月

开本：16开

页码：367

版次：1-1

计算机网路及数据通信是当今信息社会的基石，网路协定则是其中不可缺少的重要组成部分。形式化方法与技术已经渗透到网路协定开发的整个过程。本书主要内容包括：网路协定及开发概论；网路协定的形式化模型；网路协定的形式描述语言；网路协定的形式化验证；网路协定的形式化综合；网路协定的测试；网路协定的分析验证工具；电子商务协定的形式化分析等。本书可作为计算机、通信、自动化等专业高年级本科生或研究生的教学用书，也可供相关领域的研究和工程技术人员参考。

第1章 网路协定及开发概论

1.1 早期的通信及协定

1.1.1 早期的通信系统

1.1.2 协定缺陷的教训

1.2 通信与计算机的结合

1.2.1 数据通信

1.2.2 计算机网路

1.3 网路协定及其基本元素

1.3.1 网路协定的定义

1.3.2 网路协定的基本要素

1.3.3 简单协定的分析

1.4 分层结构与osi模型

1.4.1 分层结构的意义

1.4.2 osi模型

1.5 网路协定的开发过程

思考与练习

第2章 协定的形式化模型

2.1 有限状态机（fsm）

2.1.1 fsm的基本定义

2.1.2 fsm的化简与複合

.2.1.3 协定的fsm模型

2.2 petri网

2.2.1 petri网的基本定义

2.2.2 petri网的性质

2.2.3 petri网的分析

2.2.4 协定的petri网模型

2.3 时态逻辑(tl)

2.3.1 基本术语

2.3.2 时态逻辑系统

2.3.3 协定的tl模型

2.4 通信进程演算

2.4.1 ccs的基本定义

2.4.2 ccs的扩展

2.4.3 协定的ccs模型

思考与练习

第3章 网路协定的形式描述语言

3.1 estelle

3.1.1 概述

3.1.2 模组及相关概念

3.1.3 模组通信

3.1.4 状态转换

3.1.5 estelle描述举例

3.2 lotos

3.2.1 概述

3.2.2 进程及相关概念

3.2.3 行为运算元

3.2.4 抽象数据类型

3.2.5 lotos描述举例

3.3 sdl

3.3.1 概述

3.3.2 结构的定义

3.3.3 进程的行为

3.3.4 通信机制

3.3.5 数据

3.3.6 sdl描述举例

思考与练习

第4章 协定的形式化验证

4.1 协定性质概述

4.2 系统断言语言

4.2.1 字元串及其运算

4.2.2 抽象结构

4.2.3 断言语言ctl

4.2.4 ctl运算元的不动点特性

4.2.5 ctl描述举例

4.3 不变性分析

4.4 可达性分析

4.5 符号模型检验

4.5.1 有序二叉判决图

4.5.2 基于obdd的符号模型检验

思考与练习

第5章 协定的形式化综合

5.1 概述

5.2 fsm网及其性质

5.3 协定的串列综合

5.4 协定的交替功能综合

5.5 冲突和同步的解决方法

5.5.1 竞争冲突解决策略

5.5.2 冲突标识方法

5.5.3 同步的充要条件

思考与练习

第6章 网路协定的测试

6.1 协定测试概述

6.1.1 一致性测试

6.1.2 故障模型

6.1.3 协定测试结构

6.1.4 协定测试级别

6.1.5 协定测试流程

6.2 协定测试语言ttcn

6.2.1 ttcn简介

6.2.2 ttcn－3核心语言

6.2.3 简单测试案例

6.3 控制流测试序列设计

6.3.1 测试的基本假设

6.3.2 测试序列生成算法

6.4 数据流测试序列设计

6.4.1 数据流测试的概念

6.4.2 数据流测试序列生成

思考与练习

第7章 协定的分析验证工具

7.1 spin工具

7.1.1 概述

7.1.2 promela语言

7.1.3 spin的套用

7.2 smv工具

7.2.1 概述

7.2.2 smv输入语言

7.2.3 smv的套用

思考与练习

第8章 电子商务协定的形式化分析

8.1 电子商务协定设计概述

8.2 典型电子商务协定

8.2.1 set协定

8.2.2 netbill协定

8.2.3 digicash协定

8.3 电子商务协定的逻辑分析

8.3.1 逻辑分析概述

8.3.2 ban逻辑

8.3.3 kailar逻辑

8.4 电子商务协定的模型检验分析

8.4.1 模型检验分析概述

8.4.2 安全性的模型检验分析

8.4.3 原子性的模型检验分析

思考与练习

参考文献