蔡俊杰

?

一種使用Petri網(wǎng)絡(luò)模型驗(yàn)證協(xié)議的方法

蔡俊杰

隨著計(jì)算機(jī)網(wǎng)絡(luò)的高速發(fā)展，開(kāi)發(fā)新型的網(wǎng)絡(luò)協(xié)議成為熱點(diǎn)研究課題。而新型網(wǎng)絡(luò)協(xié)議的描述與驗(yàn)證又成為研究的關(guān)鍵。引入Petri網(wǎng)絡(luò)模型，給出了一種協(xié)議驗(yàn)證的方法。通過(guò)描述Petri網(wǎng)絡(luò)模型，該模型以其良好的直觀性，為協(xié)議驗(yàn)證過(guò)程提供了極大的方便。并且提出了針對(duì)復(fù)雜的協(xié)議，可分解為若干個(gè)小部分，使用Petri模型，加之以有窮狀態(tài)自動(dòng)機(jī)和高級(jí)語(yǔ)言，可較完善地解決其描述和驗(yàn)證問(wèn)題。所述的驗(yàn)證方法對(duì)于協(xié)議工程（protocol engineering）領(lǐng)域的研究，新的協(xié)議軟件的產(chǎn)生，有著積極的推動(dòng)作用。

Petri網(wǎng)絡(luò)模型；點(diǎn)火；狀態(tài)變遷；可達(dá)樹(shù)

0 引言

當(dāng)前，網(wǎng)絡(luò)技術(shù)的發(fā)展已經(jīng)進(jìn)入了一個(gè)全新的時(shí)代。OSI參考模型的出現(xiàn)為解決異構(gòu)系統(tǒng)的互連做出了重要貢獻(xiàn)。但是，由于對(duì)OSI協(xié)議的開(kāi)發(fā)仍常常由許多不同人員甚至是不同單位的人員進(jìn)行的。因此，如何系統(tǒng)地開(kāi)發(fā)協(xié)議軟件，以確保在不同實(shí)現(xiàn)之間能協(xié)調(diào)地工作，仍是一個(gè)十分重要的問(wèn)題。為了有效地解決這個(gè)問(wèn)題，本文給出了一種使用Petri網(wǎng)絡(luò)模型對(duì)協(xié)議進(jìn)行驗(yàn)證的方法。

1 Petri網(wǎng)絡(luò)模型定義

Petri網(wǎng)絡(luò)模型是一種特殊的自動(dòng)機(jī)模型。它可以用來(lái)描述通訊系統(tǒng)中各異步成分之間的關(guān)系。這種自動(dòng)機(jī)也是一種變遷模型。它允許同時(shí)發(fā)生多個(gè)狀態(tài)的變遷，因此Petri網(wǎng)是一種并發(fā)模型。在描述各種協(xié)議的過(guò)程中時(shí)，采用Petri網(wǎng)絡(luò)模型是非常方便的，下面介紹Petri網(wǎng)的基本概念，并舉例說(shuō)明它在描述協(xié)議方面的應(yīng)用。

包（bag）是集合的擴(kuò)展，和集合相似，包也是某個(gè)域中元素的集合。但是在包里，元素可以多次出現(xiàn)。例如：

B1=｛a,b,c｝，B2=｛a｝，B3=｛a,a,a｝，B4=｛a,b,c,c｝，B5=｛c,c,b,b｝。B1和B2就是集合，B3~B5則不是集合。

將元素x在包B中出現(xiàn)的次數(shù)記為#（x,B）, 在上述例子中#（a,B1）=1，#（a,B3）=3。

當(dāng)元素x為包B中的成員時(shí)，#（a,B3）=3。

當(dāng)元素x為包B中成員時(shí)，#（x,B）>0。此時(shí)可寫(xiě)為x∈B。包B的基數(shù)定義為|B|=。在上述例子中|B5|=4。

域D是一個(gè)包中各元素的集合。Dn則是包的空間，它是元素在D中且每個(gè)元素出現(xiàn)不超過(guò)n次的所有包的集合。例如，當(dāng)D=｛a,b,c,d｝，則D2=｛｛a,b,c,d｝,{a,a,b,b},{a,a,c,d},…｝。若B∈Dn則對(duì)于B：（1）若x∈B，則x∈D；（2）對(duì)所有的x，#（x，B）≤n。

集合D∞是域在D中所有包的集合。在每個(gè)包中元素出現(xiàn)的次數(shù)是沒(méi)有限制的。

Petri網(wǎng)的定義

在上述關(guān)于包的一些基本概念之基礎(chǔ)上，可以將Petri網(wǎng)定義為一個(gè)四元組C=（P，T，I，O），其中：

P=｛p1,p2, …pn｝是位置(place)的有窮集合；

T=｛t1,t2, …,tm｝是變遷的有窮集合，且T與P不相交，即T∩P=φ。

I是輸入函數(shù)，是變遷T到位置包的映射，即I：T →P∞。對(duì)于每一個(gè)tk∈T，可以得出相應(yīng)的I（tk）={pi,pj, …}。

O是輸入函數(shù)，也是一種變遷到位置包的映射，即O：T →P∞。對(duì)于每一個(gè)對(duì)于每一個(gè)tj∈T，可以得出相應(yīng)的O（tk）={pr,ps, …}。

一個(gè)Petri網(wǎng)的圖形表示法如圖1所示：

圖1 Petri網(wǎng)的構(gòu)成舉例

圓圈代表位置。位置又稱為節(jié)點(diǎn)或條件。圖1 中的位置共5個(gè)。位置集合為P={p1,p2,p3,p4,p5}。短的線段代表變遷。變遷又稱為事件?，F(xiàn)在共有3個(gè)變遷，變遷集合T=｛t1,t2,t3｝。帶箭頭的直線或弧線指出一個(gè)變遷的輸入和輸出位置有哪些。

例如，在圖1中：

I（t1）=｛p1｝,I（t2）=｛p2,p3,p4,p4｝，I（t3）=｛p5｝,

O（t1）={ p2,p3,p4}，O（t2）={p3,p4}。

在Petri網(wǎng)中最值得注意的就是位置圓圈中的黑點(diǎn)，稱之為標(biāo)記（token）。每一個(gè)位置中可以有1個(gè)或多個(gè)標(biāo)記，當(dāng)然也可以沒(méi)有標(biāo)記。Petri網(wǎng)所處的狀態(tài)是由標(biāo)記的分布決定的。在位置pi中的標(biāo)記個(gè)數(shù)常用μi來(lái)表示。在圖1 中μ1=2，μ2=μ3=μ4=μ5=0。這也可以用向量μ=（μ1，μ2，…μn）來(lái)表示整個(gè)Petri網(wǎng)的標(biāo)記分布情況?？梢钥闯?，現(xiàn)在μ=（2，0，0，0，0）。

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

一個(gè)Petri網(wǎng)的狀態(tài)變遷取決于以下兩個(gè)條件：

必須有1個(gè)或多個(gè)變遷滿足變遷條件。變遷條件就是某個(gè)變遷ti的所有輸入位置中都必須有標(biāo)記存在，并且當(dāng)輸入位置有多根弧線指向這個(gè)變遷時(shí)，該輸入位置也至少具有和弧線根數(shù)相等的標(biāo)記數(shù)。這一條件可寫(xiě)為公式（1）：

對(duì)所有Pi∈I（tj）, μ（pi）≥#(Pi,I(tj)) （1）

對(duì)于圖1的例子，只有t1滿足變遷條件。

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

發(fā)生點(diǎn)火后，標(biāo)記要重新分布。標(biāo)記移動(dòng)的規(guī)則是：從點(diǎn)火的變遷tj的所有輸入位置中均取出標(biāo)記，每個(gè)位置取出的標(biāo)記數(shù)等于該位置指向點(diǎn)火的tj的弧線數(shù)；然后再將標(biāo)記送入tj的所有輸出位置中去，送入每個(gè)位置的標(biāo)記數(shù)等于tj指向該位置的弧線數(shù)。顯然，點(diǎn)火前后的標(biāo)記總數(shù)一般是不守恒的。上述規(guī)則可用公式表示，設(shè)點(diǎn)火標(biāo)記前標(biāo)記的分布為μ（pi），則當(dāng)tj點(diǎn)火后，新的標(biāo)記分布μ’（pi）可寫(xiě)為公式（2）：

μ’（pi）=μ（pi）- #（pi,I（tj））+#（pi,O（tj））（2）

可見(jiàn)，對(duì)于既非tj的輸入位置又非tj的輸出位置的其它所有位置，其中的標(biāo)記數(shù)在點(diǎn)火前后不發(fā)生變化。

仍以圖1的Petri網(wǎng)為例，標(biāo)記的初始分布為μ=（2，0，0，0，0）。顯然，只有t1滿足變遷條件。當(dāng)發(fā)生使t1點(diǎn)火的事件后，標(biāo)記的分布變?yōu)棣獭?=（1，1，1，1，0）。若t1再次點(diǎn)火，則點(diǎn)火后的標(biāo)記分布為μ’’=（0，2，2，2，0），這時(shí)t2已具備點(diǎn)火條件。在t2點(diǎn)火后，新的標(biāo)記分布變?yōu)棣獭?（0，2，1，0，0）。至此，該P(yáng)etri網(wǎng)已不能再發(fā)生任何點(diǎn)火了。至于實(shí)際的應(yīng)用中，究竟是t1還是t2點(diǎn)火，那就要看具體的條件了。

一個(gè)Petri網(wǎng)中的變遷大致有以下3種類(lèi)型，如圖2所示：

圖2 Petri網(wǎng)中的幾種典型變遷

一種是順序變遷，如圖2（a）所示，只有當(dāng)t1點(diǎn)火后t2才能點(diǎn)火。另一種是并發(fā)變遷，如圖2（b）所示，t1和t2可同時(shí)（當(dāng)然也可以是單獨(dú)地）點(diǎn)火。第三種是互斥變遷，如圖2（c）所示，t1和t2中只有一個(gè)能點(diǎn)火，一個(gè)點(diǎn)火后另一個(gè)就不能再點(diǎn)火了。至于在實(shí)際中是t1還是t2點(diǎn)火，那就要看具體的條件了。

3 使用Petri網(wǎng)對(duì)協(xié)議進(jìn)行描述

下面以甲乙雙方用停止等待協(xié)議通信為例，來(lái)說(shuō)明如何使用Petri網(wǎng)對(duì)協(xié)議進(jìn)行描述，如圖3所示：

圖3 半雙工通信的停止等待協(xié)議的Petri網(wǎng)模型

在圖3中，共有7個(gè)位置和12個(gè)變遷。開(kāi)始時(shí)，各位置中均無(wú)標(biāo)記，因此，點(diǎn)火只能從t1開(kāi)始。t1實(shí)際上就是整個(gè)系統(tǒng)初始化，同時(shí)由甲方發(fā)出0號(hào)幀。t1點(diǎn)火后，位置p1、p3和p7中就各具有一個(gè)標(biāo)記。在這種狀態(tài)下，顯然有3個(gè)變遷（t4、t6和t11）是滿足變遷條件的。這時(shí)究竟哪個(gè)變遷點(diǎn)火，則要根據(jù)通信的具體情況而定。若0號(hào)幀丟失或出錯(cuò)，則t6點(diǎn)火，p3中的標(biāo)記即移走（不進(jìn)入任何位置），這時(shí)唯一能夠點(diǎn)火的只有t4（超時(shí)）了。整個(gè)協(xié)議都描述得十分清楚，讀者可依此自行研究每一種變遷在什么條件下方能點(diǎn)火，以及各種狀態(tài)的轉(zhuǎn)換過(guò)程。

當(dāng)然Petri網(wǎng)同樣存在著當(dāng)協(xié)議較復(fù)雜時(shí)出現(xiàn)過(guò)多的位置和變遷，以致很難在圖上將協(xié)議描述清楚。但是由于Petri有標(biāo)記及點(diǎn)火機(jī)制，使得Petri網(wǎng)在驗(yàn)證協(xié)議的正確性方面成為很有用的工具。

Petri網(wǎng)模型屬于狀態(tài)變遷模型，用這種模型描述協(xié)議的最大優(yōu)點(diǎn)就是直觀性好，同時(shí)也便于協(xié)議的驗(yàn)證。

4 使用Petri網(wǎng)對(duì)協(xié)議進(jìn)行驗(yàn)證

使用Petri網(wǎng)不但可以很直觀地對(duì)協(xié)議進(jìn)行描述，而且可以對(duì)協(xié)議進(jìn)行驗(yàn)證。具體而言，利用Petri網(wǎng)的可達(dá)樹(shù)（reachability tree）可以很方便地對(duì)協(xié)議的若干重要方面進(jìn)行驗(yàn)證。

下面以圖3中的協(xié)議為例。在一開(kāi)始t1點(diǎn)火，標(biāo)記移入位置p1,p3,p7。協(xié)議的這種狀態(tài)簡(jiǎn)稱為（1，3，7）。這相當(dāng)于以前提到過(guò)的標(biāo)記分布μ=（1,0,1,0,0,0,1）。將狀態(tài)（1，3，7）作為可達(dá)樹(shù)的根，如圖4所示：

圖4 Petri網(wǎng)的可達(dá)樹(shù)舉例

再尋找所有滿足條件的變遷。找出當(dāng)這些變遷點(diǎn)火后所達(dá)到的狀態(tài)。例如，t11和t6都滿足變遷條件而其余都不滿足變遷條件。若t11點(diǎn)火，則狀態(tài)變?yōu)?1，4，6，而當(dāng)t6點(diǎn)火后，標(biāo)記少了一個(gè)狀態(tài)為（1，7）。這樣一步一步地進(jìn)行下去，直到出現(xiàn)一個(gè)重復(fù)的狀態(tài)為止，例如在狀態(tài)（1，7）下，t4點(diǎn)火，狀態(tài)變?yōu)椋?，3，7），是個(gè)曾經(jīng)出現(xiàn)過(guò)的狀態(tài)。于是可在此狀態(tài)下劃兩道線，表示不再?gòu)脑摴?jié)點(diǎn)上繼續(xù)尋找可達(dá)樹(shù)。

當(dāng)遍歷所有可能的點(diǎn)火和可能出現(xiàn)的狀態(tài)，并且所有的樹(shù)葉都成為重復(fù)的狀態(tài)時(shí)，Petri網(wǎng)的可達(dá)樹(shù)即構(gòu)成。

從圖4得出的結(jié)果可以看出，協(xié)議中的所有可能狀態(tài)從初始狀態(tài)開(kāi)始都是可達(dá)的，還可以看出，由于所有的樹(shù)葉都是重復(fù)狀態(tài)，因此，這樣的協(xié)議不可能出現(xiàn)死鎖。從可達(dá)樹(shù)還可看出，本例也不會(huì)出現(xiàn)死循環(huán)。

還可檢驗(yàn)出協(xié)議的動(dòng)作序列都是正確的。例如，甲方從位置1到位置2再回到位置1時(shí)，t11和t12均只各點(diǎn)火一次，而且必須點(diǎn)火一次。這就保證了送交主機(jī)的幀沒(méi)有遺漏，也沒(méi)有重復(fù)。

大家還可注意到，若單純從圖3來(lái)考慮，則只要位置p1（或p2）中有標(biāo)記，則t4（或t5）在任何時(shí)刻均可點(diǎn)火。例如在狀態(tài)（1，3，7）時(shí)，t1點(diǎn)火后，使?fàn)顟B(tài)變?yōu)椋?，32，7），這里32表示在位置3中有兩個(gè)標(biāo)記。若t1再次點(diǎn)火，則狀態(tài)又變?yōu)椋?，32，7）。然而根據(jù)超時(shí)定時(shí)器控制原理，剛發(fā)出魂的幀還在信道中就接連再重發(fā)這個(gè)幀是不合理的，因此這種不合理的變遷沒(méi)有反映在圖4的可達(dá)樹(shù)中。但是當(dāng)t4（或t5）點(diǎn)火時(shí)間不受任何限制時(shí)，位置3（或5）中的標(biāo)記數(shù)將無(wú)限制地增加（因而位置4也會(huì)這樣）。這樣的Petri網(wǎng)稱為無(wú)界的。與之相對(duì)應(yīng)的是無(wú)窮狀態(tài)自動(dòng)機(jī)。實(shí)際是有用的協(xié)議都不會(huì)是這樣。

從上述情況可以看出，Petri網(wǎng)許多特性均可以用來(lái)進(jìn)行協(xié)議的驗(yàn)證，但是對(duì)于復(fù)雜的協(xié)議，狀態(tài)數(shù)目將達(dá)到無(wú)法進(jìn)行實(shí)驗(yàn)的程度，些時(shí)使用Petri網(wǎng)來(lái)解決驗(yàn)證問(wèn)題就有困難。大家認(rèn)為，此時(shí)將復(fù)雜的協(xié)議分解為若干個(gè)較小的部分，然后對(duì)這些小的部分進(jìn)行驗(yàn)證。當(dāng)協(xié)議中包含多個(gè)定時(shí)器時(shí)，要注意這些定時(shí)器設(shè)定時(shí)間的相互協(xié)調(diào)，盡量避免進(jìn)程之間信息傳送時(shí)間的延時(shí)。

總言之，解決協(xié)議的驗(yàn)證問(wèn)題，應(yīng)當(dāng)減少人工的干預(yù)，這樣才能使復(fù)雜協(xié)議的驗(yàn)證工作大大簡(jiǎn)化。

5 總結(jié)

網(wǎng)絡(luò)協(xié)議的研究一直是網(wǎng)絡(luò)技術(shù)研究的重要課題。本文所描述的Petri網(wǎng)絡(luò)模型屬于變遷模型，使用這種模型描述并驗(yàn)證協(xié)議的直觀性好，優(yōu)點(diǎn)明顯。對(duì)于非常復(fù)雜的協(xié)議的驗(yàn)證，Petri網(wǎng)絡(luò)模型與有窮狀態(tài)自動(dòng)機(jī)結(jié)合，對(duì)于協(xié)議的細(xì)節(jié)，輔之以高級(jí)語(yǔ)言來(lái)描述，這樣使得協(xié)議的描述和驗(yàn)證均比較方便。本文所闡述的Petri網(wǎng)模型對(duì)協(xié)議的描述與驗(yàn)證方法，對(duì)于新型網(wǎng)絡(luò)協(xié)議的研究具有積極的推動(dòng)作用，具有一定的實(shí)用價(jià)值。

參考文獻(xiàn)：

[1] 嚴(yán)偉,潘愛(ài)民(譯)．計(jì)算機(jī)網(wǎng)絡(luò)[M]．清華大學(xué)出版社,2012(03)．

[2] 謝希仁．計(jì)算機(jī)網(wǎng)絡(luò)[M]．電子工業(yè)出版社,2013(06)．

[3] (美國(guó))科姆．計(jì)算機(jī)網(wǎng)絡(luò)與因特網(wǎng)[M]．清華大學(xué)出版社,2010(09)．

[4] 程莉．計(jì)算機(jī)網(wǎng)絡(luò)[M]．科學(xué)出版社,2012(04)．

[5] 李成忠．計(jì)算機(jī)網(wǎng)絡(luò)[M]．清華大學(xué)出版社,2010(07)．

[6] 段標(biāo), 尹曉勇．計(jì)算機(jī)網(wǎng)絡(luò)基礎(chǔ)[M]．電子工業(yè)出版社,2012(08)．

[7] 楊琰,廖偉志,李文敬,楊文,李杰．基于Petri網(wǎng)的顧及轉(zhuǎn)向延誤的最優(yōu)路徑算法[J]. 計(jì)算機(jī)工程與設(shè)計(jì),2013,34(10): 3643-3648．

[8] 薛晨,任大勇．基于時(shí)延Petri網(wǎng)的雙重?cái)?shù)字簽名技術(shù)研究[J].計(jì)算機(jī)與數(shù)字工程,2013,41(9):1485-1488.

[9] 傅作為樂(lè)曉波．基于Petri網(wǎng)的擴(kuò)展工作流模型研究[J]. 計(jì)算機(jī)應(yīng)用與軟件,2013,30(9): 173-175．

[10] 任大勇．基于時(shí)延Petri網(wǎng)的移動(dòng)電子支付協(xié)議模型[J].計(jì)算機(jī)與數(shù)字工程,2013,41(10):1622-1624.

Method of Protocol Validation by Using Petri Network Model

Cai Junjie

(Zhaoqing Broadcast Television University, Zhaoqing 526060, China)

With the rapid development of computer networks, the development of new network protocol has become a hot research topic. The description and validation of a new network protocol has become the key of research. This paper introduces the Petri network model, and gives the method of protocol verification. Through the description of the Petri network model, the model provides convenience for protocol verification process with good visibility. And the complex protocols can be decomposed into several small parts. By using the Petri model, it can be a better solution to the problem description and validation combining with the finite state automata and advanced language. Validation of the method presented in this paper for the protocol engineering (Protocol Engineering) research in the field and the new protocol software, has a positive role in promoting.

Petri Network model; Ignition; State Transition; Reachability Tree

1007-757X(2016)04-0078-03

TP393

A

（2015.10.15）

蔡俊杰（1968-），男，安徽人，肇慶廣播電視大學(xué)，講師。研究方向：計(jì)算機(jī)通信、計(jì)算機(jī)網(wǎng)絡(luò)安全、信息安全等，肇慶，526060