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

第1章  網(wǎng)絡(luò)協(xié)議及開發(fā)概論                  
 1.1  早期的通信及協(xié)議                  
 1.1.1  早期的通信系統(tǒng)                  
 1.1.2  協(xié)議缺陷的教訓(xùn)                  
 1.2  通信與計算機(jī)的結(jié)合                  
 1.2.1  數(shù)據(jù)通信                  
 1.2.2  計算機(jī)網(wǎng)絡(luò)                  
 1.3  網(wǎng)絡(luò)協(xié)議及其基本元素                  
 1.3.1  網(wǎng)絡(luò)協(xié)議的定義                  
 1.3.2  網(wǎng)絡(luò)協(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)絡(luò)協(xié)議的開發(fā)過程                  
 思考與練習(xí)                  
 第2章  協(xié)議的形式化模型                  
 2.1  有限狀態(tài)機(jī)（FSM）                  
 2.1.1  FSM的基本定義                  
 2.1.2  FSM的化簡與復(fù)合                  
 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  通信進(jìn)程演算                  
 2.4.1  CCS的基本定義                  
 2.4.2  CCS的擴(kuò)展                  
 2.4.3  協(xié)議的CCS模型                  
 思考與練習(xí)                  
 第3章  網(wǎng)絡(luò)協(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  進(jìn)程及相關(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  進(jìn)程的行為                  
 3.3.4  通信機(jī)制                  
 3.3.5  數(shù)據(jù)                  
 3.3.6  SDL描述舉例                  
 思考與練習(xí)                  
 第4章  協(xié)議的形式化驗(yàn)證                  
 4.1  協(xié)議性質(zhì)概述                  
 4.2  系統(tǒng)斷言語言                  
 4.2.1  字符串及其運(yùn)算                  
 4.2.2  抽象結(jié)構(gòu)                  
 4.2.3  斷言語言CTL                  
 4.2.4  CTL算子的不動點(diǎn)特性                  
 4.2.5  CTL描述舉例                  
 4.3  不變性分析                  
 4.4  可達(dá)性分析                  
 4.5  符號模型檢驗(yàn)                  
 4.5.1  有序二叉判決圖                  
 4.5.2  基于OBDD的符號模型檢驗(yàn)                  
 思考與練習(xí)                  
 第5章  協(xié)議的形式化綜合                  
 5.1  概述                  
 5.2  FSM網(wǎng)及其性質(zhì)                  
 5.3  協(xié)議的串行綜合                  
 5.4  協(xié)議的交替功能綜合                  
 5.5  沖突和同步的解決方法                  
 5.5.1  競爭沖突解決策略                  
 5.5.2  沖突標(biāo)識方法                  
 5.5.3  同步的充要條件                  
 思考與練習(xí)                  
 第6章  網(wǎng)絡(luò)協(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  控制流測試序列設(shè)計                  
 6.3.1  測試的基本假設(shè)                  
 6.3.2  測試序列生成算法                  
 6.4  數(shù)據(jù)流測試序列設(shè)計                  
 6.4.1  數(shù)據(jù)流測試的概念                  
 6.4.2  數(shù)據(jù)流測試序列生成                  
 思考與練習(xí)                  
 第7章  協(xié)議的分析驗(yàn)證工具                  
 7.1  SPIN工具                  
 7.1.1  概述                  
 7.1.2  Promela語言                  
 7.1.3  SPIN的應(yīng)用                  
 7.2  SMV工具                  
 7.2.1  概述                  
 7.2.2  SMV輸入語言                  
 7.2.3  SMV的應(yīng)用                  
 思考與練習(xí)                  
 第8章  電子商務(wù)協(xié)議的形式化分析                  
 8.1  電子商務(wù)協(xié)議設(shè)計概述                  
 8.2  典型電子商務(wù)協(xié)議                  
 8.2.1  SET協(xié)議                  
 8.2.2  Netbill協(xié)議                  
 8.2.3  Digicash協(xié)議                  
 8.3  電子商務(wù)協(xié)議的邏輯分析                  
 8.3.1  邏輯分析概述                  
 8.3.2  BAN邏輯                  
 8.3.3  Kailar邏輯                  
 8.4  電子商務(wù)協(xié)議的模型檢驗(yàn)分析                  
 8.4.1  模型檢驗(yàn)分析概述                  
 8.4.2  安全性的模型檢驗(yàn)分析                  
 8.4.3  原子性的模型檢驗(yàn)分析                  
 思考與練習(xí)                  
 參考文獻(xiàn)