第1章  網絡協議及開發(fā)概論                  
 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  網絡協議的開發(fā)過程                  
 思考與練習                  
 第2章  協議的形式化模型                  
 2.1  有限狀態(tài)機（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  時態(tài)邏輯(TL)                  
 2.3.1  基本術語                  
 2.3.2  時態(tài)邏輯系統                  
 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  狀態(tài)轉換                  
 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  原子性的模型檢驗分析                  
 思考與練習                  
 參考文獻