網(wǎng)絡協(xié)議的形式化分析與設計

第1章  網(wǎng)絡協(xié)議及開發(fā)概論                  
 1.1  早期的通信及協(xié)議                  
 1.1.1  早期的通信系統(tǒng)                  
 1.1.2  協(xié)議缺陷的教訓                  
 1.2  通信與計算機的結(jié)合                  
 1.2.1  數(shù)據(jù)通信                  
 1.2.2  計算機網(wǎng)絡                  
 1.3  網(wǎng)絡協(xié)議及其基本元素                  
 1.3.1  網(wǎng)絡協(xié)議的定義                  
 1.3.2  網(wǎng)絡協(xié)議的基本要素                  
 1.3.3  簡單協(xié)議的分析                  
 1.4  分層結(jié)構(gòu)與OSI模型                  
 1.4.1  分層結(jié)構(gòu)的意義                  
 1.4.2  OSI模型                  
 1.5  網(wǎng)絡協(xié)議的開發(fā)過程                  
 思考與練習                  
 第2章  協(xié)議的形式化模型                  
 2.1  有限狀態(tài)機（FSM）                  
 2.1.1  FSM的基本定義                  
 2.1.2  FSM的化簡與復合                  
 2.1.3  協(xié)議的FSM模型                  
 2.2  Petri網(wǎng)                  
 2.2.1  Petri網(wǎng)的基本定義                  
 2.2.2  Petri網(wǎng)的性質(zhì)                  
 2.2.3  Petri網(wǎng)的分析                  
 2.2.4  協(xié)議的Petri網(wǎng)模型                  
 2.3  時態(tài)邏輯(TL)                  
 2.3.1  基本術(shù)語                  
 2.3.2  時態(tài)邏輯系統(tǒng)                  
 2.3.3  協(xié)議的TL模型                  
 2.4  通信進程演算                  
 2.4.1  CCS的基本定義                  
 2.4.2  CCS的擴展                  
 2.4.3  協(xié)議的CCS模型                  
 思考與練習                  
 第3章  網(wǎng)絡協(xié)議的形式描述語言                  
 3.1  ESTELLE                  
 3.1.1  概述                  
 3.1.2  模塊及相關(guān)概念                  
 3.1.3  模塊通信                  
 3.1.4  狀態(tài)轉(zhuǎn)換                  
 3.1.5  ESTELLE描述舉例                  
 3.2  LOTOS                  
 3.2.1  概述                  
 3.2.2  進程及相關(guān)概念                  
 3.2.3  行為算子                  
 3.2.4  抽象數(shù)據(jù)類型                  
 3.2.5  LOTOS描述舉例                  
 3.3  SDL                  
 3.3.1  概述                  
 3.3.2  結(jié)構(gòu)的定義                  
 3.3.3  進程的行為                  
 3.3.4  通信機制                  
 3.3.5  數(shù)據(jù)                  
 3.3.6  SDL描述舉例                  
 思考與練習                  
 第4章  協(xié)議的形式化驗證                  
 4.1  協(xié)議性質(zhì)概述                  
 4.2  系統(tǒng)斷言語言                  
 4.2.1  字符串及其運算                  
 4.2.2  抽象結(jié)構(gòu)                  
 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章  協(xié)議的形式化綜合                  
 5.1  概述                  
 5.2  FSM網(wǎng)及其性質(zhì)                  
 5.3  協(xié)議的串行綜合                  
 5.4  協(xié)議的交替功能綜合                  
 5.5  沖突和同步的解決方法                  
 5.5.1  競爭沖突解決策略                  
 5.5.2  沖突標識方法                  
 5.5.3  同步的充要條件                  
 思考與練習                  
 第6章  網(wǎng)絡協(xié)議的測試                  
 6.1  協(xié)議測試概述                  
 6.1.1  一致性測試                  
 6.1.2  故障模型                  
 6.1.3  協(xié)議測試結(jié)構(gòu)                  
 6.1.4  協(xié)議測試級別                  
 6.1.5  協(xié)議測試流程                  
 6.2  協(xié)議測試語言TTCN                  
 6.2.1  TTCN簡介                  
 6.2.2  TTCN－3核心語言                  
 6.2.3  簡單測試案例                  
 6.3  控制流測試序列設計                  
 6.3.1  測試的基本假設                  
 6.3.2  測試序列生成算法                  
 6.4  數(shù)據(jù)流測試序列設計                  
 6.4.1  數(shù)據(jù)流測試的概念                  
 6.4.2  數(shù)據(jù)流測試序列生成                  
 思考與練習                  
 第7章  協(xié)議的分析驗證工具                  
 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章  電子商務協(xié)議的形式化分析                  
 8.1  電子商務協(xié)議設計概述                  
 8.2  典型電子商務協(xié)議                  
 8.2.1  SET協(xié)議                  
 8.2.2  Netbill協(xié)議                  
 8.2.3  Digicash協(xié)議                  
 8.3  電子商務協(xié)議的邏輯分析                  
 8.3.1  邏輯分析概述                  
 8.3.2  BAN邏輯                  
 8.3.3  Kailar邏輯                  
 8.4  電子商務協(xié)議的模型檢驗分析                  
 8.4.1  模型檢驗分析概述                  
 8.4.2  安全性的模型檢驗分析                  
 8.4.3  原子性的模型檢驗分析                  
 思考與練習                  
 參考文獻