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

內(nèi)容概要

　　 計算機網(wǎng)絡(luò)及數(shù)據(jù)通信是當(dāng)今信息社會的基石，網(wǎng)絡(luò)協(xié)議則是其中不可缺少的重要組成部分。形式化方法與技術(shù)已經(jīng)滲透到網(wǎng)絡(luò)協(xié)議開發(fā)的整個過程。本書就網(wǎng)絡(luò)協(xié)議分析與設(shè)計中的形式化方法與技術(shù)展開討論和介紹，主要內(nèi)容包括：網(wǎng)絡(luò)協(xié)議及開發(fā)概論；網(wǎng)絡(luò)協(xié)議的形式化模型；網(wǎng)絡(luò)協(xié)議的形式描述語言；網(wǎng)絡(luò)協(xié)議的形式化驗證；網(wǎng)絡(luò)協(xié)議的形式化綜合；網(wǎng)絡(luò)協(xié)議的測試；網(wǎng)絡(luò)協(xié)議的分析驗證工具；電子商務(wù)協(xié)議的形式化分析等。本書可作為計算機、通信、自動化等專業(yè)高年級本科生或研究生的教學(xué)用書，也可供相關(guān)領(lǐng)域的研究和工程技術(shù)人員參考。

書籍目錄

第1章  網(wǎng)絡(luò)協(xié)議及開發(fā)概論1.1  早期的通信及協(xié)議1.1.1  早期的通信系統(tǒng)1.1.2  協(xié)議缺陷的教訓(xùn)1.2  通信與計算機的結(jié)合1.2.1  數(shù)據(jù)通信1.2.2  計算機網(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)機（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的擴展2.4.3  協(xié)議的CCS模型思考與練習(xí)第3章  網(wǎng)絡(luò)協(xié)議的形式描述語言3.1  ESTELLE3.1.1  概述3.1.2  模塊及相關(guān)概念3.1.3  模塊通信3.1.4  狀態(tài)轉(zhuǎn)換3.1.5  ESTELLE描述舉例3.2  LOTOS3.2.1  概述3.2.2  進(jìn)程及相關(guān)概念3.2.3  行為算子3.2.4  抽象數(shù)據(jù)類型3.2.5  LOTOS描述舉例3.3  SDL3.3.1  概述3.3.2  結(jié)構(gòu)的定義3.3.3  進(jìn)程的行為3.3.4  通信機制3.3.5  數(shù)據(jù)3.3.6  SDL描述舉例思考與練習(xí)第4章  協(xié)議的形式化驗證4.1  協(xié)議性質(zhì)概述4.2  系統(tǒng)斷言語言4.2.1  字符串及其運算4.2.2  抽象結(jié)構(gòu)4.2.3  斷言語言CTL4.2.4  CTL算子的不動點特性4.2.5  CTL描述舉例4.3  不變性分析4.4  可達(dá)性分析4.5  符號模型檢驗4.5.1  有序二叉判決圖4.5.2  基于OBDD的符號模型檢驗思考與練習(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é)議測試語言TTCN6.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é)議的分析驗證工具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é)議的模型檢驗分析8.4.1  模型檢驗分析概述8.4.2  安全性的模型檢驗分析8.4.3  原子性的模型檢驗分析思考與練習(xí)參考文獻(xiàn)

圖書封面

圖書標(biāo)簽Tags

無

評論、評分、閱讀與下載

---

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

---