數據鏈路層協議的設計分析

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