數(shù)據(jù)鏈路層協(xié)議的設(shè)計(jì)分析

petri網(wǎng)通信協(xié)議的分析在計(jì)算機(jī)網(wǎng)絡(luò)的體系結(jié)構(gòu)中，數(shù)據(jù)鏈路層位于第二層。數(shù)據(jù)鏈路層屏蔽了物理層的差異，并為網(wǎng)絡(luò)層提供了一個(gè)完整的接口，以便于當(dāng)前流行的tcp協(xié)議和ip地址。它不會(huì)受到底層的影響，也不會(huì)成功運(yùn)行。因此，對(duì)數(shù)據(jù)鏈路層的研究分析是非常重要的。Petri網(wǎng)是一種適合于并發(fā)、異步、分布式系統(tǒng)描述與分析的圖形數(shù)學(xué)工具，在通信協(xié)議的分析方面已經(jīng)成為最成功的應(yīng)用之一。為此，我們對(duì)一個(gè)基本數(shù)據(jù)鏈路層協(xié)議原有Petri網(wǎng)模型進(jìn)行了改進(jìn)及動(dòng)態(tài)行為分析，使其更加具有合理性。1網(wǎng)絡(luò)層和數(shù)據(jù)鏈路層、物理層在分析協(xié)議前，有必要假設(shè)兩個(gè)通用的理想狀態(tài)：網(wǎng)絡(luò)層、數(shù)據(jù)鏈路層、物理層是獨(dú)立的進(jìn)程；協(xié)議只考慮通信錯(cuò)誤，不考慮機(jī)器發(fā)生故障及重起引起的問題。1.1基于庫所等的petri網(wǎng)模型現(xiàn)實(shí)中，通信信道本身是不可靠的，在信道中傳輸?shù)臄?shù)據(jù)會(huì)發(fā)生丟失或者錯(cuò)誤。我們分析的是一個(gè)比較常規(guī)的噪聲信道的單工停等協(xié)議。由于所傳輸?shù)膸赡馨l(fā)生錯(cuò)誤，采用重發(fā)機(jī)制來彌補(bǔ)，引入定時(shí)器。假設(shè)發(fā)送方為A，接收方為B。A發(fā)送一幀的同時(shí)，保存該幀副本，并啟動(dòng)定時(shí)器，若在定時(shí)器溢出之前收到確認(rèn)幀，則明確知道已發(fā)送的幀被正確接收，于是刪除已發(fā)送幀的副本，并發(fā)送下一幀。如果此幀在傳輸過程中丟失，或者發(fā)生錯(cuò)誤被B拒絕，則無確認(rèn)幀發(fā)送，因而定時(shí)器溢出，A將重發(fā)該幀。若確認(rèn)幀ack丟失或損壞，則A無法意識(shí)到B已經(jīng)正確接收數(shù)據(jù)幀，A也會(huì)重發(fā)。這就會(huì)引起B(yǎng)收到重復(fù)的幀。為了解決這個(gè)問題，給每一幀加上序號(hào)。由于在該協(xié)議中采用停—等方式，我們只需將幀的序號(hào)最大定義為1。因此，A的發(fā)送次序?yàn)?幀、1幀、0幀、1幀……首先發(fā)送0幀，同時(shí)B被定義同樣的序號(hào)，即首先希望接收0幀，當(dāng)該幀正確接收后，希望接收的就是下一幀1幀。若返回的ack丟失或損壞，A重發(fā)0幀，當(dāng)重發(fā)的0幀到達(dá)B時(shí)，由于序號(hào)與此時(shí)B希望接收的幀的序號(hào)1不相符，則B意識(shí)到這是重復(fù)幀，從而拒絕該幀。文獻(xiàn)中已對(duì)該協(xié)議做出模型，具體模型參看文獻(xiàn)，233頁，F(xiàn)igure3-23ㄢ該模型是基于發(fā)送方、信道、接受方的嚴(yán)格邏輯狀態(tài)來定義庫所含義而建立模型的。我們也可以將邏輯狀態(tài)與實(shí)際情形相結(jié)合建立另外一個(gè)Petri網(wǎng)模型，此模型更加符合現(xiàn)實(shí)情況，容易理解。具體分析及建模如下：分別確定三方的庫所。對(duì)于發(fā)送方，所要發(fā)送的幀被附上序號(hào)以0幀、1幀交替發(fā)送，因此發(fā)送方需要兩個(gè)庫所，分別代表0幀、1幀的緩存器。在信道中傳輸狀態(tài)有三種：傳輸0幀、1幀、和確認(rèn)幀ack。對(duì)于接收方，相應(yīng)也需要0幀、1幀的緩存器，但是僅僅有兩個(gè)緩存器不能完整表現(xiàn)協(xié)議功能。因?yàn)闆]有體現(xiàn)出接收方只有正確接收到所期望的幀，才能進(jìn)入準(zhǔn)備接收下一幀的狀態(tài)。因此，我們認(rèn)為還應(yīng)加上兩個(gè)邏輯狀態(tài)，分別代表準(zhǔn)備接收0幀和1幀的狀態(tài)。變遷的設(shè)定需要尊重一個(gè)原則，即變遷能否發(fā)生及發(fā)生的影響完全取決于自然規(guī)律，不帶主觀性。為此，我們構(gòu)造如下Petri網(wǎng)模型：具體庫所、變遷代表的含義如下：S1、S6：分別代表發(fā)送方0幀、1幀緩存器S2、S7、S5：分別代表信道中正傳輸0幀、1幀、確認(rèn)幀ackS3、S8：分別代表接收方0幀、1幀緩存器S4：表示正確接收1幀后準(zhǔn)備接收0幀的狀態(tài)S9：表示正確接收0幀后準(zhǔn)備接收1幀的狀態(tài)t1、t8：定時(shí)器溢出t2、t6、t9：分別代表0幀、確認(rèn)幀、1幀丟失t3、t10：分別代表0幀、1幀接收t4、t11：分別代表經(jīng)過校驗(yàn)發(fā)現(xiàn)0幀、1幀錯(cuò)誤而丟棄t5：接收0幀并發(fā)送0幀的確認(rèn)幀ack，同時(shí)進(jìn)入準(zhǔn)備接收下一幀1幀的狀態(tài)t12：接收1幀并發(fā)送1幀的確認(rèn)幀ack，同時(shí)進(jìn)入準(zhǔn)備接收下一幀0幀的狀態(tài)t7：正確收到0幀的確認(rèn)幀，則刪除S1中緩存的0幀幅本，并將下一幀1幀發(fā)送到信道上同時(shí)在緩存器S6中保存此1幀的副本，啟動(dòng)定時(shí)器t13：正確收到1幀的確認(rèn)幀，則刪除S6中緩存的1幀幅本，并將下一幀0幀發(fā)送到信道上同時(shí)在緩存器S1中保存該幀副本，啟動(dòng)定時(shí)器t14：拒絕重復(fù)幀0幀，并再次返回確認(rèn)幀（如果0幀已經(jīng)被正確接收，則計(jì)數(shù)器S9變?yōu)榧せ顮顟B(tài)，即接收方已經(jīng)處于準(zhǔn)備接受1幀的狀態(tài)，而返回的確認(rèn)幀丟失，則發(fā)送方認(rèn)為此0幀發(fā)生錯(cuò)誤或者丟失，則重發(fā)，在接受方收到重復(fù)的0幀，拒絕并且再次返回確認(rèn)幀）t15：拒絕重復(fù)幀1幀，并再次返回確認(rèn)幀1.2噪聲信道的單工停等協(xié)議的性能分析協(xié)議的正確性驗(yàn)證主要包括以下幾個(gè)方面：協(xié)議的活性（無死鎖）；協(xié)議的循環(huán)可達(dá)性（能否按規(guī)定正常循環(huán)運(yùn)轉(zhuǎn)）；協(xié)議的一致性（協(xié)議的服務(wù)行為與協(xié)議內(nèi)部行為一致性）；協(xié)議的完備性（協(xié)議性質(zhì)符合協(xié)議環(huán)境的各要求）；協(xié)議的自恢復(fù)性（任何出錯(cuò)狀態(tài)都可自動(dòng)恢復(fù)到常態(tài)）；有界性（不會(huì)發(fā)生緩沖區(qū)溢出之類的問題）等。我們用可達(dá)樹對(duì)模型進(jìn)行分析，可達(dá)樹可以方便的分析系統(tǒng)的可達(dá)性、有界性、活性等各種動(dòng)態(tài)特性。用關(guān)聯(lián)矩陣來計(jì)算后繼標(biāo)識(shí)。寫出圖1的關(guān)聯(lián)矩陣：由初始標(biāo)識(shí)M0開始依次計(jì)算后繼標(biāo)識(shí)。M0=(110100000)T,t2發(fā)生時(shí)U(t2)=(010000000000000)T,所以M′=M0+CU=(110100000)T+(0-10000000)T=(100100000)T同理,可計(jì)算得各個(gè)變遷發(fā)生后的后繼標(biāo)識(shí)。畫出協(xié)議可達(dá)圖：分析可達(dá)圖，可以看出，該模型不存在死鎖現(xiàn)象，因?yàn)樗凶冞w都是活的，即此模型動(dòng)態(tài)運(yùn)行可達(dá)到的任何標(biāo)識(shí)狀態(tài)下都有變遷可啟動(dòng)并生成后繼標(biāo)識(shí)。而且協(xié)議循環(huán)可達(dá)。另外可以看到，變遷t2,t4,t6,t9,t11,t14,t15是我們不希望出現(xiàn)卻現(xiàn)實(shí)存在的發(fā)生錯(cuò)誤的變遷，在可達(dá)樹中都可以自動(dòng)循環(huán)恢復(fù)至常態(tài)。以上討論的是單工協(xié)議。在大多數(shù)實(shí)際環(huán)境中，數(shù)據(jù)傳輸是雙向的。實(shí)現(xiàn)全雙工數(shù)據(jù)傳輸?shù)姆椒ㄊ恰吧訋Т_認(rèn)”，將確認(rèn)幀附在發(fā)送的數(shù)據(jù)幀上，從而使得通信雙方都可發(fā)送數(shù)據(jù)。我們將雙向協(xié)議稱為滑動(dòng)窗口協(xié)議。由于實(shí)際的滑動(dòng)窗口協(xié)議較為復(fù)雜，因此建立Petri網(wǎng)模型的狀態(tài)空間比較大，更適合用高級(jí)Petri網(wǎng)進(jìn)行建模及分析。2協(xié)議的驗(yàn)證以上通過pertri網(wǎng)對(duì)基本數(shù)據(jù)鏈路層協(xié)議進(jìn)行了建模及改