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

內容概要

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

書籍目錄

第1章  網(wǎng)絡協(xié)議及開發(fā)概論1.1  早期的通信及協(xié)議1.1.1  早期的通信系統(tǒng)1.1.2  協(xié)議缺陷的教訓1.2  通信與計算機的結合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  分層結構與OSI模型1.4.1  分層結構的意義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)的性質2.2.3  Petri網(wǎng)的分析2.2.4  協(xié)議的Petri網(wǎng)模型2.3  時態(tài)邏輯(TL)2.3.1  基本術語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  ESTELLE3.1.1  概述3.1.2  模塊及相關概念3.1.3  模塊通信3.1.4  狀態(tài)轉換3.1.5  ESTELLE描述舉例3.2  LOTOS3.2.1  概述3.2.2  進程及相關概念3.2.3  行為算子3.2.4  抽象數(shù)據(jù)類型3.2.5  LOTOS描述舉例3.3  SDL3.3.1  概述3.3.2  結構的定義3.3.3  進程的行為3.3.4  通信機制3.3.5  數(shù)據(jù)3.3.6  SDL描述舉例思考與練習第4章  協(xié)議的形式化驗證4.1  協(xié)議性質概述4.2  系統(tǒng)斷言語言4.2.1  字符串及其運算4.2.2  抽象結構4.2.3  斷言語言CTL4.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)及其性質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é)議測試結構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  控制流測試序列設計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  原子性的模型檢驗分析思考與練習參考文獻

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

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

---