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

第1章  網(wǎng)絡(luò)協(xié)議及開發(fā)概論                  
 1.1  早期的通信及協(xié)議                  
 1.1.1  早期的通信系統(tǒng)                  
 1.1.2  協(xié)議缺陷的教訓(xùn)                  
 1.2  通信與計(jì)算機(jī)的結(jié)合                  
 1.2.1  數(shù)據(jù)通信                  
 1.2.2  計(jì)算機(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  簡(jiǎn)單協(xié)議的分析                  
 1.4  分層結(jié)構(gòu)與OSI模型                  
 1.4.1  分層結(jié)構(gòu)的意義                  
 1.4.2  OSI模型                  
 1.5  網(wǎng)絡(luò)協(xié)議的開發(fā)過(guò)程                  
 思考與練習(xí)                  
 第2章  協(xié)議的形式化模型                  
 2.1  有限狀態(tài)機(jī)（FSM）                  
 2.1.1  FSM的基本定義                  
 2.1.2  FSM的化簡(jiǎn)與復(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  時(shí)態(tài)邏輯(TL)                  
 2.3.1  基本術(shù)語(yǔ)                  
 2.3.2  時(shí)態(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é)議的形式描述語(yǔ)言                  
 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)斷言語(yǔ)言                  
 4.2.1  字符串及其運(yùn)算                  
 4.2.2  抽象結(jié)構(gòu)                  
 4.2.3  斷言語(yǔ)言CTL                  
 4.2.4  CTL算子的不動(dòng)點(diǎn)特性                  
 4.2.5  CTL描述舉例                  
 4.3  不變性分析                  
 4.4  可達(dá)性分析                  
 4.5  符號(hào)模型檢驗(yàn)                  
 4.5.1  有序二叉判決圖                  
 4.5.2  基于OBDD的符號(hào)模型檢驗(yàn)                  
 思考與練習(xí)                  
 第5章  協(xié)議的形式化綜合                  
 5.1  概述                  
 5.2  FSM網(wǎng)及其性質(zhì)                  
 5.3  協(xié)議的串行綜合                  
 5.4  協(xié)議的交替功能綜合                  
 5.5  沖突和同步的解決方法                  
 5.5.1  競(jìng)爭(zhēng)沖突解決策略                  
 5.5.2  沖突標(biāo)識(shí)方法                  
 5.5.3  同步的充要條件                  
 思考與練習(xí)                  
 第6章  網(wǎng)絡(luò)協(xié)議的測(cè)試                  
 6.1  協(xié)議測(cè)試概述                  
 6.1.1  一致性測(cè)試                  
 6.1.2  故障模型                  
 6.1.3  協(xié)議測(cè)試結(jié)構(gòu)                  
 6.1.4  協(xié)議測(cè)試級(jí)別                  
 6.1.5  協(xié)議測(cè)試流程                  
 6.2  協(xié)議測(cè)試語(yǔ)言TTCN                  
 6.2.1  TTCN簡(jiǎn)介                  
 6.2.2  TTCN－3核心語(yǔ)言                  
 6.2.3  簡(jiǎn)單測(cè)試案例                  
 6.3  控制流測(cè)試序列設(shè)計(jì)                  
 6.3.1  測(cè)試的基本假設(shè)                  
 6.3.2  測(cè)試序列生成算法                  
 6.4  數(shù)據(jù)流測(cè)試序列設(shè)計(jì)                  
 6.4.1  數(shù)據(jù)流測(cè)試的概念                  
 6.4.2  數(shù)據(jù)流測(cè)試序列生成                  
 思考與練習(xí)                  
 第7章  協(xié)議的分析驗(yàn)證工具                  
 7.1  SPIN工具                  
 7.1.1  概述                  
 7.1.2  Promela語(yǔ)言                  
 7.1.3  SPIN的應(yīng)用                  
 7.2  SMV工具                  
 7.2.1  概述                  
 7.2.2  SMV輸入語(yǔ)言                  
 7.2.3  SMV的應(yīng)用                  
 思考與練習(xí)                  
 第8章  電子商務(wù)協(xié)議的形式化分析                  
 8.1  電子商務(wù)協(xié)議設(shè)計(jì)概述                  
 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)