第一章 概述

一、協(xié)議定義

1. 為網(wǎng)絡(luò)中互相通信的對(duì)等實(shí)體間進(jìn)行數(shù)據(jù)交換二建立的規(guī)則安皱、標(biāo)準(zhǔn)或約定，保證實(shí)體在計(jì)算機(jī)網(wǎng)絡(luò)中有序地交換數(shù)據(jù)。

   
   
   實(shí)體及對(duì)等實(shí)體.png

2. 協(xié)議是關(guān)于分布式系統(tǒng)進(jìn)行信息交換時(shí)地一種約定谷丸，協(xié)議應(yīng)按照語言地方式進(jìn)行定義。即：網(wǎng)絡(luò)協(xié)議就是具有規(guī)定文法应结、語法和語義地語言刨疼。

   
   
   文法語法及語義
3. 延伸為計(jì)算機(jī)通信協(xié)議
   協(xié)議時(shí)計(jì)算機(jī)網(wǎng)絡(luò)和分布式系統(tǒng)中各種通信實(shí)體或進(jìn)程間相互交換信息是必須遵守的一組規(guī)則或約定。

二鹅龄、協(xié)議三要素

語法揩慕、語義、同步

1. 語法
   網(wǎng)絡(luò)協(xié)議中地語法體現(xiàn)為數(shù)據(jù)報(bào)文中的控制信息和各種控制報(bào)文的結(jié)構(gòu)扮休、格式迎卤。
2. 語義
   協(xié)議數(shù)據(jù)報(bào)文中的控制信息和控制報(bào)文所約定的含義，即需要完成何種動(dòng)作玷坠，發(fā)出何種控制信息及做出何種響應(yīng)蜗搔。
3. 同步
   同步是指事件發(fā)生順序的詳細(xì)說明劲藐。具體來說，同步是指通信過程中各種控制報(bào)文傳送的順序關(guān)系樟凄。
   常用建立通信雙方的有限狀態(tài)機(jī)的方法來描述網(wǎng)絡(luò)協(xié)議聘芜。

三、網(wǎng)絡(luò)體系結(jié)構(gòu)

采用層次式結(jié)構(gòu)

網(wǎng)絡(luò)體系結(jié)構(gòu)=計(jì)算機(jī)網(wǎng)絡(luò)的各層+各層協(xié)議的集合

ISO的OSI/RM：

七層模型

IETF的TCP/IP：
網(wǎng)絡(luò)訪問層缝龄、互聯(lián)網(wǎng)層汰现、傳輸層、應(yīng)用層

TCP/IP協(xié)議結(jié)構(gòu)

四叔壤、協(xié)議標(biāo)準(zhǔn)化

符合其用途
促進(jìn)貿(mào)易瞎饲、交流和技術(shù)轉(zhuǎn)讓
簡(jiǎn)化以提高可用性
規(guī)定一類設(shè)備必須能夠執(zhí)行的任務(wù)或者描述一個(gè)裝置和它的安全特征。

五炼绘、協(xié)議工程

協(xié)議工程

1. 協(xié)議工程學(xué)用形式化方法描述協(xié)議設(shè)計(jì)和維護(hù)中的各個(gè)過程嗅战。

2. 協(xié)議工程過程

集成化、形式化的協(xié)議開發(fā)過程饭望。

• 集成化
  協(xié)議描述仗哨、驗(yàn)證、實(shí)現(xiàn)和測(cè)試等技術(shù)前后銜接铅辞。
• 形式化
  指用形式描述技術(shù)FDT貫穿協(xié)議開發(fā)的各個(gè)階段厌漂。

目的：減少協(xié)議開發(fā)過程中潛在的錯(cuò)誤，提高協(xié)議開發(fā)的效率斟珊，促進(jìn)協(xié)議標(biāo)準(zhǔn)化的發(fā)展苇倡。

3. 協(xié)議開發(fā)過程

協(xié)議設(shè)計(jì)、形式描述囤踩、驗(yàn)證旨椒、實(shí)現(xiàn)、測(cè)試堵漱、運(yùn)行

協(xié)議開發(fā)過程

設(shè)計(jì)

根據(jù)協(xié)議的需求說明構(gòu)造協(xié)議的非形式描述文本稱為協(xié)議設(shè)計(jì)综慎。
包括：協(xié)議環(huán)境分析、協(xié)議的功能設(shè)計(jì)勤庐、協(xié)議組織形式的確定示惊、協(xié)議元素的構(gòu)造、協(xié)議文本的編制等愉镰。
遵循原則：結(jié)構(gòu)化米罚、模塊化等。
結(jié)果：非形式描述協(xié)議文本丈探。

形式描述

形式描述模型：
1. 有限狀態(tài)機(jī)FSM
2. Petri網(wǎng)
形式描述語言：
CCITT制定的SDL

驗(yàn)證

兩項(xiàng)工作：

1.在語法和語義方面進(jìn)行驗(yàn)證
2.進(jìn)行計(jì)算機(jī)模擬

驗(yàn)證的主要內(nèi)容：

1.可達(dá)性分析
2.死鎖和活鎖檢測(cè)
3.協(xié)議的有界性和完整性檢查
4.協(xié)議的動(dòng)作序列檢查
5.通道溢出檢查等

驗(yàn)證方法：

1.模型檢查
最常見方法：可達(dá)性分析录择。包括狀態(tài)窮舉、狀態(tài)隨機(jī)枚舉、狀態(tài)概率枚舉等方法隘竭。
2.證明：推理演算塘秦，嚴(yán)密證明
3.模擬：通過模擬試驗(yàn)測(cè)試協(xié)議的各種性質(zhì)

實(shí)現(xiàn)

協(xié)議實(shí)現(xiàn)是指由協(xié)議規(guī)范到協(xié)議的可執(zhí)行目標(biāo)代碼的過程
協(xié)議實(shí)現(xiàn)的自動(dòng)化：協(xié)議工程的主要目的之一。
通過形式化描述技術(shù)可實(shí)現(xiàn)半自動(dòng)化货裹。步驟：
1.利用翻譯程序?qū)f(xié)議的形式描述文本轉(zhuǎn)換成與機(jī)器無關(guān)的源代碼
2.手工編寫與機(jī)器有關(guān)的嗤形、在協(xié)議規(guī)范中沒有描述的問題的處理代碼精偿。

測(cè)試

驗(yàn)證一個(gè)協(xié)議的實(shí)現(xiàn)弧圆，主要考慮：
1.協(xié)議一致性測(cè)試
1.1 檢測(cè)新協(xié)議實(shí)現(xiàn)是否能滿足該協(xié)議規(guī)范所規(guī)定的規(guī)則。
1.2 如果協(xié)議實(shí)現(xiàn)不能通過一致性測(cè)試笔咽，則說明該協(xié)議實(shí)現(xiàn)與其他同樣通過一致性測(cè)試的協(xié)議實(shí)現(xiàn)不能在同一個(gè)全局系統(tǒng)中很好地協(xié)調(diào)工作搔预。
1.3 一致性測(cè)試的基礎(chǔ)：FDT
1.4 一致性測(cè)試要解決的問題：
-> 測(cè)試系統(tǒng)設(shè)計(jì)
測(cè)試方法和測(cè)試系統(tǒng)體系結(jié)構(gòu)
-> 測(cè)試序列的產(chǎn)生
“徹底性”、“標(biāo)準(zhǔn)化”叶组。測(cè)試序列的自動(dòng)生成和形式化描述拯田。
1.5 測(cè)試序列生成器
可以產(chǎn)各種可能發(fā)生的情況組合，測(cè)試所實(shí)現(xiàn)的協(xié)議是否在各種正常和非正常情況下均能正確工作甩十。
2.對(duì)協(xié)議實(shí)現(xiàn)的評(píng)價(jià)船庇。
要求：
1.徹底性 須徹底測(cè)試所實(shí)現(xiàn)的協(xié)議
2.標(biāo)準(zhǔn)化 使用的測(cè)試集須是標(biāo)準(zhǔn)的

性能

主要包括吞吐量和時(shí)延
目的：
改善協(xié)議機(jī)制，提高執(zhí)行效率侣监。

協(xié)議維護(hù)

六鸭轮、思考題

1.“軟件工程”和“協(xié)議工程”的關(guān)系。
區(qū)別：
協(xié)議工程比軟件工程更加一體化橄霉，形式化窃爷。協(xié)議工程的目的是減少協(xié)議開發(fā)過程中潛在的錯(cuò)誤，提高協(xié)議開發(fā)效率姓蜂，促進(jìn)協(xié)議標(biāo)準(zhǔn)化的發(fā)展按厘。
協(xié)議工程的開發(fā)過程包括：
設(shè)計(jì)，描述钱慢，驗(yàn)證逮京，實(shí)現(xiàn)，性能分析和測(cè)試
軟件工程的開發(fā)過程包括：
可行性分析束莫，需求分析懒棉，概要設(shè)計(jì)，詳細(xì)設(shè)計(jì)麦箍，具體開發(fā)漓藕。
聯(lián)系：
協(xié)議工程和軟件工程都是為了簡(jiǎn)化開發(fā)過程，協(xié)議工程時(shí)以協(xié)議軟件為研究對(duì)象的軟件工程挟裂。
2.選擇一個(gè)網(wǎng)絡(luò)協(xié)議享钞，說明該協(xié)議的三要素。

第二章 協(xié)議設(shè)計(jì)

一、兩種標(biāo)準(zhǔn)

1. OSI/RM

法律上的國際標(biāo)準(zhǔn)——開放系統(tǒng)互聯(lián)參考模型栗竖，并沒有得到市場(chǎng)的認(rèn)可暑脆。只要遵循OSI標(biāo)準(zhǔn)，一個(gè)系統(tǒng)就可以和位于世界上任何地方的狐肢、也遵循這同一標(biāo)準(zhǔn)的其他任何系統(tǒng)進(jìn)行通信添吗。

1.1 各層基本功能

ISO/OSI各層基本功能

1.2 OSI失敗的原因

1. OSI的專家們?nèi)狈?shí)際經(jīng)驗(yàn)，他們?cè)谕瓿蒓SI標(biāo)準(zhǔn)時(shí)缺乏商業(yè)驅(qū)動(dòng)力份名；
2. OSI的協(xié)議實(shí)現(xiàn)起來過于復(fù)雜碟联，而且運(yùn)行效率很低；
3. OSI標(biāo)準(zhǔn)的制定周期太長(zhǎng)僵腺，因而使得OSI標(biāo)準(zhǔn)生產(chǎn)的設(shè)備無法及時(shí)進(jìn)入市場(chǎng)鲤孵；
4. OSI的層次劃分不太合理，有些功能在多個(gè)層次中重復(fù)出現(xiàn)辰如。

2. TCP/IP

非國際標(biāo)準(zhǔn)普监，但常被稱為事實(shí)上的國際標(biāo)準(zhǔn)。

2.1 TCP/IP各層對(duì)應(yīng)的主要協(xié)議

TCP/IP各層及主要協(xié)議

2.2 IP數(shù)據(jù)包的轉(zhuǎn)發(fā)過程

整體情況

個(gè)別情況

兩個(gè)路由器的IP地址并不出現(xiàn)在IP數(shù)據(jù)報(bào)的首部中夺饲，路由器只根據(jù)目的站的IP地址的網(wǎng)絡(luò)號(hào)進(jìn)行路由選擇

路由情況

二奸汇、為什么要分層

1. 分層的好處

• 各層之間是獨(dú)立的
  由于每一層只實(shí)現(xiàn)一種相對(duì)獨(dú)立的功能，因而可將一個(gè)難以處理的復(fù)雜問題分解為若干個(gè)較容易處理的往声、更小一些的問題擂找。這樣，整個(gè)問題的復(fù)雜程度就下降了浩销。
  某一層并不需要知道它的下一層是如何實(shí)現(xiàn)的贯涎，而僅僅需要知道該層通過層間的接口所提供的服務(wù)。
• 靈活性好
  當(dāng)任何一層發(fā)生變化時(shí)慢洋，只要層間接口關(guān)系保持不變塘雳，則在這層以上或以下的各層均不受影響。故易于擴(kuò)充或者改變協(xié)議普筹。
• 結(jié)構(gòu)上可分割開
  各層可以采用最合適的技術(shù)來實(shí)現(xiàn)
• 易于實(shí)現(xiàn)和維護(hù)
  因?yàn)檎麄€(gè)的系統(tǒng)已被分解為若干個(gè)相對(duì)獨(dú)立的子系統(tǒng)败明，使得實(shí)現(xiàn)和調(diào)試變得容易。
• 能促進(jìn)標(biāo)準(zhǔn)化工作
  因?yàn)槊恳粚拥墓δ芗捌渌峁┑姆?wù)都已有了精確的說明太防。

2. 不分層的后果

如果不分層妻顶，每一個(gè)新的應(yīng)用程序都必須為每個(gè)網(wǎng)絡(luò)重新實(shí)現(xiàn)一次。

三、OSI模型的核心

服務(wù)讳嘱、接口幔嗦、協(xié)議

• Service – says what a layer does
  指某一層向上一層提供的一組原語(操作)，一個(gè)服務(wù)由一組原語正式說明沥潭，用戶進(jìn)程通過這些原語來訪問服務(wù)
  定義了該層準(zhǔn)備代表其用戶執(zhí)行哪些操作邀泉，但不涉及如何實(shí)現(xiàn)這些操作
• Interface – says how to access the service
  規(guī)定了有哪些參數(shù)，以及結(jié)果是什么
• Protocol – says how is the service implemented
  一組規(guī)則钝鸽，規(guī)定了同一層的對(duì)等實(shí)體之間所交換的數(shù)據(jù)包或者報(bào)文的格式和含義汇恤。
  對(duì)等實(shí)體利用協(xié)議來實(shí)現(xiàn)他們的服務(wù)定義，可以自由改變協(xié)議寞埠，只要不改變呈現(xiàn)給他們的用戶的服務(wù)即可屁置。

服務(wù)與協(xié)議是完全分離的焊夸，服務(wù)涉及層與層之間的接口仁连，協(xié)議涉及不同機(jī)器上兩個(gè)對(duì)等實(shí)體之間發(fā)送的數(shù)據(jù)包

四、n層協(xié)議模型

協(xié)議模型

• 相關(guān)概念
  實(shí)體阱穗、（n）服務(wù)饭冬、（n）用戶搀崭、SP熊响、SAP、TSAP轨功、NSAP

1. 實(shí)體

在OSI中鲁僚，實(shí)體(entity)表示任何可以發(fā)送和接收信息的硬件或軟件進(jìn)程炊苫。在許多情況下，實(shí)體就是一個(gè)特定的模塊冰沙。

2. SP-服務(wù)原語

在進(jìn)行交互時(shí)所要交換的一些必須信息或命令侨艾，以表明需要本地的或遠(yuǎn)端的對(duì)等實(shí)體做什么事情。

• 4種服務(wù)原語
  Request (請(qǐng)求): 一個(gè)實(shí)體希望得到某種服務(wù)
  Indication (指示)：把關(guān)于某一事件的信息告訴某一實(shí)體
  Response (響應(yīng))：一個(gè)實(shí)體愿意響應(yīng)某一事件
  Confirm (證實(shí))：把一個(gè)實(shí)體的服務(wù)請(qǐng)求加以確認(rèn)并告訴它

3. SAP-服務(wù)訪問點(diǎn)

同一系統(tǒng)相鄰兩層的實(shí)體進(jìn)行交互的地方拓挥。服務(wù)用戶通過在一個(gè)SAP遞交數(shù)據(jù)并從另一個(gè)SAP讀出唠梨。

• TSAP-傳輸服務(wù)訪問點(diǎn)（端口）
• NSAP-網(wǎng)絡(luò)服務(wù)訪問點(diǎn)（例如IP地址）

4. 服務(wù)

一個(gè)(n)實(shí)體向上一層所提供的服務(wù)由以下三部分構(gòu)成：
(1) (n)實(shí)體自己提供的某些功能。
(2) 通過與處在另一系統(tǒng)中的對(duì)等(n)實(shí)體的通信而得到的服務(wù)侥啤。
(3) 從(n-1)層及其以下各層以及本地系統(tǒng)環(huán)境得到的服務(wù)当叭。

服務(wù)與協(xié)議：
本層的服務(wù)用戶只能看見服務(wù)而無法看見下面的協(xié)議。下面的協(xié)議對(duì)上面的服務(wù)用戶是透明的盖灸。
協(xié)議是“水平的”蚁鳖，即協(xié)議是控制對(duì)等實(shí)體之間通信的規(guī)則。
服務(wù)是“垂直的”赁炎，即服務(wù)是由下層向上層通過層間接口提供的醉箕。
“透明”-指存在但看不見的事物
“虛擬”-指看起來存在但實(shí)際上不存在的事物

5. 協(xié)議數(shù)據(jù)單元PDU

將(n)層對(duì)等實(shí)體之間，為實(shí)現(xiàn)該層協(xié)議所交換的信息單元稱為協(xié)議數(shù)據(jù)單元PDU (Protocol Data Unit)。通常將第n層的協(xié)議數(shù)據(jù)單元記為(n)PDU琅攘。

• 組成
  PDU通常由用戶數(shù)據(jù)和協(xié)議控制信息PCI組成
  PCI一般作為首部加在用戶數(shù)據(jù)的前面垮庐，有時(shí)也可作為尾部加在用戶數(shù)據(jù)后，如檢驗(yàn)和坞琴。
• 類型
  1.數(shù)據(jù)PDU
  2.控制PDU哨查，不攜帶用戶數(shù)據(jù)
• 不同的協(xié)議層次的PDU表示法
  1.物理層：比特(bit)；
  2.數(shù)據(jù)鏈路層：幀(frame)或信元(cell)剧辐；
  3.網(wǎng)絡(luò)層 ：分組或包(packet)
  4.運(yùn)輸層 ：分段(segment)寒亥、數(shù)據(jù)報(bào)(datagram)
  5.應(yīng)用層：消息(message)

6. 服務(wù)數(shù)據(jù)單元SDU

OSI將層與層之間交換的數(shù)據(jù)的單元稱為服務(wù)數(shù)據(jù)單元SDU。
一個(gè)(n)服務(wù)數(shù)據(jù)單元就是(n)服務(wù)所要傳送的邏輯數(shù)據(jù)單元荧关。

PDU與SDU的區(qū)別與聯(lián)系：
SDU就是數(shù)據(jù)PDU中的用戶數(shù)據(jù)溉奕，但不一定是一一對(duì)應(yīng)關(guān)系。
可以是多個(gè)SDU合成為一個(gè)PDU(稱為“拼裝”)忍啤，也可以是將一個(gè)SDU劃分為幾個(gè)PDU(稱為“分段”)加勤。

PDU和SDU

7. 通道

N層中任何兩個(gè)協(xié)議實(shí)體通過(n-1)SAP所形成的邏輯數(shù)據(jù)通路稱為(n-1)層通道。

n層協(xié)議的通信環(huán)境：

1.用戶應(yīng)用要求
2.(n-1)層通道(Channel)的性質(zhì)
3.n層協(xié)議運(yùn)行時(shí)的操作系統(tǒng)和硬件環(huán)境

通道的類型：

1.空通道-報(bào)文的發(fā)送時(shí)間和延遲時(shí)間為0的通道
2.非緩沖通道-通道中 最多只有一個(gè)正在傳送中的報(bào)文
3.緩沖通道-允許有多個(gè)報(bào)文停留的通道

通道性質(zhì)：

(n-1)層通道的性質(zhì)對(duì)n層協(xié)議的構(gòu)成有非常重要的影響

1.通道的形成方式：

A和B建立并獨(dú)占一條連接同波，此時(shí)(n-1)層應(yīng)提供有連接服務(wù)
A和B與其它協(xié)議實(shí)體一起共享一條連接
A和B利用(n-1)層提供的無連接服務(wù)進(jìn)行通信
如果(n-1)層為物理層鳄梅，A和B可獨(dú)占一條物理信道，或共享一條物理信道

2.通道的隊(duì)列性質(zhì)：

除物理層外未檩，一般可將(n-1)層通道看作是隊(duì)列通道戴尸。
即一個(gè)數(shù)據(jù)報(bào)文從n層源端協(xié)議實(shí)體發(fā)出之后要在n層以下各層多次存貯轉(zhuǎn)發(fā)，在每個(gè)存貯轉(zhuǎn)發(fā)處就存在一個(gè)隊(duì)列冤狡。
隊(duì)列的主要性質(zhì)是平均隊(duì)列長(zhǎng)度以及最大隊(duì)列允許長(zhǎng)度孙蒙。
隊(duì)列越長(zhǎng)，那么數(shù)據(jù)報(bào)文在通道中的時(shí)延就會(huì)越大悲雳；
如果隊(duì)列長(zhǎng)度達(dá)到最大允許長(zhǎng)度挎峦，那么后續(xù)的數(shù)據(jù)報(bào)文將會(huì)丟失 。

3.回程時(shí)延RTT

RTT是從n層源端實(shí)體發(fā)出報(bào)文到該報(bào)文的確認(rèn)信息到達(dá)該實(shí)體之間的時(shí)間間隔怜奖，它包括目標(biāo)實(shí)體收到報(bào)文之后浑测，對(duì)報(bào)文進(jìn)行處理然后發(fā)出確認(rèn)信息的時(shí)間。

時(shí)延的產(chǎn)生

4.差錯(cuò)特性

• 參數(shù)：
  報(bào)文的出錯(cuò)率歪玲、報(bào)文的丟失率迁央、報(bào)文的重復(fù)率、報(bào)文失序率
• 差錯(cuò)特性與它的形成方式有關(guān)：
  1.如果通道是利用(n-1)層的有連接服務(wù)形成的滥崩，那么傳遞的報(bào)文不會(huì)失序岖圈；
  2.如果通道是利用(n-1)層的無連接服務(wù)形成的，或是物理信道钙皮，則報(bào)文的順序就有可能失序蜂科。

5.可靠性

通道的可靠性是指通道無故障顽决，如連接中斷、復(fù)位等导匣。

6.報(bào)文的最大長(zhǎng)度或最大傳輸單元MTU

通道所能接收的最大報(bào)文長(zhǎng)度才菠。主要影響n層協(xié)議的報(bào)文分段、拼接等功能贡定。

7.工作方式

-單工赋访、半雙工、全雙工
-同步與異步

8.通信方式

1. 點(diǎn)對(duì)點(diǎn)-任意兩個(gè)N 層協(xié)議實(shí)體利用一條(N - 1)層通道通信缓待，協(xié)同完成指定協(xié)議功能蚓耽。如TCP連接，UDP點(diǎn)對(duì)點(diǎn)方式旋炒。
2. 點(diǎn)對(duì)多點(diǎn)-任意兩個(gè)以上N 層協(xié)議實(shí)體利用多條(N - 1)層通道通信步悠，協(xié)同執(zhí)行一定的任務(wù)。如ATM的點(diǎn)對(duì)多點(diǎn)連接瘫镇，UDP的廣播方式鼎兽。

9.安全性

對(duì)用戶數(shù)據(jù)加密和安全控制（如口令、權(quán)限）

10.通道的帶寬

通信線路的帶寬也稱通頻帶汇四，用頻率來度量接奈。
通道的帶寬可進(jìn)一步分為前向帶寬、后向帶寬通孽、峰值帶寬等。

五睁壁、協(xié)議提供的服務(wù)

1. 面向連接的服務(wù)

• 三個(gè)階段：
  連接建立背苦、數(shù)據(jù)傳輸和連接釋放
• 在傳送數(shù)據(jù)時(shí)是按序傳送的
• 比較適合于在一定期間內(nèi)要向同一目的地發(fā)送許多報(bào)文的情況
• 網(wǎng)絡(luò)層：虛電路服務(wù)
• 永久虛電路：適于兩個(gè)用戶需要經(jīng)常進(jìn)行頻繁的

2. 無連接的服務(wù)

• 不能保證報(bào)文的丟失、重復(fù)潘明、失序
• 三種類型：
  1.數(shù)據(jù)報(bào)-不需要接收端做任何響應(yīng)
  2.證實(shí)交付（可靠的數(shù)據(jù)報(bào)）-對(duì)每一個(gè)報(bào)文產(chǎn)生一個(gè)證實(shí)給發(fā)放用戶行剂，這個(gè)證實(shí)來自提供服務(wù)的層。
  3.請(qǐng)求應(yīng)答-收端用戶每收到一個(gè)報(bào)文钳降，就向發(fā)端用戶發(fā)送一個(gè)應(yīng)答報(bào)文厚宰。始于“事務(wù)”中的通信。
• 適于傳送少量零星的報(bào)文

3. 思考題

1. 面向連接的服務(wù)和無連接服務(wù)的選擇遂填。
   答：
   強(qiáng)調(diào)數(shù)據(jù)傳輸?shù)耐暾圆酢⒖煽啃院涂煽刂菩詴r(shí)，選擇面向連接的服務(wù)吓坚。
   強(qiáng)調(diào)數(shù)據(jù)傳輸性能時(shí)撵幽，選擇無連接的服務(wù)。
2. HTTP協(xié)議利用有連接的TCP作為傳輸通道礁击，并不斷建立連接和斷開連接盐杂。這樣做的好處與壞處分別是什么逗载。
   答：
   好處：管理簡(jiǎn)單，存在的連接都是有用的連接链烈。一定程度保證完整性厉斟、可靠性。
   壞處：如果請(qǐng)求過于頻繁强衡，將在TCP的建立與關(guān)閉上浪費(fèi)時(shí)間和帶寬捏膨。

六、協(xié)議功能

（N）層協(xié)議為了向上一層提供服務(wù)食侮，必須實(shí)現(xiàn)一定的功能号涯。

1. 基本的協(xié)議功能的類型

• 連接管理
• 數(shù)據(jù)交換
  --
• 差錯(cuò)控制
• 流量控制
• 擁塞控制

1.1 連接管理

兩種連接：

點(diǎn)對(duì)點(diǎn)、點(diǎn)對(duì)多點(diǎn)

三種主要功能：

連接建立

雙方協(xié)商工作參數(shù)：初始序號(hào)
信用量锯七、QoS链快。協(xié)商失敗則連接建立失敗。

連接釋放

突然釋放-立即關(guān)閉
文明釋放-成功發(fā)送所有數(shù)據(jù)后關(guān)閉

連接維護(hù)

如Keep-alive查詢眉尸、參數(shù)變更等域蜗。

針對(duì)延遲的保護(hù)措施：

• 如TCP三次握手機(jī)制
• 基于時(shí)鐘的連接管理方法

1.2 數(shù)據(jù)交換

數(shù)據(jù)的發(fā)送與接收：

• n層協(xié)議接收n層用戶遞交的(n)SDU，將之轉(zhuǎn)換成(n)PDU噪猾，從(n-1)層通道發(fā)送出去霉祸；
• 反之，它接收(n-1)層通道的(n)PDU袱蜡，提取其中的(n)SDU丝蹭，將之轉(zhuǎn)交給n層用戶。

協(xié)議支持的用戶數(shù)據(jù)坪蚁、類型：

塊數(shù)據(jù)奔穿、流數(shù)據(jù)、批數(shù)據(jù)敏晤、優(yōu)先數(shù)據(jù)贱田、帶外數(shù)據(jù)、緊急數(shù)據(jù)嘴脾、編碼數(shù)據(jù)男摧。

實(shí)現(xiàn)數(shù)據(jù)傳輸?shù)淖庸δ埽?/h5>

• 對(duì)齊
• 分段和合段
• 拼裝和分離
• PDU的裝配與拆裝（封裝/解封裝）
• SDU編碼與解碼
• 加校驗(yàn)和
  以（n）數(shù)據(jù)的全部或部分作為輸入，產(chǎn)生一個(gè)固定大小的校驗(yàn)和作為輸出译打。
• 抖動(dòng)補(bǔ)償
  使得協(xié)議能接受任何類型的通信量模式的SDU數(shù)據(jù)流作為輸入耗拓，產(chǎn)生一個(gè)連續(xù)的SDU流作為輸出。
• 帶外數(shù)據(jù)扶平、緊急數(shù)據(jù)的發(fā)送和接收

1.3 差錯(cuò)控制

差錯(cuò)：丟失帆离、重復(fù)、亂序等结澄。
(n-1)通道提供的數(shù)據(jù)通道的可靠性越高哥谷，則n層協(xié)議需實(shí)現(xiàn)的差錯(cuò)控制機(jī)制則越少岸夯。

• 序號(hào)
• 確認(rèn)
• 計(jì)時(shí)器
• 重傳

序號(hào)：

序號(hào)是確認(rèn)和重傳的基礎(chǔ)，此外序號(hào)可用于流量控制们妥。

1）三種不同的產(chǎn)生方式

• SDU序號(hào)
  對(duì)每個(gè)SDU都編號(hào)猜扮，從SDU序號(hào)得到PDU的序號(hào)。若某個(gè)SDU被分段攜帶在多個(gè)PDU中监婶，應(yīng)附加一個(gè)SDU分段號(hào)旅赢。
• PDU序號(hào)
  對(duì)PDU連續(xù)編號(hào)，不管它們攜帶的SDU的數(shù)據(jù)量惑惶。
• 字節(jié)序號(hào)
  對(duì)SDU的每個(gè)字節(jié)編號(hào)煮盼。PDU的序號(hào)來自與它所攜帶的SDU的第一個(gè)字節(jié)序號(hào)和最后一個(gè)字節(jié)的序號(hào)。

2）如何防止序號(hào)重復(fù)

使用一個(gè)非常大的序號(hào)空間带污。
使得在數(shù)據(jù)單元從一端到另一端的最大可能延遲時(shí)間L內(nèi)僵控，所有從源點(diǎn)發(fā)送出去的新數(shù)據(jù)單元都有不同的序號(hào)。

3）序號(hào)空間的大小與信道特點(diǎn)鱼冀、確認(rèn)方法报破、流量控制方法和PDU中的數(shù)據(jù)字段長(zhǎng)度有關(guān)

• 如果信道的質(zhì)量比較好，則序號(hào)空間要求比較大千绪，從而可以連續(xù)發(fā)送多個(gè)數(shù)據(jù)單元充易，提高協(xié)議效率
• 采用周期性確認(rèn)，序號(hào)空間就不一定要很大
• 在停止等待協(xié)議中荸型，只需要0和1兩個(gè)序號(hào)即可
• 一般來說盹靴，序號(hào)空間的大小與數(shù)據(jù)字段的長(zhǎng)度成反比

確認(rèn)：

接收者顯式地通知發(fā)送者所發(fā)送的數(shù)據(jù)的接受情況

1） 被確認(rèn)的對(duì)象

• PDU
• 字節(jié)

2）確認(rèn)的情況

• 已正確到達(dá)
• 還沒有收到
• 收到但有錯(cuò)

3）確認(rèn)分為三種類型

• 肯定確認(rèn)（Ack）
• 否定確認(rèn)（Nak）
• 選擇確認(rèn)（Select Ack）
  指示收到的和沒收到的PDU

4）兩種發(fā)送方式

在一種協(xié)議中，通常兩種確認(rèn)形式并存帆疟。

• 獨(dú)立確認(rèn)
  使用一個(gè)確認(rèn)PDU來攜帶確認(rèn)信息鹉究。可隨時(shí)發(fā)送踪宠。
• 應(yīng)答攜帶
  將確認(rèn)信息放在數(shù)據(jù)PDU中發(fā)送，可提高協(xié)議效率妈嘹，要求接收方有數(shù)據(jù)發(fā)送時(shí)才能發(fā)送確認(rèn)柳琢。

5）如何標(biāo)識(shí)被確認(rèn)的對(duì)象

用被確認(rèn)的數(shù)據(jù) PDU或字節(jié)的序號(hào)來標(biāo)識(shí)

6）累計(jì)確認(rèn)

如果否定確認(rèn)或肯定確認(rèn)的語義是表示所給定的序號(hào)之前的所有序號(hào)(包括或不包括本序號(hào))的數(shù)據(jù)PDU都已被成功地接收了，則該確認(rèn)又稱為累計(jì)確認(rèn)润脸。

計(jì)時(shí)器：

檢測(cè)數(shù)據(jù)PDU柬脸、確認(rèn)PDU或重傳請(qǐng)求信號(hào)的丟失。

1）超時(shí)值的設(shè)置

• 依賴于PDU的往返時(shí)間RTT
• 使用算法毙驯，動(dòng)態(tài)估計(jì)往返時(shí)間和定時(shí)值

2）計(jì)時(shí)器超時(shí)值設(shè)置不當(dāng)會(huì)導(dǎo)致什么后果倒堕？

如果超時(shí)值設(shè)置太短，連續(xù)大量的數(shù)據(jù)重傳爆价，嚴(yán)重情況下將加劇網(wǎng)絡(luò)的擁塞程度垦巴，出現(xiàn)更多數(shù)據(jù)丟失 媳搪；
如果超時(shí)值設(shè)置太長(zhǎng)，出現(xiàn)數(shù)據(jù)丟失而得不到及時(shí)糾正骤宣，也會(huì)降低協(xié)議的性能秦爆。

3）TCP協(xié)議中的計(jì)時(shí)器

• 重傳計(jì)時(shí)器
• 堅(jiān)持計(jì)時(shí)器
• 保活計(jì)時(shí)器
• 時(shí)間等待計(jì)時(shí)器

重傳：

發(fā)送者重傳：

• 由確認(rèn)PDU所指出的數(shù)據(jù)PDU
• 重傳計(jì)時(shí)器超時(shí)仍未收到確認(rèn)的數(shù)據(jù)PDU

1）基于滑動(dòng)窗口的重傳方法

• 回退n幀
  接收方直接地丟棄所有不按序到達(dá)的數(shù)據(jù)PDU憔披。
  發(fā)送方從第一個(gè)否定的確認(rèn)或發(fā)生超時(shí)的時(shí)刻所指出的數(shù)據(jù)PDU的序號(hào)開始等限，重傳所有后續(xù)數(shù)據(jù)PDU。

• 選擇重傳
  發(fā)送方只重傳否定確認(rèn)芬膝、選擇確認(rèn)和超時(shí)的時(shí)刻所指出的那些數(shù)據(jù)PDU

1.4 流量控制

指“接收端控制發(fā)送端的數(shù)據(jù)發(fā)送速率以消除接收端緩存溢出的可能性望门，并使網(wǎng)絡(luò)不致過載”

1）為什么使用流量控制？

• 接收方接受能力有限
• 緩存不夠
• 處理能力不夠

2）舉例

• 停等協(xié)議
• 滑動(dòng)窗口

1.5 擁塞控制

在某段時(shí)間锰霜，若對(duì)網(wǎng)絡(luò)中某一資源（鏈路容量筹误、交換節(jié)點(diǎn)中的緩沖區(qū)、處理機(jī)）的需求超過了網(wǎng)絡(luò)所能提供的可用部分锈遥，網(wǎng)絡(luò)的性能就要降低纫事。這種情況就叫做擁塞(congestion)。

1）擁塞控制的主要功能

• 防止網(wǎng)絡(luò)因過載二引起吞吐量下降和延遲增加
• 在互相競(jìng)爭(zhēng)的各用戶之間公平地分配資源
• 避免死鎖：直接死鎖所灸，重裝死鎖
  直接死鎖-由互相占用了對(duì)方需要地資源而造成地死鎖丽惶。
  重裝死鎖-由于分組不完整無法交付給主機(jī)產(chǎn)生地死鎖。

2）擁塞控制與流量控制地區(qū)別和聯(lián)系

區(qū)別：
流量控制只在一對(duì)給定的發(fā)送方和接收方之間爬立，控制發(fā)送方以不超過接收方處理能力的速率發(fā)送數(shù)據(jù)钾唬。
擁塞控制是一個(gè)全局性的過程，涉及到網(wǎng)絡(luò)中所有的主機(jī)侠驯、所有的路由器抡秆，以及與降低網(wǎng)絡(luò)傳輸性能有關(guān)的所有因素。

聯(lián)系：
流量控制限制了進(jìn)入網(wǎng)絡(luò)中地信息總量吟策，可以在一定程度上減緩擁塞地作用儒士。

2. 其他功能

• 無活動(dòng)控制
• 通信量（流量）監(jiān)控
• 通信量填充（防止通信量分析）
• 通信量整形
• 路由選擇
• 媒體訪問控制

七、協(xié)議元素

協(xié)議三要素

語法檩坚、語義着撩、同步

協(xié)議的主體

狀態(tài)-事件轉(zhuǎn)換機(jī)制

協(xié)議六元素

并不是所有協(xié)議都必須包含以下六種元素。多個(gè)協(xié)議功能組成一個(gè)完整的協(xié)議之后匾委，這六種元素一般使必須的拖叙。

元素之間的有機(jī)聯(lián)系：在什么協(xié)議狀態(tài)下，在什么輸入事件驅(qū)動(dòng)下赂乐，調(diào)用什么協(xié)議過程薯鳍；協(xié)議過程在什么條件下(謂詞)，采取什么協(xié)議動(dòng)作(操作)挨措，輸出什么事件或修改哪些協(xié)議狀態(tài)和變量挖滤。
在上述元素中崩溪，通常用狀態(tài)變遷表或狀態(tài)轉(zhuǎn)換圖來描述協(xié)議的狀態(tài)、事件壶辜、操作和謂詞悯舟。

• 服務(wù)原語和服務(wù)原語時(shí)序
• 協(xié)議數(shù)據(jù)單元PDU和PDU交換時(shí)序
• 協(xié)議狀態(tài)
• 協(xié)議事件
• 協(xié)議變量
• 協(xié)議操作和謂詞

1. 服務(wù)原語及其時(shí)序

一般用服務(wù)規(guī)范(Service Specification)來定義和描述N層協(xié)議向外部所提供的服務(wù)。
服務(wù)規(guī)范定義了服務(wù)用戶和服務(wù)提供者之間的交互作用的規(guī)則砸民，包括：服務(wù)原語和服務(wù)原語時(shí)序抵怎。
N 層協(xié)議的服務(wù)原語和原語參數(shù)詳細(xì)準(zhǔn)確地描述了N層協(xié)議和它的服務(wù)用戶之間的接口。

1）根據(jù)服務(wù)原語對(duì)服務(wù)的分類：

1.需要證實(shí)的服務(wù)
2.不需要證實(shí)的服務(wù)

2）一個(gè)完整的服務(wù)原語通常包括

原語名字岭参、原語類型反惕、原語參數(shù)

原語

2. PDU及其時(shí)序

N層協(xié)議的PDU從語法和語義上詳細(xì)準(zhǔn)確地定義了n層協(xié)議實(shí)體之間交換的信息（PDU編碼格式/協(xié)議使用的詞匯表）。

3. 協(xié)議狀態(tài)

• 局部狀態(tài)：?jiǎn)蝹€(gè)協(xié)議實(shí)體在某時(shí)刻的執(zhí)行情況
• 全局狀態(tài)：參與執(zhí)行某種協(xié)議功能的所有協(xié)議實(shí)體的狀態(tài)總和演侯。包括（n-1)層通道姿染。

N層協(xié)議必須定義所有的協(xié)議狀態(tài)。

4. 協(xié)議事件

1）根據(jù)用途分類

• 輸入事件
  a.收到一個(gè)PDU
  b.收到n層服務(wù)用戶的一條服務(wù)原語
  c.內(nèi)部事件（如計(jì)時(shí)器超時(shí)）
• 輸出事件
  a.發(fā)送一個(gè)PDU
  b.向n層服務(wù)用戶發(fā)出一條服務(wù)原語

2）根據(jù)事件的作用范圍分類

• 通信事件
  收發(fā)服務(wù)原語或收發(fā)PDU秒际，又可分為同步事件和異步事件悬赏。
• 內(nèi)部事件：如計(jì)時(shí)器超時(shí)。

3）協(xié)議事件的三個(gè)性質(zhì)

• 成對(duì)性
  指一個(gè)事件的發(fā)生總是伴隨著另一個(gè)事件的發(fā)生娄徊。通信事件成對(duì)闽颇，內(nèi)部事件不成對(duì)。
• 原子性
  指事件要么不發(fā)生寄锐，一旦發(fā)生就一定完成兵多。
  具有原子性的事件被稱為原子事件。
• 時(shí)序性
  指發(fā)生的事件在時(shí)間上是有先后順序的橄仆。
  事件時(shí)序性決定了狀態(tài)的時(shí)序性剩膘。

5. 協(xié)議變量

保存協(xié)議運(yùn)行的歷史數(shù)據(jù)、運(yùn)行參數(shù)的變量盆顾，以及協(xié)議機(jī)制本身所設(shè)置的變量怠褐。

常見的協(xié)議變量：

• 發(fā)送序號(hào)變量
• 接受序號(hào)變量
• 重發(fā)時(shí)間間隔變量

6. 協(xié)議操作和謂詞

每種協(xié)議功能都是通過一組協(xié)議過程的執(zhí)行來實(shí)現(xiàn)的。
協(xié)議過程：協(xié)議在輸入事件的驅(qū)動(dòng)下您宪，在一定條件下惫搏，執(zhí)行一系列的操作或動(dòng)作。

一定條件：
這些約束條件涉及協(xié)議參數(shù)蚕涤、協(xié)議變量、協(xié)議運(yùn)行環(huán)境等铣猩。將描述這些約束條件的語句稱之為謂詞(predicate)揖铜。

這些操作包括：
-產(chǎn)生輸出事件
-清楚和設(shè)置計(jì)時(shí)器
-修改協(xié)議變量
-改變協(xié)議狀態(tài)

原子過程：
原子過程包含多個(gè)協(xié)議操作，并且過程一旦啟動(dòng)之后达皿，所有包括的操作一次性完成天吓，不經(jīng)歷中間協(xié)議狀態(tài)贿肩，不被其它過程打斷。
一般來說龄寞，在協(xié)議運(yùn)行時(shí)汰规，可將它從一個(gè)狀態(tài)到另一個(gè)狀態(tài)的轉(zhuǎn)換處理成原子過程。

八物邑、協(xié)議組織

協(xié)議組織是指將相關(guān)協(xié)議功能和協(xié)議元素組成一個(gè)完整協(xié)議的過程溜哮。

這個(gè)過程涉及以下技術(shù)和方法：

• 協(xié)議層次化
• 協(xié)議階段化
• 協(xié)議分類
• 協(xié)議的運(yùn)行方式

1. 協(xié)議層次化

如果n層協(xié)議的功能和結(jié)構(gòu)仍然很復(fù)雜，可將n層協(xié)議的眾多功能進(jìn)一步分成多個(gè)子層色解。
子層的劃分可使復(fù)雜協(xié)議的結(jié)構(gòu)變得清晰茂嗓，有利于協(xié)議的設(shè)計(jì)、驗(yàn)證科阎、實(shí)現(xiàn)和測(cè)試述吸。但是，子層的劃分可能降低協(xié)議性能锣笨。

2.協(xié)議階段化

可將n層協(xié)議分成多個(gè)運(yùn)行階段蝌矛，每個(gè)階段只涉及到一部分協(xié)議功能。如OSI體系結(jié)構(gòu)的運(yùn)輸層協(xié)議的正常運(yùn)行被分為三個(gè)階段：連接建立階段错英、數(shù)據(jù)傳輸階段入撒、連接釋放階段。

3.協(xié)議分類

由于不同用戶的需求以及協(xié)議的運(yùn)行環(huán)境的不同導(dǎo)致協(xié)議的復(fù)雜性走趋。因此衅金，可以將協(xié)議分成不同類別或不同級(jí)別，每類協(xié)議只適用于特定用戶和特定環(huán)境簿煌，那么復(fù)雜協(xié)議就會(huì)變得簡(jiǎn)單氮唯。

4.運(yùn)行方式

協(xié)議運(yùn)行方式有三種：

• 協(xié)議交替 - n層內(nèi)的多個(gè)協(xié)議或一個(gè)協(xié)議的多個(gè)類別或一個(gè)協(xié)議的多個(gè)協(xié)議功能交替活躍
  可在不同時(shí)間內(nèi)適用于不同用戶和不同通道的協(xié)議環(huán)境。相比并發(fā)和并行性能低。
• 協(xié)議并發(fā) - 同時(shí)活躍，并發(fā)運(yùn)行
  可在同一時(shí)間內(nèi)適用多種協(xié)議環(huán)境
• 協(xié)議并行 - 同時(shí)活躍徐钠，同時(shí)運(yùn)行
  協(xié)議性能更好

九坑傅、協(xié)議文本

協(xié)議文本是協(xié)議設(shè)計(jì)階段的最終結(jié)果。
協(xié)議文本中枚碗，最重要、最主要部分是協(xié)議元素的描述。必須對(duì)每一項(xiàng)協(xié)議元素作出準(zhǔn)確伍玖、清晰、無二義性的定義剿吻。此外窍箍，協(xié)議的各元素是有機(jī)聯(lián)系的，協(xié)議文本應(yīng)清晰表達(dá)這些關(guān)系。

十椰棘、協(xié)議設(shè)計(jì)方法

1. 設(shè)計(jì)原則

• 簡(jiǎn)單
• 模塊化
• 有界性
• 健壯性
• 一致性

其中纺棺，最基本的是：簡(jiǎn)單和模塊化。

2. 分層的原則

• 當(dāng)需要有一個(gè)不同等級(jí)的抽象時(shí)邪狞，就應(yīng)當(dāng)有一個(gè)相應(yīng)的層次
• 每一層的功能應(yīng)當(dāng)是非常明確的
• 選擇的層與層的邊界應(yīng)該使通過這些邊界的信息量盡量地少
• 難點(diǎn)：層次太少會(huì)使每一層協(xié)議太復(fù)雜祷蝌，太多則在描述和綜合各層的系統(tǒng)時(shí)難度較大。

3. 自頂向下的設(shè)計(jì)方法

協(xié)議設(shè)計(jì)方法

第三章 協(xié)議形式化描述技術(shù)

• 有限狀態(tài)機(jī)FSM
• Petri網(wǎng)
• SDL

一帆卓、形式化技術(shù)的產(chǎn)生

過去人么習(xí)慣使用自然語言描述協(xié)議巨朦。
優(yōu)點(diǎn)：方便易懂
缺點(diǎn)：不嚴(yán)格、不精確鳞疲、結(jié)構(gòu)不好罪郊、沒有描述標(biāo)準(zhǔn)、有二義性尚洽。不同的人對(duì)協(xié)議描述的理解不同悔橄。難以進(jìn)行驗(yàn)證、實(shí)現(xiàn)和測(cè)試自動(dòng)化腺毫。

解決辦法：形式化技術(shù)

是將協(xié)議工程各階段在技術(shù)上銜接起來的紐帶癣疟。

形式描述模型FDM

• 狀態(tài)變遷模型：
  有限狀態(tài)機(jī)FSM
  擴(kuò)展的有限狀態(tài)機(jī)EFSM模型
  通信有限狀態(tài)機(jī)CFSM模型
  Carl Adam Petri的Petri網(wǎng)
• 時(shí)態(tài)邏輯TL
• 進(jìn)程代數(shù)：
  通信系統(tǒng)演算CCS（以進(jìn)程代數(shù)為基礎(chǔ)）
  通信順序進(jìn)程CSP（以CCS為基礎(chǔ)）

形式描述語言FDL

• ISO制定的Estelle和LOTOS
• CCITT制定的SDL
  ……

模型與語言

模型：
對(duì)象或系統(tǒng)的抽象（OSI/RM）
描述對(duì)象或系統(tǒng)的方法或技術(shù)（FSM/PetriNet）

形式語言：
具有嚴(yán)格的語法和語義；
可精確潮酒、完全表述協(xié)議的功能及行為睛挚；
以一種或多種數(shù)學(xué)方法或形式模型為基礎(chǔ)。如SDL基于擴(kuò)展的FSM和抽象數(shù)據(jù)類型急黎。

二扎狱、FSM

1. 有限狀態(tài)機(jī)FSM的幾個(gè)概念

狀態(tài)（State）

指的是對(duì)象在其生命周期中的一種狀況，處于某個(gè)特定狀態(tài)中的對(duì)象必然會(huì)滿足某些條件勃教、執(zhí)行某些動(dòng)作或者是等待某些事件淤击。

事件（Event）

指的是在時(shí)間和空間上占有一定位置，并且對(duì)狀態(tài)機(jī)來講是有意義的事情故源。事件通常會(huì)引起狀態(tài)的變遷污抬，促使?fàn)顟B(tài)機(jī)從一種狀態(tài)切換到另一種狀態(tài)。

轉(zhuǎn)換绳军、轉(zhuǎn)移印机、變遷、遷移（Transition）

指的是兩個(gè)狀態(tài)之間的一種關(guān)系门驾，表明對(duì)象將在第一個(gè)狀態(tài)中執(zhí)行一定的動(dòng)作射赛，并將在某個(gè)事件發(fā)生且滿足某個(gè)特定條件時(shí)進(jìn)入第二個(gè)狀態(tài)。

動(dòng)作（Action）

指的是狀態(tài)機(jī)中可以執(zhí)行的原子操作奶是，所謂原子操作指的是它們?cè)谶\(yùn)行的過程中不能被其他消息所中斷咒劲，必須一直執(zhí)行下去顷蟆。

2. 形式化定義

FSM和非確定FSM，可以看成僅接收輸入并發(fā)生狀態(tài)改變腐魂，但無任何輸出的自動(dòng)機(jī)。

FSM的形式化定義

對(duì)于不確定的有限自動(dòng)機(jī)NFA逐纬，其下一時(shí)刻狀態(tài)為一個(gè)狀態(tài)子集蛔屹。

3. Moore機(jī)和Mealy機(jī)

具有輸出的自動(dòng)機(jī)器模型按照輸出的不同分成兩類：

• Moore 機(jī)：輸出與狀態(tài)有關(guān)
• Mealy機(jī)：輸出與狀態(tài)和輸入有關(guān)

Moore機(jī)在接收輸入串的過程中不斷改變狀態(tài)并在每個(gè)狀態(tài)上有字符輸出。
Mealy機(jī)只是在接收輸入串的過程中不斷改變狀態(tài)豁生，并且字符輸出與當(dāng)前狀態(tài)及輸入串有關(guān)兔毒。

有限狀態(tài)機(jī)可看作是Moore機(jī)的一個(gè)特例
Moore機(jī)可看作是Mealy機(jī)的一個(gè)特例

Moore機(jī)FSM形式化定義

Mealy機(jī)FSM形式化定義

4. 如何設(shè)計(jì)FSM

• 理解系統(tǒng)的功能：
  通過系統(tǒng)的需求與實(shí)現(xiàn)的目標(biāo)，理解系統(tǒng)的運(yùn)轉(zhuǎn)過程
  可以通過系統(tǒng)的流程圖甸箱，劃分出系統(tǒng)的各功能模塊
• 確定FSM的設(shè)計(jì)策略
• 整理出系統(tǒng)的全部輸入和輸出
• 構(gòu)造狀態(tài)空間
  從系統(tǒng)中抽象出全部的系統(tǒng)狀態(tài)育叁，進(jìn)行狀態(tài)分割，構(gòu)造FSM的狀態(tài)空間
• 明確系統(tǒng)各狀態(tài)之間的遷移關(guān)系
• 明確各狀態(tài)遷移關(guān)系所對(duì)應(yīng)的輸入事件與輸出事件
• 確定FSM
  畫出系統(tǒng)狀態(tài)遷移圖或狀態(tài)遷移表芍殖，明確系統(tǒng)FSM的所有要素
• 狀態(tài)空間簡(jiǎn)化
  FSM狀態(tài)空間的簡(jiǎn)化豪嗽，盡可能使?fàn)顟B(tài)重復(fù)利用，消除冗余的狀態(tài)豌骏，簡(jiǎn)化設(shè)計(jì)龟梦，降低系統(tǒng)復(fù)雜度，提高可靠性
• 系統(tǒng)編碼
  對(duì)輸入窃躲、輸出计贰、各狀態(tài)及各狀態(tài)轉(zhuǎn)移關(guān)系根據(jù)設(shè)計(jì)策略進(jìn)行編碼
  其它的設(shè)計(jì)階段

5. FSM的優(yōu)點(diǎn)

• 簡(jiǎn)單性
• 可預(yù)測(cè)性
• 易于實(shí)現(xiàn)
• 易于測(cè)試

6. 停等協(xié)議

停等協(xié)議甲乙雙方

將甲乙兩方各自的有限狀態(tài)機(jī)合在一起，用一個(gè)有限狀態(tài)機(jī)來描述整個(gè)系統(tǒng)蒂窒。這回導(dǎo)致狀態(tài)數(shù)目大大增加躁倒，因此需要合并一些狀態(tài)，考慮一些次要的細(xì)節(jié)洒琢。

合并后的狀態(tài)變遷圖

7. FSM的簡(jiǎn)化

• 狀態(tài)層次化
• 使用原子過程
• 使用協(xié)議變量
  可大大減少狀態(tài)機(jī)的狀態(tài)數(shù)秧秉。
• 隱藏內(nèi)部協(xié)同事件
• 簡(jiǎn)化通道FSM
  如果n層協(xié)議采用同步通信方式，那么不管(n-1)層通道是否是緩沖通道纬凤，都可以處理成非緩沖通道福贞；
  如果報(bào)文傳送時(shí)間和延遲時(shí)間對(duì)協(xié)議機(jī)制無影響，或者只影響協(xié)議變量的值停士，那么非緩沖通道可處理成空通道挖帘。

8. FSM的錯(cuò)誤模型

可達(dá)性分析：
死鎖
活鎖
無限分支
不可達(dá)狀態(tài)

其他：
輸出錯(cuò)
轉(zhuǎn)移錯(cuò)
輸出轉(zhuǎn)移錯(cuò)

9. EFSM

FSM的缺點(diǎn)：

• 處理復(fù)雜問題時(shí)可能發(fā)生狀態(tài)空間爆炸
• FSM可以很好地描述狀態(tài)間地遷移特性，但無法很好地描述輸入輸出間地變換特性
• FSM只反映協(xié)議事件和協(xié)議狀態(tài)之間地關(guān)系恋技，不能表達(dá)其他協(xié)議元素

FSM擴(kuò)展模型地目的：

• 增強(qiáng)FSM描述能力
• 簡(jiǎn)化描述
• 使各狀態(tài)之間地變遷清晰化
• 最終提高對(duì)局部以至整個(gè)模型地描述與分析能力
• 可被用作為以后開發(fā)者描述解決方案地工具

其中拇舀，明顯的缺點(diǎn)為：
FSM不能方便地描述對(duì)變量地操作
缺少描述任意數(shù)值的傳送能力

從兩個(gè)方面對(duì)FSM進(jìn)行擴(kuò)展：

• 變量
  如果變量的取值范圍是有限的，則變量的加入并沒有增加FSM的計(jì)算能力蜻底。 可以用有限狀態(tài)機(jī)來描述一個(gè)取值范圍有限的變量骄崩。
  優(yōu)點(diǎn)：
  變量地引入豐富了FSM地狀態(tài)變遷函數(shù)地表達(dá)能力，還可以減少FSM的狀態(tài)空間

• 引入一組操縱變量地算術(shù)和邏輯操作符

三、PetriNet

Petri網(wǎng)是一種圖形化的數(shù)學(xué)工具要拂，適合于描述和分析并發(fā)抠璃、異步、分布式的系統(tǒng)脱惰，特別便于描述系統(tǒng)中進(jìn)程或組件的順序搏嗡、并發(fā)、沖突以及同步等關(guān)系拉一。
Petri網(wǎng)也是一種狀態(tài)變遷模型采盒，它允許同時(shí)發(fā)生多個(gè)狀態(tài)變遷，因而Petri網(wǎng)是一種并發(fā)模型蔚润“醢保可用來描述通信系統(tǒng)中各異步組件之間的關(guān)系。

Petri網(wǎng)所處的狀態(tài)是由標(biāo)記的分布來決定的嫡纠。

1. Petri網(wǎng)形式化定義

Petri網(wǎng)的四元組

2. Petri網(wǎng)的狀態(tài)變遷

發(fā)生變遷的條件：

• 必須有1個(gè)或多個(gè)變遷滿足變遷條件
  變遷條件：
  某個(gè)變遷tj的所有輸入位置中都必須有標(biāo)記存在烦租，并且當(dāng)輸入位置有多條弧線指向這個(gè)變遷時(shí)，該輸入位置也至少具有和弧線數(shù)相等的標(biāo)記數(shù)货徙；
  所有輸入位置中的標(biāo)記數(shù)都必須大于或者等于該輸入位置指向tj的弧線數(shù)左权。

• 必須發(fā)生點(diǎn)火
  所謂點(diǎn)火就是發(fā)生了一些事件(1個(gè)或多個(gè))，而這些事件所對(duì)應(yīng)的變遷滿足變遷條件痴颊。

標(biāo)記移動(dòng)規(guī)則：

發(fā)生點(diǎn)火后赏迟，標(biāo)記要重新分布。

• 從點(diǎn)火的變遷tj的所有輸入位置中均取出標(biāo)記蠢棱，每個(gè)位置取出的標(biāo)記數(shù)等于該位置指向點(diǎn)火的變遷tj 的弧線數(shù)锌杀；
• 然后再將標(biāo)記送入tj 的所有輸出位置中去，送入每個(gè)位置的標(biāo)記數(shù)等于點(diǎn)火的tj 指向該位置的弧線數(shù)泻仙。

一個(gè)簡(jiǎn)單的例子：

圖1

圖2

圖3

狀態(tài)變遷類型：

• 順序變遷
  只有t1點(diǎn)火后t2才能點(diǎn)火
• 并發(fā)變遷
  t1和t2可同時(shí)點(diǎn)火
• 互斥變遷
  t1和t2只能有一個(gè)點(diǎn)火糕再。一個(gè)點(diǎn)火后另一個(gè)就不能再點(diǎn)火了。

3. PetriNet的擴(kuò)充

• 基于標(biāo)記和位置的擴(kuò)充
  一個(gè)位置中的不同標(biāo)記用不同的名字或標(biāo)識(shí)號(hào)來表示——有色Petri網(wǎng)
• 基于輸入函數(shù)和輸出函數(shù)的擴(kuò)充
  允許每個(gè)位置減少或增加多個(gè)標(biāo)記玉转，并再弧線上標(biāo)上增加或減少的標(biāo)記數(shù)
• 基于變遷的擴(kuò)充
  在變遷上標(biāo)明謂詞和動(dòng)作——謂詞-動(dòng)作Petri網(wǎng)

4. PetriNet的性質(zhì)

• 行為性質(zhì) - 與初始標(biāo)記量有關(guān)的性質(zhì)
• 結(jié)構(gòu)性質(zhì) - 與初始標(biāo)記量無關(guān)的性質(zhì)

行為性質(zhì)：

• 可達(dá)性
• 有界性
• 活性
• 可逆性
• 可覆蓋性
• 可持續(xù)性

1）可達(dá)性

• 可達(dá)的
  如果存在一系列變遷t1, t2, …, tn的發(fā)生使得Petri網(wǎng)的標(biāo)記向量轉(zhuǎn)換為Mn突想，則稱標(biāo)記向量Mn是從M0可達(dá)的 。
• 變遷的引發(fā)序列
  將M0 t1, M1 t2, M2 t3, …, tnMn稱為變遷的引發(fā)序列究抓，記為σ猾担，或簡(jiǎn)記為σ=t1, t2, …, tn。
• 可達(dá)標(biāo)記向量集
  所有可達(dá)的標(biāo)記向量形成一個(gè)可達(dá)標(biāo)記向量集刺下，一般記為R(M0)绑嘹。
• 引發(fā)序列集
  從M0出發(fā)的所有可能引發(fā)序列形成一個(gè)引發(fā)序列集，一般記為L(zhǎng)(M0)橘茉。

2)有界性

• 有界性
  在一個(gè)Petri網(wǎng)中工腋，如果存在一個(gè)非負(fù)整數(shù)k姨丈，使得從M0開始的任一可達(dá)標(biāo)記向量中的位置p上的標(biāo)記數(shù)都不超過k，則稱位置p為k有界擅腰。
  如果Petri網(wǎng)中每一位置都是k有界的蟋恬，則稱該P(yáng)etri網(wǎng)為k有界。
  有界性意味著位置中的標(biāo)記數(shù)量不會(huì)無限地增加惕鼓。
• 安全性
  如果位置p為1有界筋现，則稱位置p是安全的。如果Petri網(wǎng)中每一位置都是１有界的箱歧，則稱該P(yáng)etri網(wǎng)是安全的。

3）活性

活性：反映的是系統(tǒng)中無死鎖的特性一膨。

• 潛在可引發(fā)的
  在一個(gè)Petri網(wǎng)中呀邢，初始標(biāo)記向量為M0，如果存在一個(gè)標(biāo)記向量M∈R(M0)(可達(dá)標(biāo)記向量集)豹绪，使得變遷t使能(滿足變遷條件)价淌，則稱t是潛在可引發(fā)的。
• 變遷在M0下是活的
  如果對(duì)任何M∈R(M0)瞒津，變遷t都是潛在可引發(fā)的蝉衣，則稱t在標(biāo)記向量M0下是活的。即從M0可達(dá)的任一標(biāo)記向量出發(fā)巷蚪，都可以通過執(zhí)行某一變遷序列而最終引發(fā)變遷t病毡。
• Petri網(wǎng)是活的
  如果所有變遷t都是活的，則稱該P(yáng)etri網(wǎng)是活的屁柏，或者稱M0是網(wǎng)的活標(biāo)識(shí)啦膜。

變遷t的活性等級(jí)劃分：
L0 - 沒有任何一個(gè)變遷序列可以引發(fā)變遷t，即該變遷是“死的”
L1 - 在某些變遷序列中淌喻，變遷t至少被引發(fā)一次
L2 - 在某些變遷序列中僧家，變遷t至少被引發(fā)k次
L3 - 在某些變遷序列中，變遷t可無限次被引發(fā)
L4 - 在每個(gè)變遷序列中裸删，變遷t至少被引發(fā)一次

4）可逆性

在一個(gè)Petri網(wǎng)中八拱，如果存在一個(gè)引發(fā)序列σ=t1, t2, …, tn，使得從該P(yáng)etri網(wǎng)的任一可達(dá)標(biāo)記向量M出發(fā)可以返回到初始標(biāo)記向量M0涯塔，則稱該P(yáng)etri網(wǎng)是可逆的肌稻。

5）可覆蓋性

在一個(gè)Petri網(wǎng)中，對(duì)于標(biāo)記向量M伤塌，如果存在一標(biāo)記向量M′灯萍，任一位置p，都有：位置p在M′中的分量的值都大于等于該位置在M中的分量的值每聪，則稱標(biāo)記向量M是可覆蓋的旦棉。

6）可持續(xù)性

在一個(gè)Petri網(wǎng)中齿风，如果對(duì)于任何兩個(gè)滿足變遷條件的變遷，其中一個(gè)變遷被引發(fā)以后绑洛，另一個(gè)變遷仍然滿足變遷條件救斑，則稱該P(yáng)etri網(wǎng)是可持續(xù)的。

7）公平性

在一個(gè)Petri 網(wǎng)中真屯，對(duì)于兩個(gè)變遷t1, t2脸候，如果其中一個(gè)變遷可以引發(fā) 而另一個(gè)變遷不可引發(fā)的這種情況出現(xiàn)的最大次數(shù)是有界的，稱這兩個(gè)變遷具有有界公平關(guān)系绑蔫。
如果該P(yáng)etri網(wǎng)中运沦，任意一對(duì)變遷都存在有界公平關(guān)系，則稱該P(yáng)etri網(wǎng)為有界公平網(wǎng)配深。

結(jié)構(gòu)性質(zhì)：

• 結(jié)構(gòu)活性
  存在活的初始標(biāo)記向量M0
• 結(jié)構(gòu)有界性
  Petri對(duì)任何初始標(biāo)記向量都有界
• 可重復(fù)性
  存在一個(gè)初始標(biāo)記向量和一個(gè)引發(fā)序列携添，使得所有變遷被引發(fā)無限次，則稱該P(yáng)etri網(wǎng)為可重復(fù)篓叶；
  如果使得部分變遷被引發(fā)無限次烈掠，則稱該P(yáng)etri網(wǎng)為部分可重復(fù)。
• 相容性
  如果存在一個(gè)初始標(biāo)記向量M0和一個(gè)引發(fā)序列σ∈L(M0)缸托，使得所有變遷至少被引發(fā)一次左敌，則稱該P(yáng)etri網(wǎng)為相容的；
  如果使得部分變遷至少被引發(fā)一次俐镐，則稱該P(yáng)etri網(wǎng)為部分相容的矫限。
• 結(jié)構(gòu)有界公平性
  對(duì)于任何初始標(biāo)記向量，如果兩個(gè)變遷之間總存在有界公平關(guān)系京革，則稱這兩個(gè)變遷具有結(jié)構(gòu)有界公平關(guān)系奇唤；
  如果一個(gè)Petri網(wǎng)對(duì)于任何初始標(biāo)記向量都是有界公平的，則稱該P(yáng)etri網(wǎng)為結(jié)構(gòu)有界公平的 匹摇。

5. Petri網(wǎng)在協(xié)議描述中的應(yīng)用

• 停等協(xié)議

不編號(hào)的停等協(xié)議

編號(hào)的停等協(xié)議

• 讀寫

  
  
  讀寫進(jìn)程

第四章 協(xié)議形式描述語言（SDL）

SDL是基于擴(kuò)展有限狀態(tài)機(jī)和抽象數(shù)據(jù)類型的混合技術(shù)咬扇。SDL既可描述系統(tǒng)的概要設(shè)計(jì)，亦可描述系統(tǒng)的詳細(xì)設(shè)計(jì)廊勃。

一懈贺、SDL的三種語法形式

1. 圖形表示的SDL/PR

較適合于描述系統(tǒng)的結(jié)構(gòu)和控制流

2. 用文字短語表示的SDL/PR

較適合于機(jī)器處理

3. 程序語言形式的SDL，X.250

二坡垫、SDL系統(tǒng)結(jié)構(gòu)

1. 概述

在SDL中梭灿，整個(gè)系統(tǒng)由多個(gè)互連的抽象機(jī)（擴(kuò)展的有限狀態(tài)機(jī)FSM）所組成。
每個(gè)抽象機(jī)的動(dòng)態(tài)行為由其他抽象機(jī)或環(huán)境的交互和對(duì)交互數(shù)據(jù)的操作來描述冰悠。

SDL/PR使用的主要符號(hào)：

SDL/PR使用的主要符號(hào)

2. SDL的靜態(tài)結(jié)構(gòu)

一個(gè)SDL應(yīng)用的靜態(tài)結(jié)構(gòu)由系統(tǒng)堡妒、功能塊、進(jìn)程溉卓、過程和通道構(gòu)成皮迟。

SDL的靜態(tài)結(jié)構(gòu)

1）系統(tǒng)

規(guī)范所描述的對(duì)象稱為一個(gè)系統(tǒng)搬泥。
根據(jù)系統(tǒng)與環(huán)境之間是否有交互，將系統(tǒng)分為開放的和封閉的伏尼。

一個(gè)系統(tǒng)的規(guī)范描述由以下部分組成：
所有通道忿檩、信號(hào)(Signal)、信號(hào)表(Signal List)爆阶、預(yù)定義的數(shù)據(jù)類型與/或宏(macro)的定義燥透；一個(gè)或多個(gè)功能塊。

2）功能塊

功能塊含有進(jìn)程辨图，并用來構(gòu)造系統(tǒng)班套。功能塊通過通道互連，并通過通道連接到系統(tǒng)邊界故河。
在描述功能塊時(shí)孽尽，進(jìn)程、過程(Procedure)忧勿、服務(wù)類型、數(shù)據(jù)類型和信號(hào)均可作為功能塊描述規(guī)范的一部分瞻讽。

3）進(jìn)程

可保留和處理數(shù)據(jù)鸳吸，數(shù)據(jù)受進(jìn)程的局部變量(由該進(jìn)程定義)約束。
利用信號(hào)速勇，數(shù)據(jù)值可在進(jìn)程之間傳送晌砾，也可傳送給環(huán)境或從環(huán)境接收。

4）通道

通道充當(dāng)功能塊之間以及功能塊與系統(tǒng)邊界之間傳輸信號(hào)的媒介烦磁。既可以是單方向的养匈，也可以是雙方向的。

在SDL中都伪，將系統(tǒng)呕乎、功能塊、進(jìn)程等稱為代理陨晶。各個(gè)代理用塊圖來表示猬仁，一個(gè)代理可以對(duì)應(yīng)多個(gè)塊圖。

三先誉、SDL對(duì)系統(tǒng)動(dòng)態(tài)行為的描述

1. SDL的結(jié)構(gòu)化概念

系統(tǒng)中的每一個(gè)功能塊由一組進(jìn)程或一組子功能塊組成湿刽，進(jìn)程間通過信號(hào)路由(Signal routes)或功能塊的子結(jié)構(gòu)(Substructure)相連接。
子功能塊又可由一組進(jìn)程或一組子功能塊組成褐耳。這樣可得到一個(gè)系統(tǒng)的分級(jí)多層描述：功能塊樹 (Tree of Blocks)

2. 動(dòng)態(tài)行為描述

• 各功能塊包含若干個(gè)進(jìn)程诈闺，SDL系統(tǒng)的動(dòng)態(tài)行為具體表現(xiàn)為各進(jìn)程的實(shí)例的并發(fā)操作 (Instance，即進(jìn)程的一次活動(dòng)铃芦，用PId來表示) 雅镊。

• 進(jìn)程的狀態(tài)與動(dòng)作是用擴(kuò)展的FSM來建模的襟雷。
  1.進(jìn)程狀態(tài)的變化受外來信號(hào)激勵(lì)，同時(shí)漓穿，進(jìn)程也可向環(huán)境返回響應(yīng)信號(hào)嗤军。
  2.一個(gè)進(jìn)程可同時(shí)收到多個(gè)信號(hào)。
  SDL設(shè)置了隊(duì)列以暫時(shí)存放這些信號(hào)(一般采用先進(jìn)先出的方式)晃危。
  3.進(jìn)程也可自行處理保留信號(hào)叙赚。
  保留信號(hào)是指在某些狀態(tài)下需等待其他信號(hào)到達(dá)并處理之后才能處理的信號(hào)。

四僚饭、SDL中的數(shù)據(jù)

在SDL中震叮，數(shù)據(jù)的定義一般基于抽象數(shù)據(jù)類型。
“抽象數(shù)據(jù)類型”是指其定義并不描述(數(shù)據(jù))類型是如何實(shí)現(xiàn)的鳍鸵，而僅僅描述當(dāng)將操作符(Operators)應(yīng)用到該類型的數(shù)值上時(shí)產(chǎn)生何種結(jié)果苇瓣。

1. SDL預(yù)定義數(shù)據(jù)類型

SDL定義了一些預(yù)定義的數(shù)據(jù)類型，
如布爾(Boolean)偿乖、整數(shù)(Integer)击罪、自然數(shù)(Natural)、實(shí)數(shù)(Real)贪薪、字符(Character)媳禁、字符串(Charstring)、進(jìn)程標(biāo)識(shí)符(PId)画切、時(shí)刻(Time)竣稽、持續(xù)時(shí)間(Duration)。
此外霍弹，SDL還預(yù)定義了一些產(chǎn)生器(Generator)毫别，
如數(shù)組(Array)、串(String)典格、計(jì)時(shí)器(Timer)和冪集(Powerset)等岛宦。
這些預(yù)定義的數(shù)據(jù)類型可在任何級(jí)別上的SDL描述中使用。
用戶還可用上述數(shù)據(jù)類型自行定義其他的數(shù)據(jù)類型钝计。

2. 類

在SDL中恋博，類(Sort) 是值的集合。集合中的元素個(gè)數(shù)可以是有限的私恬，也可以是無限的债沮，但不能為空。
一般來說本鸣，SDL中的數(shù)據(jù)類型定義包括三個(gè)部分：類定義疫衩，操作符(Operators)定義和等價(jià)式(Equations)定義。

1）類定義

例：Boolean類定義

Boolean類定義

• 詞
  值與操作符的組合構(gòu)成詞

• 等價(jià)式
  給出規(guī)則荣德，說明給定類中的哪些詞表示同一個(gè)值

• 等值類
  由值相等的詞所構(gòu)成的集合闷煤，稱為等值類童芹。將詞的集合分為多個(gè)子集。

第五章 協(xié)議驗(yàn)證技術(shù)

一鲤拿、驗(yàn)證的含義

正確性
完整性
一致性

驗(yàn)證協(xié)議的實(shí)現(xiàn) 一致性測(cè)試

Verification 在功能方面驗(yàn)證
Validation 語法方面驗(yàn)證

二假褪、驗(yàn)證的方法

1. 非形式化驗(yàn)證

主要通過遍歷和代碼檢查

2. 形式化驗(yàn)證

以形式描述技術(shù)為前提，主要將形式描述技術(shù)與推理技術(shù)結(jié)合近顷。
一方面可以獲得無二義性的協(xié)議規(guī)范生音，另一方面可以借助計(jì)算機(jī)輔助工具來幫助實(shí)施自動(dòng)或半自動(dòng)驗(yàn)證。

• 模型檢測(cè)
  基于狀態(tài)搜索

• 演繹驗(yàn)證
  基于定理證明

1）模型檢測(cè)/模型檢查/模型檢驗(yàn)

本質(zhì)上是用嚴(yán)密的數(shù)學(xué)方法來驗(yàn)證設(shè)計(jì)是否滿足預(yù)設(shè)的需求窒升，從而自動(dòng)化地發(fā)現(xiàn)設(shè)計(jì)中的錯(cuò)誤缀遍。是一種檢查給定模型是否滿足某一邏輯規(guī)則的方法。

• 基本思想
  (1)用狀態(tài)遷移系統(tǒng)(S)表示系統(tǒng)的行為饱须，用模態(tài)/時(shí)序邏輯公式(F)描述系統(tǒng)的性質(zhì)域醇。
  (2)“系統(tǒng)是否具有某種期望的性質(zhì)”就轉(zhuǎn)化數(shù)學(xué)問題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個(gè)模型？”
  公式表示：S |= F?

• 過程描述
  1.建立模型
  2.描述系統(tǒng)性質(zhì)
  3.驗(yàn)證

• 模型檢測(cè)方法
  最常見方法：可達(dá)性分析蓉媳、不變性分析
  特性：
  能給出反例
  自動(dòng)化程度高
  問題：
  狀態(tài)空間爆炸

2）演繹驗(yàn)證方法

定理證明方法：

• 步驟
  1.將實(shí)現(xiàn)方案和功能描述都轉(zhuǎn)換為一種形式邏輯譬挚，如命題邏輯、一階邏輯(First Order Logic, FOL)酪呻、高階邏輯(Higher Order Logic, HOL)等
  2.建立公理系統(tǒng)殴瘦，作為驗(yàn)證的依據(jù)，并將協(xié)議性質(zhì)構(gòu)造成一組代數(shù)定理
  3.根據(jù)公理系統(tǒng)号杠，使用定理證明器，通過邏輯推理丰歌、邏輯歸約等手段姨蟋，構(gòu)造證明過程，證明實(shí)現(xiàn)方案和功能描述等價(jià)

• 問題
  入門難立帖，前兩步難

三眼溶、協(xié)議性質(zhì)

協(xié)議驗(yàn)證的最主要任務(wù)是檢查協(xié)議是否滿足規(guī)定的協(xié)議性質(zhì)。

• 一般性質(zhì)
• 特殊性質(zhì)

也有文獻(xiàn)將其分為安全性和活動(dòng)性晓勇。
活動(dòng)性體現(xiàn)在終止性和進(jìn)展性兩個(gè)方面堂飞。

1. 一般性質(zhì)

• 可達(dá)性
• 沒有死鎖
• 沒有活鎖
• 弱活鎖
• 時(shí)間相關(guān)的活鎖（臨時(shí)阻塞）
• 無狀態(tài)二義性
• 有界性
• 可恢復(fù)性或自同步性
• 互斥性
• 公平性
• 終止或進(jìn)展

1）可達(dá)性

協(xié)議的各種可能狀態(tài)之間的可達(dá)關(guān)系。

2. 特殊性質(zhì)

• 完整性
• 一致性

3. 一般性質(zhì)和特殊性質(zhì)

協(xié)議驗(yàn)證著重于一般性質(zhì)
協(xié)議測(cè)試著重于特殊性質(zhì)

四绑咱、可達(dá)性分析

檢查協(xié)議描述中是否有不可達(dá)绰筛，死鎖、未定義描融、活鎖等協(xié)議模型錯(cuò)誤铝噩；包括狀態(tài)窮舉风秤，狀態(tài)隨機(jī)枚舉失息，狀態(tài)概率枚舉等方法搓萧。

可達(dá)性分析是最常用的協(xié)議驗(yàn)證方法,它試圖產(chǎn)生和檢查協(xié)議所有或部分可達(dá)狀態(tài)袒啼。

• 全局狀態(tài)(Global state): 協(xié)作的協(xié)議實(shí)體以及連接這些協(xié)議實(shí)體的通道的整體狀態(tài)。
• 可達(dá)狀態(tài): 指協(xié)議從初始狀態(tài)開始經(jīng)歷有限次變遷之后可到達(dá)的狀態(tài)具被。
  所有可達(dá)狀態(tài)構(gòu)成可達(dá)圖

可達(dá)性分析的三個(gè)重要技術(shù)：
怎樣找出所有可達(dá)狀態(tài)玻募，構(gòu)成可達(dá)圖。
怎樣檢測(cè)死鎖一姿、活鎖等協(xié)議錯(cuò)誤七咧。
怎樣解決狀態(tài)空間爆炸問題。

可達(dá)性分析練習(xí)

1. 可達(dá)性分析原理：

采用窮舉法檢查同一層內(nèi)兩個(gè)或多個(gè)協(xié)議實(shí)體間所有可能的交互所產(chǎn)生的全局狀態(tài)啸蜜。
從一個(gè)給定的初始狀態(tài)開始坑雅，觸發(fā)所有可能的變遷(用戶命令、超時(shí)衬横、消息發(fā)送裹粤、接收等)，產(chǎn)生新的全局狀態(tài)蜂林。
對(duì)每一個(gè)新產(chǎn)生的狀態(tài)重復(fù)執(zhí)行上述過程直到?jīng)]有新的狀態(tài)產(chǎn)生(某些變遷將導(dǎo)致系統(tǒng)返回到已產(chǎn)生的狀態(tài))遥诉。
對(duì)于一個(gè)給定的初始狀態(tài)，這種分析能夠確定協(xié)議可能產(chǎn)生的所有結(jié)果噪叙。

2. 可達(dá)性分析算法

• 窮盡性可達(dá)性分析算法
• 受控部分搜索算法
  1.限制深度法
  2.散開搜索法
  3.定向搜索法
  4.概率搜索法
  5.隨機(jī)選擇法
• 隨機(jī)模擬算法

1）窮盡性可達(dá)性分析算法

窮盡性可達(dá)性分析算法

• 深度優(yōu)先與廣度優(yōu)先
  當(dāng)發(fā)現(xiàn)一個(gè)錯(cuò)誤時(shí)矮锈，在廣度優(yōu)先算法中，必須依據(jù)從狀態(tài)集合A 中得到的信息來重構(gòu)從初始系統(tǒng)狀態(tài)開始的路徑睁蕾。(先進(jìn)先出苞笨， W中無法按執(zhí)行序列保存之前的狀態(tài))；
  在深度優(yōu)先算法中子眶，一個(gè)重要的優(yōu)點(diǎn)是瀑凝，當(dāng)發(fā)現(xiàn)錯(cuò)誤時(shí)，算法能從初始狀態(tài)開始通過一系列有效的狀態(tài)轉(zhuǎn)換到達(dá)錯(cuò)誤點(diǎn)臭杰。無需重構(gòu)從初始系統(tǒng)狀態(tài)開始的路徑粤咪，因?yàn)檫@個(gè)序列已被集合W中的堆棧排序中隱含定義了。(先進(jìn)后出渴杆， W中按執(zhí)行序列保存了之前的狀態(tài))寥枝。

先廣搜索的優(yōu)點(diǎn)：優(yōu)先發(fā)現(xiàn)執(zhí)行序列短的錯(cuò)誤狀態(tài)；
先深搜索方法的優(yōu)點(diǎn)之一是占用存貯空間小磁奖。
假定每個(gè)狀態(tài)有兩個(gè)后繼狀態(tài)囊拜，算法執(zhí)行m步之后，對(duì)于先深搜索方法比搭，W的長(zhǎng)度為m艾疟；而對(duì)于先廣搜索方法，W的長(zhǎng)度為2m。

2）受控部分搜索算法

一般來說蔽莱，受控部分搜索算法較全局搜索方法有效和可行弟疆。但是，這種方法不能保證協(xié)議無錯(cuò)盗冷。通常需要執(zhí)行多次才能得到比較可信的結(jié)果怠苔。

3）隨機(jī)模擬算法

隨機(jī)模擬/隨機(jī)遍歷

隨機(jī)模擬算法

隨機(jī)模擬算法與協(xié)議系統(tǒng)的大小和復(fù)雜性無關(guān)，即使是無限大的系統(tǒng)仪糖，也可以應(yīng)用柑司。因此，對(duì)于復(fù)雜的驗(yàn)證問題锅劝，這種算法也許是唯一可用的方法攒驰。

4）三種算法的比較

• 窮盡性可達(dá)性分析算法的優(yōu)點(diǎn)在于可以證明協(xié)議中沒有錯(cuò)誤，但問題在于其應(yīng)用范圍有限故爵。（系統(tǒng)狀態(tài)數(shù)目非常大時(shí)可能發(fā)生狀態(tài)空間爆炸/對(duì)于復(fù)雜的協(xié)議搜索質(zhì)量會(huì)下降）
• 受控部分搜索算法的目的是證明錯(cuò)誤地存在而不是證明沒有錯(cuò)誤玻粪。它在一定程度上能夠解決空間爆炸問題劲室。其缺點(diǎn)是：協(xié)議中的錯(cuò)誤的可能位置難以預(yù)測(cè)；無法保證其狀態(tài)空間大小與可用內(nèi)存相匹配结窘；有效搜索的部分狀態(tài)空間大小是協(xié)議相關(guān)的很洋，只能通過實(shí)驗(yàn)確定；為了尋找最優(yōu)方法隧枫，需要按不同的選擇策略多次驗(yàn)證喉磁。
• 隨機(jī)模擬算法與協(xié)議系統(tǒng)的大小和復(fù)雜性無關(guān)，即使是無限大的系統(tǒng)官脓，也可以應(yīng)用线定。因此，對(duì)于復(fù)雜的驗(yàn)證問題确买，這種算法也許是唯一可用的方法。其缺點(diǎn)是沒有明確的終止纱皆，無法判斷是否已訪問系統(tǒng)的所有可達(dá)狀態(tài)湾趾，因此，只能發(fā)現(xiàn)協(xié)議中的錯(cuò)誤派草，而不能證明協(xié)議中沒有錯(cuò)誤搀缠。

3. 基于可達(dá)性分析的協(xié)議錯(cuò)誤檢測(cè)

• 死鎖
• 非定義的輸入事件
• 無意義事件
• 活鎖

4. 狀態(tài)空間爆炸問題的解決

• 部分搜索算法
• 部分規(guī)范描述和驗(yàn)證
• 選擇大的動(dòng)作單元
• 分解或劃分
• 按斷言來分類狀態(tài)

五、不變性分析

如果一個(gè)系統(tǒng)的某個(gè)性質(zhì)能用一個(gè)確定的邏輯表達(dá)式描述艺普，并且恒為真(不隨系統(tǒng)的狀態(tài)變化或執(zhí)行序列而改變)岸浑，那么這個(gè)性質(zhì)稱為系統(tǒng)的不變性質(zhì)，簡(jiǎn)稱為系統(tǒng)不變性(system invariance)。

• 協(xié)議不變性分析的兩個(gè)工作：
  1.完全正確地找出系統(tǒng)的不變性質(zhì)
  2.驗(yàn)證不變性表達(dá)式是否恒為真

1. 不變性分析的途徑

• 不變性證明系統(tǒng)（通常采用歸納法）
• 不變性監(jiān)測(cè)系統(tǒng)

1）不變性證明系統(tǒng)

采用歸納法：
驗(yàn)證初始狀態(tài)的不變性表達(dá)式是否成立；
假定某個(gè)狀態(tài)的不變性成立揩徊，驗(yàn)證從該狀態(tài)開始的所有相關(guān)事件過程中不變性是否成立猾普。

2）不變性監(jiān)測(cè)系統(tǒng)

借助監(jiān)測(cè)軟件和監(jiān)測(cè)方法對(duì)模擬運(yùn)行或符號(hào)執(zhí)行中的協(xié)議進(jìn)行不變性校驗(yàn)的過程稱之為不變性監(jiān)測(cè)。

第七章 一致性測(cè)試技術(shù)

驗(yàn)證一項(xiàng)新的協(xié)議實(shí)現(xiàn)陌知，通常需要進(jìn)行多項(xiàng)測(cè)試志笼。一般要考慮以下四個(gè)方面：

• 一致性測(cè)試(conformance testing)
  一致性測(cè)試旨在檢測(cè)所實(shí)現(xiàn)的協(xié)議實(shí)體(或系統(tǒng))與協(xié)議規(guī)范的符合程度(而驗(yàn)證則是檢查形式化規(guī)范的邏輯正確性)

• 互操作測(cè)試(interoperateability testing)
  檢測(cè)同意協(xié)議的不同實(shí)現(xiàn)版本的互通能力和互操作能力

• 性能測(cè)試(performance testing)
  非功能測(cè)試，主要檢測(cè)協(xié)議實(shí)體或系統(tǒng)的性能參數(shù)疗锐。

• 魯棒性測(cè)試(robustness testing)
  檢測(cè)協(xié)議實(shí)體或系統(tǒng)在各種惡劣環(huán)境下運(yùn)行的能力。

一、 一致性測(cè)試與驗(yàn)證

“一致性測(cè)試”的目的是檢查一個(gè)給定協(xié)議實(shí)現(xiàn)的外部行為是否符合協(xié)議的規(guī)范。
“驗(yàn)證”檢查形式化規(guī)范的邏輯正確性祭玉。

二律姨、 功能測(cè)試與結(jié)構(gòu)測(cè)試

• 功能測(cè)試
  協(xié)議實(shí)現(xiàn)是否實(shí)現(xiàn)了協(xié)議規(guī)范的所有功能；協(xié)議實(shí)現(xiàn)是否可以正確地以與協(xié)議規(guī)范一致的方式拒絕錯(cuò)誤輸入凤价。
  問題：復(fù)雜性；難以標(biāo)準(zhǔn)化。

• 結(jié)構(gòu)測(cè)試
  協(xié)議實(shí)現(xiàn)的控制結(jié)構(gòu)與規(guī)范的結(jié)構(gòu)是否一致。如果二者的狀態(tài)集等價(jià)并且狀態(tài)轉(zhuǎn)換相同疆导，則二者具有相同的結(jié)構(gòu)舰攒。
  問題：無法完全檢查芬骄，常需要增加一些限制條件。

三、 一致性測(cè)試的前提

假定協(xié)議標(biāo)準(zhǔn)本身是正確的。

通過一致性測(cè)試可以給用戶提供兩個(gè)信息：
通過了一致性測(cè)試的協(xié)議實(shí)現(xiàn)，具有協(xié)議所要求的各種能力。
在具有代表性的通信實(shí)例中蕴轨，被測(cè)試的協(xié)議實(shí)現(xiàn)的外部特性與協(xié)議標(biāo)準(zhǔn)的要求一致燥狰。

四、一致性測(cè)試要求

• 靜態(tài)一致性要求
• 動(dòng)態(tài)一致性要求

DCR和SCR
動(dòng)態(tài)一致性是指協(xié)議規(guī)范中規(guī)定的通信實(shí)例中的協(xié)議實(shí)現(xiàn)所必須呈現(xiàn)的外部特性的組合或允許的各種選擇性組合嗤练；
而靜態(tài)一致性是指協(xié)議規(guī)范中為了使協(xié)議實(shí)現(xiàn)能夠互連而定義的功能類別革答、功能單元的分組以及選擇性功能等旗扑。

五蹦骑、一致性測(cè)試級(jí)別

ISO 9646將協(xié)議一致性測(cè)試分為四級(jí)，由低到高分別為

• 基本互連測(cè)試
• 能力測(cè)試
• 行為測(cè)試
• 一致性分解測(cè)試

行為測(cè)試可分兩級(jí)：
覆蓋性測(cè)試：只要求測(cè)試序列歷經(jīng)IUT的所有變遷至少一次即可臀防。
窮盡性測(cè)試：要求檢查每個(gè)變遷的前后狀態(tài)眠菇。

六、一致性測(cè)試模型

七致燥、一致性測(cè)試流程

八续捂、一致性測(cè)試方法

一致性測(cè)試方法決定了 測(cè)試集的產(chǎn)生和描述方法、測(cè)試執(zhí)行系統(tǒng)的結(jié)構(gòu) 等洗做。
ISO 9646中定義了四種標(biāo)準(zhǔn)的抽象測(cè)試方法：

• 本地測(cè)試法(Local Mehtod)
• 分布式測(cè)試法(Distributed Method)
• 協(xié)調(diào)測(cè)試法(Coordination Mehtod)
• 遠(yuǎn)程測(cè)試法(Remote Method)杯缺。

本地測(cè)試法：

本地測(cè)試法

分布式測(cè)試法：

分布式測(cè)試法

協(xié)同測(cè)試法：

協(xié)同測(cè)試法

遠(yuǎn)程測(cè)試法：

遠(yuǎn)程測(cè)試法

上述這幾種測(cè)試法是最基本的，適于單層協(xié)議測(cè)試，有許多變種，如渡船測(cè)試法(Ferry Method)镰惦、多方測(cè)試法及騎跨式(Astride)測(cè)試法等聘殖。

九陨舱、測(cè)試集

測(cè)試集包括兩部分：
測(cè)試序列
測(cè)試數(shù)據(jù)

對(duì)同一測(cè)試序列的事件施加不同的測(cè)試數(shù)據(jù)(即測(cè)試事件攜帶不同參數(shù))，就產(chǎn)生不同的測(cè)試?yán)终础Ｒ粋€(gè)測(cè)試序列對(duì)應(yīng)多個(gè)測(cè)試?yán)?/p>

測(cè)試集具有層次結(jié)構(gòu)：

1. 測(cè)試集由多個(gè)測(cè)試組組成既琴。每一測(cè)試組覆蓋某一類測(cè)試目的纹腌。
   比較常用的測(cè)試組劃分方法是根據(jù)協(xié)議的不同狀態(tài)霎终，為每一狀態(tài)的測(cè)試目的集合構(gòu)造一個(gè)測(cè)試組。測(cè)試組由多個(gè)測(cè)試?yán)M成升薯，每一測(cè)試?yán)槍?duì)某一測(cè)試目的莱褒。
2. 利用測(cè)試步(Test Step) ，可以將測(cè)試?yán)K化涎劈。所有測(cè)試步都是按照測(cè)試事件的順序或其它較小的測(cè)試步來定義的广凸，因此，全部測(cè)試步等效于測(cè)試事件的序列蛛枚。

3. 測(cè)試事件是測(cè)試?yán)蜏y(cè)試步的最小單位谅海，是測(cè)試步內(nèi)規(guī)范的基本單元。

   
   
   測(cè)試集的層次結(jié)構(gòu)

十蹦浦、測(cè)試表示方法

描述測(cè)試系統(tǒng)和IUT的行為扭吁。

通用的協(xié)議測(cè)試表示方法需滿足的要求：

1. 所描述的測(cè)試集應(yīng)該是系統(tǒng)獨(dú)立的。
2. 可以描述任一協(xié)議的一致性測(cè)試集盲镶。
3. 能為測(cè)試集的設(shè)計(jì)人員提供自動(dòng)或半自動(dòng)支持工具以加快測(cè)試集開發(fā)過程侥袜。
4. 降低整個(gè)測(cè)試集的開發(fā)和維護(hù)費(fèi)用。
5. 提高協(xié)議一致性測(cè)試集的標(biāo)準(zhǔn)化程度溉贿，以增強(qiáng)開放系統(tǒng)之間的互操作性枫吧。
6. 易于學(xué)習(xí)和掌握，對(duì)于測(cè)試操作人員而言宇色，易于理解九杂。

描述測(cè)試集的方法：

• SDL、ESTELLE宣蠕、LOTOS
• 編程語言
• 樹型記法尼酿、表型記法
  易于被測(cè)試人員理解。ISO將二者綜合植影，提出樹表組合記法TTCN裳擎。

TTCN：

TTCN提供兩種表示方法：樹型記法和表型記法
樹型記法主要用于描述測(cè)試事件之間的時(shí)序關(guān)系，即描述協(xié)議的動(dòng)態(tài)行為思币。
表型記法主要用于簡(jiǎn)化所有靜態(tài)數(shù)據(jù)的表示鹿响，如數(shù)據(jù)類型、PDU和ASP的格式谷饿、與測(cè)試事件相關(guān)聯(lián)的測(cè)試判決等等惶我。