一種基于ＣＩＰＮ的網(wǎng)絡(luò)協(xié)議建模方法

(1.電子科技大學(xué) 計算機(jī)科學(xué)與工程學(xué)院，成都 610054；2.中國科學(xué)院 深圳先進(jìn)技術(shù)研究院， 廣東 深圳 518067)

摘要：基于Petri網(wǎng)的網(wǎng)絡(luò)協(xié)議建模技術(shù)需要更有效地與現(xiàn)有通用網(wǎng)絡(luò)協(xié)議仿真技術(shù)協(xié)同工作，結(jié)合CPN和IPN，提出了一種新的Petri網(wǎng)派生類CIPN用于網(wǎng)絡(luò)協(xié)議的建模和形式化分析，突出了協(xié)議的離散事件系統(tǒng)特性。給出了CIPN的定義，并討論了CIPN的運(yùn)行機(jī)制，證明了CIPN事件可觀測性的充要條件。通過一個MACA協(xié)議作為示例，完成了從網(wǎng)絡(luò)協(xié)議的一般CPN模型到CIPN模型的等價性轉(zhuǎn)換，并利用CIPN的事件可觀測性定理對MACA協(xié)議進(jìn)行了事件觀測性分析。

關(guān)鍵詞：網(wǎng)絡(luò)協(xié)議；離散事件系統(tǒng)；著色解釋Petri網(wǎng)；協(xié)議工程

中圖分類號：TP393文獻(xiàn)標(biāo)志碼：A

文章編號：1001-3695(2008)11-3430-04



Novel CIPN-based modeling for network protocols



PENG Lei1，2，BI Ya-lei2，ZENG Jia-zhi1

（1.School of Computer Science Engineering ，University of Electronic Science Technology of China， Chengdu Sichuan610054， China；2.Shenzhen Institute of Advanced Technology， Chinese Academy of Sciences， Shenzhen Guangdong 518067， China）

Abstract:The Petri net-based modeling technique for network protocols need cooperate with existing network protocol simulators more effectively. Combing CPN and IPN together， this paper introduced a novel descent of Petri net named CIPN in order to get a model highlighting the DES essence and take a formal analysis easily. Then discussed definition and operation mechanism of CIPN.Also the necessary and sufficient condition for event observability of CIPN got proofed. A MACA protocol-based example shows that the transmission from CPN model to its equative CIPN counterpart. And analyzed the event observability of MACA with employing event observability theorem in CIPN.

Key words:network protocols;discrete event system (DES);colored interpreted Petri nets (CIPN);protocol engineering



0引言

通信協(xié)議是一類特殊的軟件，工作于系統(tǒng)內(nèi)核，空間分布性、并發(fā)性、異步性是協(xié)議運(yùn)轉(zhuǎn)時的主要特點。同時，通信協(xié)議為用戶透明了網(wǎng)絡(luò)，使之成為一個可靠的比特管道。因此通信協(xié)議的完整性、正確性、安全性是衡量一個通信協(xié)議設(shè)計質(zhì)量的關(guān)鍵指標(biāo)，一旦協(xié)議部署，糾正錯誤的代價就非常昂貴，同時也會造成用戶對網(wǎng)絡(luò)系統(tǒng)的極大失望。 要保證協(xié)議設(shè)計優(yōu)良，必須引入規(guī)范化的方法來引導(dǎo)協(xié)議設(shè)計，這就是所謂的協(xié)議工程（protocol engineering， PE）^[1]。

在繼承了軟件工程的一些共有理念和基本流程后，協(xié)議工程引入了形式化描述技術(shù)（formal description technique，F(xiàn)DT）^[2]，貫穿于協(xié)議開發(fā)的各階段，起始于協(xié)議規(guī)范描述，以保證在協(xié)議設(shè)計過程中，可對協(xié)議進(jìn)行形式化分析和求解，從而使協(xié)議的研究開發(fā)可以獨(dú)立于非形式的自然語言文本和最終實現(xiàn)代碼，避免了協(xié)議驗證測試的復(fù)雜性。

形式化的協(xié)議行為分析是協(xié)議工程中非常重要的環(huán)節(jié)。一種主要的思路是基于Petri網(wǎng)理論對協(xié)議展開研究^[3]，主要從協(xié)議行為和協(xié)議性能這兩個方面來進(jìn)行分析。協(xié)議性能分析主要對協(xié)議的網(wǎng)絡(luò)開銷、信道利用率、吞吐率等指標(biāo)使用時延Petri和隨機(jī)Petri進(jìn)行建模分析；協(xié)議行為分析主要針對協(xié)議的設(shè)計與實現(xiàn)，包括對協(xié)議的容錯和魯棒性的研究，現(xiàn)多使用高級Petri網(wǎng)如著色Petri網(wǎng)^[4]、層次Petri網(wǎng)進(jìn)行建模。

目前的現(xiàn)狀是協(xié)議工程的研究進(jìn)展并不理想，遠(yuǎn)遠(yuǎn)落后于軟件工程。除了協(xié)議自身的特殊性，

協(xié)議工程中缺乏貫穿工程全階段的一致模型是一大因素，這使得各階段的工作難以環(huán)環(huán)相扣，基于Petri網(wǎng)的形式化分析的結(jié)論或成果難以直接指導(dǎo)協(xié)議的仿真與研發(fā)行為。

現(xiàn)在主流的協(xié)議仿真工具如NS2、OPNET的通用仿真，或如TOSSIM這種只針對于TinyOS上的WSN協(xié)議仿真，無不使用DES作為協(xié)議模型的驅(qū)動機(jī)制。因此，考慮基于DES機(jī)制構(gòu)建形式化的協(xié)議行為分析網(wǎng)是解決上文中提出的保持模型一致性的有效方法。

IPN^[5]是近年來Petri網(wǎng)的又一變種，比較適合用來構(gòu)建DES系統(tǒng)模型，但目前的研究工作顯示^[6~8]：IPN受所采用的簡單Petri限制，難以描述類似網(wǎng)絡(luò)協(xié)議這樣的復(fù)雜系統(tǒng)。因此，本文提出將目前在協(xié)議行為分析中使用較多的CPN與之結(jié)合，構(gòu)建出一類新的、本文命名為CIPN的Petri網(wǎng)派生種類，在能夠較好地模擬復(fù)雜協(xié)議行為的同時還具備了較好的DES性質(zhì)。

本文結(jié)合CPN和IPN給出CIPN的形式化定義，以此對CIPN的基本特性如運(yùn)行和可觀測性作出分析。通過一個MACA協(xié)議，展示如何從一個CPN構(gòu)建等價的CIPN模型，并使用CIPN來分析MACA協(xié)議。

1CIPN的形式化定義

定義1一個CIPN由一個六元組CIPN=（CN，Σ，λ，O，δ，φ）構(gòu)成。其中：

CN=(p，T;F，C，I-，I+)，為一個基本著色Petri網(wǎng)，但是去除了初始標(biāo)記M0，CN是協(xié)議活動的核心網(wǎng)。

Σ={ε1，ε2，ε3，…，εr}，表示為DES系統(tǒng)信號輸入表，εi∈Σ為輸入信號，在協(xié)議活動中，該信號表示數(shù)據(jù)包到、超時觸發(fā)等信號。

λ:T→Σ∪{ε′} ，一個變遷命名關(guān)系，該關(guān)系需滿足以下約束條件：ti，tj∈T，i≠j，p∈P，如果I-(p，ti)=I-(p，tj)≠C(0)MS同時λ(ti)，λ(tj)≠ε′則λ(ti)≠λ(tj)。ε′為系統(tǒng)內(nèi)部事件，在DES中為非觀測事件。具體到協(xié)議活動中，λ關(guān)系將數(shù)據(jù)包與時間等事件與該事件的處理流程相綁定，其約束條件是表達(dá)了事件處理的惟一性。

O=(o1，o2，o3，…，os)，信號輸出表，可描述協(xié)議活動中數(shù)據(jù)包發(fā)送、啟動超時機(jī)制等信號。

δ:T→O∪{o′}，信號輸出的變遷命名關(guān)系，不要求信號輸出的惟一性，o′為1信號，該信號將不被DES觀測。

φ：R(CN，M0)→{Z+}q:系統(tǒng)輸出函數(shù)，本文使用單色托肯作為系統(tǒng)事件表述，此處R(CN，M0)是著色Petri網(wǎng)從初始標(biāo)記M0開始的可達(dá)集，q為可觀測信號的數(shù)目。

針對協(xié)議行為分析，系統(tǒng)輸出函數(shù)φ有兩種定義方式，表達(dá)了對網(wǎng)絡(luò)協(xié)議分析的兩種模式：

φ′:R(CN，M0)→{O∪Σ}q，q=|O∪Σ|，白盒模式，對協(xié)議中所有的信號進(jìn)行觀察。

φ″:R(CN，M0)→{O∩Σ}q，q=|O∩Σ|，黑盒模式，與白盒模式的區(qū)別在于縮小了觀測信號集。O∩Σ是協(xié)議數(shù)據(jù)包，因此黑盒模式是以一種類似Sniffer竊聽的方式來進(jìn)行網(wǎng)絡(luò)協(xié)議分析的。

本文假設(shè)φ是一個線性關(guān)系，則φ能以q×n矩陣形式表示：φ=[φij]，n=|P|。第i行分量φi表示與第i個信號相關(guān)的庫所單色托肯數(shù)量，φij=1…M(pj)≥10…M(pj)≥0。

2CIPN的形式化分析

21CIPN的運(yùn)行機(jī)制

CIPN中的CN如果滿足Mk(pi)[＞tj，即pj∈·tj→Mk(pi)≥I-(pi，tj)。如果λ(tj)=εn≠ε′，則變遷tj將確定發(fā)生；如果λ(tj)=ε′，則變遷tj以概率性發(fā)生，帶有一定的不確定性，這將由CN的具體實例決定，此時系統(tǒng)的輸出信號為yk=φ·Mk。當(dāng)變遷tj發(fā)生時，后續(xù)標(biāo)記及其輸出信號為

Mk+1=Mk+AT·tj

yk+1=φ·Mk+1

其中：AT是一個n×m×|R(C)MS|的立方陣，為CN的關(guān)聯(lián)矩陣

ATtj=[AT*1tj，AT*2tj，…，AT*mtj]T=

[ni=1Ai1tj(i)，ni=1Ai2tj(i)，…，ni=1Aimtj(i)]T

22CIPN的事件可觀測性分析

定義2CIPN中，一個變遷t在白盒模式下是可觀測的，當(dāng)且僅當(dāng)λ(t)≠ε′∨δ(t)≠o′；若變遷t在黑盒模式下可觀測，當(dāng)且僅當(dāng)λ(t)≠ε′∧δ(t)≠o′。

定義關(guān)系Γ:T→Boolean來表示T的可觀測性。如果Γ(t)=true，則t可觀測；否則，t不可觀測。

進(jìn)一步，定義變遷觸發(fā)語言。

定義3給定一個CIPN，定義s(CIPN)={σ|σ=titj…tk…，M0[ti＞M1[tj…Mn[tk…}，為CIPN的變遷觸發(fā)語言。

基于變遷T集的可觀測性，語言s被分解為可觀測部分與不可觀測部分：σ∈s， σ=t可通過系統(tǒng)的輸出信號進(jìn)行區(qū)分，則說明該CIPN具有事件可觀測性。

通過此定義，容易得到如下性質(zhì)及相關(guān)定理。

性質(zhì)1具有事件可觀測性的CIPN不存在不可觀測變遷。

定理1給定一個CIPN，該P(yáng)etri網(wǎng)具有n個變遷，m個單色觀測信號，如果該CIPN具有事件可觀測性，則變遷與觀測信號之間須滿足不等式n≤3m-1。

證明t∈T觸發(fā)時，對單色信號θ∈(ORΣ)（R::∪|∩）的可能影響有三種，即產(chǎn)生一個θ、消耗一個θ或者對θ沒有影響，記為(1，-1，0)，因此m個觀測信號可以表述3m個不同的信號序列，但一個全0的序列意味著一個不可見或者多個不可觀測的變遷發(fā)生。要觀測n個不同的變遷，觀測信號的數(shù)量m必須滿足3m-1≥n。

定理2一個CIPN=(CN，Σ，λ，O，δ，φ)是事件可觀測的，當(dāng)且僅當(dāng)φ·AT產(chǎn)生的列分量矩陣Φm=φ·AT*m(m={1，2，…，|T|)為非零矩陣且兩兩各異。

證明(充分性)若CIPN事件可觀測，則必不存在一個不可觀測變遷，因為不可觀測變遷對觀測信號沒有影響，輸出信號必然保持與前一變遷一致，或為零矩陣。對任意兩個可觀測變遷ti、tj而言，不失一般性，設(shè)Mk[ti＞Mi[tj＞Mj，其輸出信號為

如果φ·Φm=φ·Φj={0}，則變遷tj、tm為不可觀測變遷，這表明CIPN不具備事件可觀測性。

這表明由tj、tm變遷引發(fā)的輸出信號無法區(qū)分，該CIPN不具有事件可觀測性。

3MACA協(xié)議的CIPN構(gòu)建與分析

MACA協(xié)議是繼CSMA/CA協(xié)議后提出的一個較為完善的自組網(wǎng)接入控制協(xié)議。該協(xié)議提出的基于RTS/CTS控制信號能較好地避免所謂的隱藏終端和暴露終端的問題，該握手機(jī)制隨后得到了廣泛的應(yīng)用。本文以MACA協(xié)議為樣本來示例CIPN的分析方法。

31MACA的CPN模型

MACA的CPN模型假設(shè)如下：

a）兩節(jié)點參與，使用MACA協(xié)議進(jìn)行數(shù)據(jù)收發(fā)；

b）無線網(wǎng)絡(luò)是可靠的，不引入丟包概率；

c）節(jié)點RF元件可靠，不引入調(diào)制誤差；

d）模型中忽略數(shù)據(jù)包格式和內(nèi)容；

e)模型中忽略具體MAC地址。

模型如圖1所示;庫所定義和意義如表1所示。模型顏色集定義如下所示:

變遷意義比較明確，在此不再贅述。發(fā)送節(jié)點與接收節(jié)點通過wireless network 庫所的融合（如圖1的“Fusion1”融合標(biāo)記）實現(xiàn)模型的連接。此處，使用基于一種復(fù)合色的庫所p融合和對t∈·p輸出的弧上描述（inscription）加以限定，以及t∈p·加以守衛(wèi)（guard）條件，能夠很好地模擬網(wǎng)絡(luò)，特別是廣播式網(wǎng)絡(luò)。該方法筆者也在文獻(xiàn)[9]中使用過，得到了很好的效果。通過對該CPN模型在CPNTOOLS^[10]中加以軟件仿真運(yùn)行，所得到的可達(dá)圖如圖2所示，各方塊為MACA的系統(tǒng)狀態(tài)，弧表示各狀態(tài)間的轉(zhuǎn)換路徑。狀態(tài)1是系統(tǒng)初態(tài)M0，其余各態(tài)均滿足M0]＞。例如，圖2中狀態(tài)6為系統(tǒng)狀態(tài)M5，狀態(tài)分量如圖3所示。不難看出該標(biāo)記表述了發(fā)送節(jié)點正在發(fā)送用戶數(shù)據(jù)（TRANSMIT），而接收節(jié)點正在準(zhǔn)備接收數(shù)據(jù)（WFDATA）這一系統(tǒng)狀態(tài)。

通過對狀態(tài)圖的遍歷，MACA協(xié)議的死鎖、變遷活性與家態(tài)庫所等重要性質(zhì)容易得到驗證，本文在此不作過多描述。

盡管CPN模型已經(jīng)足以用來分析MACA協(xié)議，但是該模型尚與通常意義的DES系統(tǒng)有一定距離，難以映射到基于DES的常用協(xié)議仿真工具，如NS2、OPNET等。因此需要對該模型擴(kuò)展為CIPN。

32MACA的CIPN模型

同原始的CPN模型相比，CIPN模型（圖4）增添了幾個單色庫所，刪除了復(fù)合色的wireless network庫所，但兩個Petri網(wǎng)等價，筆者將在稍后給出證明。作為一個CIPN網(wǎng)絡(luò)，需要定義系統(tǒng)的輸入與輸出信號/事件，及其變遷與信號之間的命名關(guān)系。首先完成發(fā)送節(jié)點的

則協(xié)議MACA的系統(tǒng)觀測信號在本例中無論采用白盒還是黑盒模式，都有

下面證明該CIPN與MACA的CPN模型的等價性：

證明若兩個Petri網(wǎng)等價，則其可達(dá)圖是同構(gòu)的，并且Mi∈R(P1，M0)，MiMi′，Mi′∈R(P2，M′0)，Mi、Mi′對系統(tǒng)的描述是一致的?，F(xiàn)在MACA的CPN可達(dá)圖（圖2）已知，只需對MACA的CIPN計算其可達(dá)圖。通過CPNTOOL的狀態(tài)分析器，得到MACA的CIPN可達(dá)圖如圖5所示。

顯而易見，CIPN的可達(dá)圖與CPN的可達(dá)圖同構(gòu)。同時，可對可達(dá)圖中每個對應(yīng)的標(biāo)記進(jìn)行對比說明。以標(biāo)記6為例：CPN和CIPN皆在發(fā)送節(jié)點的TRANSIMIT庫所持有1′node(1)托肯，在接收節(jié)點的WFDATA庫所中持有1′node(2)托肯，這表明CIPN和CPN中描述的MACA協(xié)議狀態(tài)一致。同理，逐個比較標(biāo)記1～9可以發(fā)現(xiàn)，CIPN和CPN模型描述的MACA狀態(tài)具有一致性，因此兩個Petri網(wǎng)等價。

33MACA協(xié)議的變遷可觀測性分析

首先，注意到變遷tReady對任何系統(tǒng)輸出信號不產(chǎn)生影響，因此，在不引入新的系統(tǒng)信號下（如加上定時器信號，但必須在白盒模式下觀測），觸發(fā)tReady不能從系統(tǒng)輸出信號中觀測出，MACA的CIPN此時不能基于T集觀測。但可以經(jīng)過對發(fā)送節(jié)點的CIPN進(jìn)行網(wǎng)歸約(圖6)，從而實現(xiàn)T集可觀測性。

對于tReady，由于C(·tReady)=C（t·Ready），同時tReady保持了局部的S不變量特性，歸約后不會改變原CPN語意。

命題：歸約tReady后的MACA的CIPN具有T集的可觀測性。

證明目前使用三個單色信號{RTS|CTS|USERDATA}對六個變遷進(jìn)行監(jiān)控，顯然滿足T集觀測性的不等式3m-1≥n。

顯然，各分量非零且兩兩互異，故該CIPN為T集可觀測。同理可證接收節(jié)點的CIPN的T集可觀測性。

4結(jié)束語

協(xié)議工程的質(zhì)量在很大程度上取決于在工程過程中抽象模型的一致性，這樣才能保障協(xié)議工程各環(huán)節(jié)，特別在協(xié)議分析、驗證、仿真環(huán)節(jié)的分析對象具有連貫性和一致性。在目前協(xié)議仿真工具都基于DES驅(qū)動的情況下，建立一個基于DES的協(xié)議形式化模型是保持模型一致性最為有效的方法。本文將CPN和IPN結(jié)合，提出了一種適合用于網(wǎng)絡(luò)協(xié)議行為分析的CIPN，并對CIPN運(yùn)行機(jī)制和觀測性作了相應(yīng)的分析。一個基于MACA協(xié)議的示例展示了如何從一個CPN模型構(gòu)造一個與之等價的CIPN模型，并使用CIPN的事件可觀測性定理對該模型進(jìn)行了事件可觀測性分析。具有事件可觀測性的Petri網(wǎng)模型能夠較為容易地轉(zhuǎn)換為通用協(xié)議仿真工具中的對應(yīng)模型，如OPNET的Process模型，在保持模型一致的基礎(chǔ)上可以實現(xiàn)對協(xié)議行為和性能的同步分析。

參考文獻(xiàn)：

［1］

HOLZMANN G J.Protocol design: redefining the state of the art[J].IEEE Software，1992，9(1):17-22.

［2］GUNWAN E，TAN T P，SHI N.Survey of formal description techniques (FDTs) for protocol converter design[C]//Proc ofIEEE Region 10 Conference on Computer， Communication， Control and Power Engineering.[S.l.]:IEEE，1993:422-425.

［3］BERTHELOT G，TERRAT R.Petri nets theory for the correctness of protocols[J].IEEE Trans on Communications，1982，30(12):2497-2505.

［4］JENSEN K.Colored Petri nets:basic concepts，analysis methods and practical use[M].[S.l.]:Springer-Verlag，1992.

［5］MEDA M E，RAMIRES A，MALO A.Identification in discrete event systems[C]//Proc of IEEE International Conference on Systems， Man， and Cybernetics.1998:740-745.

［6］ALCARAZ-MEJIA M，LOPEZ-MELLADO E，RAMIREZ-TREVINO A，et al.Petri net based fault diagnosis of discrete event systems[C]//Proc ofIEEE International Conference on Systems， Man and Cybernetics.[S.l.]:IEEE，2003:4730-4735.

［7］CAMPOS-RODRIGUEZ R，RAMIREZ-TREVINO A，LOPEZ-MELLADO E.Observability analysis of free-choice Petri net models[C]//Proc of IEEE/SMC International Conference on System of Systems Engineering.[S.l.]:IEEE，2006:77-82.

［8］BASILE F，CHIACCHIO P.On the implementation of supervised control of discrete event systems[J].IEEE Trans on Control Systems Technology，2007，15(4):725-739.

［9］PENG Lei，WU Lei，YE Ya-lan，et al.CPN modeling and analysis of HMIPv6[C]//Proc of IEEE International Conference on Integration Technology.[S.l.]:IEEE，2007:63-68.

［10］CPN Group， University of Aarhus. CPNTools community online[EB/OL].(2007-10-08).http://www.daimi.au.dk/CPNTools/.