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

定　價：￥25.00

作　者：	古天龍，蔡國永著
出版社：	電子工業(yè)出版社
叢編項：
標　簽：	暫缺

購買這本書可以去

當當網(wǎng) (￥20.00)

ISBN：	9787505386464	出版時間：	2003-06-01	包裝：	膠版紙
開本：	21cm	頁數(shù)：	367	字數(shù)：

內(nèi)容簡介

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

作者簡介

暫缺《網(wǎng)絡協(xié)議的形式化分析與設計》作者簡介

圖書目錄

第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  ESTELLE
3.1.1  概述
3.1.2  模塊及相關概念
3.1.3  模塊通信
3.1.4  狀態(tài)轉換
3.1.5  ESTELLE描述舉例
3.2  LOTOS
3.2.1  概述
3.2.2  進程及相關概念
3.2.3  行為算子
3.2.4  抽象數(shù)據(jù)類型
3.2.5  LOTOS描述舉例
3.3  SDL
3.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  斷言語言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)及其性質
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é)議測試語言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  原子性的模型檢驗分析
思考與練習
參考文獻