內容簡介
圖書封面內容簡介計算機網路及數據通信是當今信息社會的基石，網路協定則是其中不可缺少的重要組成部分。形式化方法與技術已經滲透到網路協定開發的整個過程。本書就網路協定分析與設計中的形式化方法與技術展開討論和介紹，主要內容包括：網路協定及開發概論；網路協定的形式化模型；網路協定的形式描述語言；網路協定的形式化驗證；網路協定的形式化綜合；網路協定的測試；網路協定的分析驗證工具；電子商務協定的形式化分析等。本書可作為計算機、通信、自動化等專業高年級本科生或研究生的教學用書，也可供相關領域的研究和工程技術人員參考。
圖書目錄
第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.1Estelle
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.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.1SET協定
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 原子性的模型檢驗分析
思考與練習
參考文獻
