摘 要：隨著計(jì)算機(jī)網(wǎng)絡(luò)協(xié)議的廣泛度和復(fù)雜度的增加，協(xié)議的形式化工作顯得越來越重要。Petri網(wǎng)與其他形式化建模技術(shù)相比，具有特別的優(yōu)越性，更加適用于通信協(xié)議的仿真與性能分析?；趦蓚€(gè)基本通信協(xié)議：stop—wait協(xié)議和CSMA/CD協(xié)議，用Petri網(wǎng)對(duì)他們進(jìn)行建模與仿真，對(duì)于協(xié)議開發(fā)與驗(yàn)證有重大意義。

關(guān)鍵詞：協(xié)議工程;隨機(jī)Petri網(wǎng);stop—wait協(xié)議;CSMA/CD協(xié)議

中圖分類號(hào)：TP393 文獻(xiàn)標(biāo)識(shí)碼：B

文章編號(hào)：1004373X(2008)0316603

Stochastic Petri Net Modeling Based on Communication Protocols

ZHANG Yahui，HU Xiaohui，GAO Jie

(Lanzhou Jiaotong University，Lanzhou，730070，China)

Abstract：With the increasing of popularity and complication of network protocols，the formal work of protocols become more and more important.cocompared with other Formal Description Techniques(FDT)，Petri net has its own superiority，it is more suited for modeling and analysis of communication protocols.This paper describes two essential network protocols:stop—wait protocol and CSMA/CD protocol used Petri net，which has great significance to the development and verification of protocols.

Keywords：protocol engineering;stochastic Petri net;stop—wait protocol;CSMA/CD protocol

1 網(wǎng)絡(luò)通信協(xié)議驗(yàn)證技術(shù)的研究方法比較

協(xié)議工程用形式化描述技術(shù)嚴(yán)格的設(shè)計(jì)和維護(hù)協(xié)議的各個(gè)活動(dòng)，建立準(zhǔn)確的協(xié)議模型，驗(yàn)證協(xié)議的邏輯正確性。目前協(xié)議工程已經(jīng)有一些網(wǎng)絡(luò)協(xié)議驗(yàn)證技術(shù)：基于FSM模型的協(xié)議驗(yàn)證與分析，基于時(shí)序邏輯的協(xié)議驗(yàn)證與分析，基于Petri網(wǎng)的協(xié)議驗(yàn)證與分析等[1]。FSM由于簡(jiǎn)單、直觀而得到廣泛應(yīng)用，但不易于描述復(fù)雜的系統(tǒng)，故不適于協(xié)議驗(yàn)證的實(shí)現(xiàn)。時(shí)序邏輯包括基于模態(tài)邏輯研究，狀態(tài)搜索和代數(shù)歸納證明。但他們有各自的缺陷，模態(tài)邏輯研究分析需要理想化協(xié)議，狀態(tài)搜索僅限于有限狀態(tài)，代數(shù)歸納證明工作量太大。

雖然用Petri網(wǎng)進(jìn)行協(xié)議驗(yàn)證也可能像FSM一樣會(huì)出現(xiàn)狀態(tài)爆炸的情況，但較其他技術(shù)，有其獨(dú)有的優(yōu)越性，表現(xiàn)在：用圖表示，清晰直觀；具有很好的適應(yīng)性，不僅能適應(yīng)計(jì)算機(jī)科學(xué)而且也適應(yīng)于其他領(lǐng)域；描述系統(tǒng)的并發(fā)行為，能得到系統(tǒng)行為信息；具有堅(jiān)實(shí)的數(shù)學(xué)基礎(chǔ)和分析技術(shù)，如可達(dá)性分析、不變量分析、保持特性的變換、構(gòu)造理論、形式語言理論等。對(duì)于網(wǎng)絡(luò)協(xié)議評(píng)價(jià)使用最多的隨機(jī)Petri網(wǎng)(SPN)，數(shù)學(xué)基礎(chǔ)是隨機(jī)過程，能定量地求解系統(tǒng)的主要性能指標(biāo)，如報(bào)文隊(duì)列長(zhǎng)度、吞吐量和丟包率等。

2 Petri網(wǎng)概述

Petri網(wǎng)是原聯(lián)邦德國Cart Adam Petri博士在20世紀(jì)60年代初提出的研究信息系統(tǒng)及其相互關(guān)系的數(shù)學(xué)模型，現(xiàn)在已成為具有嚴(yán)密數(shù)學(xué)基礎(chǔ)，多種抽象層次的通用網(wǎng)絡(luò)，并已得到了廣泛的應(yīng)用。

Petri網(wǎng)是一種包含兩種節(jié)點(diǎn)(位置、變遷)的有向圖，可描述事物的因果關(guān)系，同時(shí)可用Token的移動(dòng)來描述動(dòng)態(tài)系統(tǒng)。他有4個(gè)元素：位置、變遷、弧、令牌(Token)。他是一種圖示語言，一般用圓圈表示位置，方框表示轉(zhuǎn)移，帶箭頭線表示變遷，黑點(diǎn)表示Token。

定義[2]：N= (s，T，F(xiàn))稱作網(wǎng)，當(dāng)且僅當(dāng):

(1) S∪T≠，S ∩ T=

(2) F(S×T)∪(T×S)

(3) dom(F)∪cod(F)=S∪T，任意x∈S∪T，有#8226;x={y∈(y ∈S∪T)∧((y，x)∈F)}和x#8226;={y︳(y∈S∪T)∧((x，y)∈F)} ，稱#8226;x和x#8226;分別為x的前置集和后置集。

3 運(yùn)用Petri網(wǎng)對(duì)通信協(xié)議的建模

要進(jìn)行協(xié)議的驗(yàn)證和分析，建立協(xié)議模型是最基本也是最關(guān)鍵的一步。本文就基于Petri網(wǎng)對(duì)兩個(gè)典型的通信協(xié)議進(jìn)行建模。

3.1 stop—wait協(xié)議

stop—wait的思想：發(fā)送方傳送一幀后，在傳輸下一幀之前等待一個(gè)確認(rèn)，如果在某段時(shí)間之后確認(rèn)沒有到達(dá)，原發(fā)送方認(rèn)為超時(shí)，重發(fā)。需注意的是沒必要對(duì)每一次正確傳輸?shù)臄?shù)據(jù)包都回傳一個(gè)鏈路層的響應(yīng)，而只對(duì)出錯(cuò)的幀發(fā)響應(yīng)信號(hào)。若校驗(yàn)正確，就接著看發(fā)送方或者接受方是否有信息要發(fā)送給對(duì)方，若沒有信息則向?qū)Ψ桨l(fā)送一個(gè)鏈路層響應(yīng)正確信息，如果有信息內(nèi)容需要發(fā)送，則直接發(fā)送信息至對(duì)方而不需要再次發(fā)送正確的數(shù)據(jù)包。如圖1所示為stop—wait的交互工作。

圖1 stop—wait的交互工作

用SPN對(duì)此協(xié)議建模，他在每個(gè)變遷的可實(shí)施與實(shí)施之間聯(lián)系一個(gè)隨機(jī)延遲時(shí)間，連續(xù)時(shí)間隨機(jī)變量滿足指數(shù)分布。SPN與連續(xù)時(shí)間馬爾可夫鏈同構(gòu)[3]。庫所用圈表示，變遷用白長(zhǎng)方塊表示。

因?yàn)閷?shí)際網(wǎng)絡(luò)通信中，信道往往易受環(huán)境干擾和本身情況所限，使得通信狀況較差，因此必須在Petri模型中引入超時(shí)與出錯(cuò)雙重處理的機(jī)制。須考慮到所有干擾情況：

(1) 要發(fā)送的數(shù)據(jù)1或2在鏈路中丟失，超時(shí)重發(fā)；

(2) 收到數(shù)據(jù)1或2后發(fā)送回應(yīng)時(shí)回應(yīng)數(shù)據(jù)丟失，超時(shí)重發(fā)；

(3) 接收方等待數(shù)據(jù)1時(shí)卻收到數(shù)據(jù)2 ，接收方等待數(shù)據(jù)2時(shí)卻收到數(shù)據(jù)1，錯(cuò)誤重發(fā)。

建立的模型如圖2所示。

圖2 stop—wait協(xié)議模型

庫所說明：p1：發(fā)送方等待第1個(gè)幀的回應(yīng)。p2：發(fā)送方等待第2個(gè)幀的回應(yīng)。p3：第1幀在信道中。p4：第1幀的回應(yīng)在信道中。p5：第2幀的回應(yīng)在信道中。p6：第2幀在信道中。p7：接收方等待第2幀。p8：接收方等待第1幀。

變遷說明：t1：發(fā)送方發(fā)送第1幀。t2：發(fā)送方發(fā)送第2幀。t3：發(fā)送方等待第1個(gè)幀的回應(yīng)超時(shí)。t4:發(fā)送方等待第2個(gè)幀的回應(yīng)超時(shí)。t5：接收方收到第1幀。t6：接收方收到第2幀。t7：接收方等待第2幀時(shí)卻收到第1幀。t8:接收方等待第1幀時(shí)卻收到第2幀。t9：第1個(gè)幀丟失。t10:第1個(gè)幀的回應(yīng)丟失。t11:第2個(gè)幀的回應(yīng)丟失;t12:第2個(gè)幀丟失。

初始標(biāo)識(shí)：M0=(1，0，1，0，0，0，0，1)

建立好的stop—wait協(xié)議模型利用工具對(duì)其進(jìn)行可達(dá)性和不變量分析，如果協(xié)議所描述的狀態(tài)都是可達(dá)的，并且無死鎖，沒有無用循環(huán)，其最終狀態(tài)總是回到初始狀態(tài)，那么就是無沖突的活性模型，然后用Timenet工具分析得出各項(xiàng)性能指標(biāo)。

3.2 CSMA／CD協(xié)議

CSMA／CD[4] 是以太網(wǎng)中各個(gè)節(jié)點(diǎn)對(duì)總線資源訪問的仲裁機(jī)制，是以太網(wǎng)的基礎(chǔ)，對(duì)其進(jìn)行研究有利于深入了解以太網(wǎng)性能，因此對(duì)CSMA／CD協(xié)議進(jìn)行性能評(píng)價(jià)成為必須。CSMA／CD協(xié)議思想：當(dāng)一個(gè)站點(diǎn)產(chǎn)生一個(gè)新數(shù)據(jù)分組，他首先監(jiān)聽傳輸線路以判定任何正常進(jìn)行傳輸?shù)拇嬖?。如果線路正忙，分組的傳輸被延時(shí)直到線路變?yōu)殚e置。此時(shí)站點(diǎn)等待一個(gè)短時(shí)間的延時(shí)d后，不管線路狀態(tài)而傳輸這個(gè)分組，在分組傳送期間線路被監(jiān)督一側(cè)是其他傳輸?shù)呐鲎?。若一個(gè)碰撞被檢測(cè)到，傳輸立即停止，線路被干擾一個(gè)短時(shí)間以保證所有站點(diǎn)都識(shí)別到這個(gè)碰撞。這個(gè)分組傳輸在一個(gè)隨機(jī)的延時(shí)后再重新調(diào)度發(fā)送。站點(diǎn)假定沒有緩沖功能，只有在前一個(gè)傳輸發(fā)送后才能接受新的傳輸要求。

此處用DSPN(確定與隨機(jī)Petri網(wǎng))來描述CSMA／CD協(xié)議，DSPN[3]是SPN的一種擴(kuò)充，主要表現(xiàn)在時(shí)間變遷的實(shí)施延時(shí)既可以是常數(shù)(確定時(shí)間變遷)，也可以是指數(shù)分布的隨機(jī)變量(指數(shù)時(shí)間變遷)當(dāng)然也可以有瞬時(shí)變遷。且可有禁止弧(禁止弧所連接的位置的原可實(shí)施條件變?yōu)椴豢蓪?shí)施條件，原不可實(shí)施條件變?yōu)榭蓪?shí)施條件，且在相連變遷是實(shí)施時(shí)沒有標(biāo)記從相連位置移出)。確定時(shí)間變遷用黑長(zhǎng)方塊表示，指數(shù)時(shí)間變遷用白長(zhǎng)方塊表示，瞬時(shí)變遷用黑粗線表示。建模如圖3所示。

庫所說明：thi:思考狀態(tài)，其中有token代表網(wǎng)絡(luò)中有發(fā)送請(qǐng)求，其中的token表示連接到 Lan總線的站點(diǎn)的數(shù)量。back：后備狀態(tài)，碰撞出現(xiàn)后但還沒有重新發(fā)送數(shù)據(jù)。line:站點(diǎn)要進(jìn)行分組傳輸。bfree：總線處于空閑狀態(tài)。frig：傳輸開始的脆弱狀態(tài)，脆弱狀態(tài)就是當(dāng)一個(gè)站點(diǎn)正在傳輸時(shí)，他的信號(hào)還沒有傳到距其最遠(yuǎn)的站點(diǎn)，因此，他并不知最遠(yuǎn)站點(diǎn)是否傳輸，此時(shí)他檢測(cè)到的總線仍是空閑，他仍繼續(xù)傳輸?shù)臓顟B(tài)beginx：傳輸開始前等待檢測(cè)的狀態(tài)。endfrig：沒有碰撞，脆弱狀態(tài)結(jié)束。beftran：準(zhǔn)備好分組傳輸。relbus：總線使用完畢。biginjam：放置其他站點(diǎn)傳輸要求(有沖突)。knowjam：確認(rèn)傳輸出現(xiàn)沖突。jam：第二個(gè)分組傳輸被干擾狀態(tài)。endjam：干擾結(jié)束。begining：站點(diǎn)等待。begin：當(dāng)前正要傳輸?shù)牡谝粋€(gè)站點(diǎn)。

圖3 CSMA／CD的DSPN模型

變遷說明：thi：思考時(shí)間變遷，實(shí)施速率正比于thi中標(biāo)記數(shù)量。back：后備時(shí)間變遷，實(shí)施速率正比于back中標(biāo)記數(shù)量。first：進(jìn)入第一個(gè)站點(diǎn)傳輸。dist：模擬兩站點(diǎn)之間距離的指數(shù)變遷。nocol：沒有碰撞，結(jié)束脆弱狀態(tài)，使位置endfrig變空。efrig：若沒有碰撞發(fā)生，他的實(shí)施使frig變空，截止dist實(shí)施。tran：進(jìn)行并完成分組傳輸。beginx：占有總線。nobody：line中沒有傳輸要求，實(shí)施使總線處于空閑狀態(tài)bfree。somebody：line中有傳輸要求，則實(shí)施開始準(zhǔn)備傳輸下面的分組begin。conf：因?yàn)橛袥_突，通道請(qǐng)空。senconf：確認(rèn)沖突。jam：沖突干擾結(jié)束。endback：第一個(gè)沖突站點(diǎn)變?yōu)楹髠錉顟B(tài)，釋放總線。dela：

近似模擬一對(duì)站點(diǎn)的傳播延時(shí)。delay：數(shù)據(jù)包傳輸前所經(jīng)歷的延時(shí)。started：只要第一個(gè)站點(diǎn)開始傳輸，他就從begining向beginjam移動(dòng)token，以阻塞其他站點(diǎn)。 others：在脆弱狀態(tài)期間有其他站點(diǎn)發(fā)出傳輸要求，他把此要求于startjam中。baking：把token從sensejam移到back。

用DSPNexpress—NG工具分析模型的各項(xiàng)性能指標(biāo)，DSPNexpress是德國Dortmund大學(xué)的Lindeman教授開發(fā)的DSPN軟件，DSPNexpress—NG是DSPNexpress的升級(jí)版，是功能強(qiáng)大的DSPN分析軟件[6]。

4 結(jié) 語

Petri網(wǎng)是一種適于系統(tǒng)描述與分析的數(shù)學(xué)模型，能夠很好地描述系統(tǒng)結(jié)構(gòu)與系統(tǒng)行為，他在描述并發(fā)、沖突、同步等重要行為現(xiàn)象所表現(xiàn)出的優(yōu)勢(shì)以及具有形式化步驟與數(shù)學(xué)圖論相支持的理論嚴(yán)密性，特別是其圖形表達(dá)直觀和便于編程實(shí)現(xiàn)的技術(shù)特點(diǎn)尤其適合并發(fā)任務(wù)系統(tǒng)的設(shè)計(jì)，在協(xié)議工程領(lǐng)域有著廣闊的前景。

參考文獻(xiàn)

[1]Billington J.Protocol Engineering and Nets[C].In：Proceedings of the 8th European Workshop on Application and Theory of Perti Nets，1987:137—156.

[2]袁崇義.Petri 網(wǎng)原理[M].北京:電子工業(yè)出版社，1998.

[3]林闖.計(jì)算機(jī)網(wǎng)絡(luò)和計(jì)算機(jī)系統(tǒng)的性能分析[M].北京：清華大學(xué)出版社，2001.

[4]謝希仁.計(jì)算機(jī)網(wǎng)絡(luò)[M].北京：電子工業(yè)出版社，2003.

[5]ChristophLindemann，Gerald S Shedler.Numerical Analysis of Deterministic and Stochastic Petri Nets with Concurrent Deterministic Transitions[J].Performance Evaluation，1996(10):565—582.

注：本文中所涉及到的圖表、注解、公式等內(nèi)容請(qǐng)以PDF格式閱讀原文。