一種基于ＣＩＰＮ的網絡協議建模方法
2008-12-31 00:00:00彭磊畢亞雷曾家智
計算機應用研究 2008年11期
(1.電子科技大學 計算機科學與工程學院，成都 610054；2.中國科學院 深圳先進技術研究院， 廣東 深圳 518067)
摘要：基于Petri網的網絡協議建模技術需要更有效地與現有通用網絡協議仿真技術協同工作，結合CPN和IPN，提出了一種新的Petri網派生類CIPN用于網絡協議的建模和形式化分析，突出了協議的離散事件系統特性。給出了CIPN的定義，并討論了CIPN的運行機制，證明了CIPN事件可觀測性的充要條件。通過一個MACA協議作為示例，完成了從網絡協議的一般CPN模型到CIPN模型的等價性轉換，并利用CIPN的事件可觀測性定理對MACA協議進行了事件觀測性分析。
關鍵詞：網絡協議；離散事件系統；著色解釋Petri網；協議工程
中圖分類號：TP393文獻標志碼：A
文章編號：1001-3695(2008)11-3430-04
Novel CIPN-based modeling for network protocols
PENG Lei1，2，BI Ya-lei2，ZENG Jia-zhi1
（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引言
通信協議是一類特殊的軟件，工作于系統內核，空間分布性、并發性、異步性是協議運轉時的主要特點。同時，通信協議為用戶透明了網絡，使之成為一個可靠的比特管道。因此通信協議的完整性、正確性、安全性是衡量一個通信協議設計質量的關鍵指標，一旦協議部署，糾正錯誤的代價就非常昂貴，同時也會造成用戶對網絡系統的極大失望。 要保證協議設計優良，必須引入規范化的方法來引導協議設計，這就是所謂的協議工程（protocol engineering， PE）[1]。
在繼承了軟件工程的一些共有理念和基本流程后，協議工程引入了形式化描述技術（formal description technique，FDT）[2]，貫穿于協議開發的各階段，起始于協議規范描述，以保證在協議設計過程中，可對協議進行形式化分析和求解，從而使協議的研究開發可以獨立于非形式的自然語言文本和最終實現代碼，避免了協議驗證測試的復雜性。
形式化的協議行為分析是協議工程中非常重要的環節。一種主要的思路是基于Petri網理論對協議展開研究[3]，主要從協議行為和協議性能這兩個方面來進行分析。協議性能分析主要對協議的網絡開銷、信道利用率、吞吐率等指標使用時延Petri和隨機Petri進行建模分析；協議行為分析主要針對協議的設計與實現，包括對協議的容錯和魯棒性的研究，現多使用高級Petri網如著色Petri網[4]、層次Petri網進行建模。
目前的現狀是協議工程的研究進展并不理想，遠遠落后于軟件工程。除了協議自身的特殊性，
協議工程中缺乏貫穿工程全階段的一致模型是一大因素，這使得各階段的工作難以環環相扣，基于Petri網的形式化分析的結論或成果難以直接指導協議的仿真與研發行為。
現在主流的協議仿真工具如NS2、OPNET的通用仿真，或如TOSSIM這種只針對于TinyOS上的WSN協議仿真，無不使用DES作為協議模型的驅動機制。因此，考慮基于DES機制構建形式化的協議行為分析網是解決上文中提出的保持模型一致性的有效方法。
IPN[5]是近年來Petri網的又一變種，比較適合用來構建DES系統模型，但目前的研究工作顯示[6~8]：IPN受所采用的簡單Petri限制，難以描述類似網絡協議這樣的復雜系統。因此，本文提出將目前在協議行為分析中使用較多的CPN與之結合，構建出一類新的、本文命名為CIPN的Petri網派生種類，在能夠較好地模擬復雜協議行為的同時還具備了較好的DES性質。
本文結合CPN和IPN給出CIPN的形式化定義，以此對CIPN的基本特性如運行和可觀測性作出分析。通過一個MACA協議，展示如何從一個CPN構建等價的CIPN模型，并使用CIPN來分析MACA協議。
1CIPN的形式化定義
定義1一個CIPN由一個六元組CIPN=（CN，Σ，λ，O，δ，φ）構成。其中：
CN=(p，T;F，C，I-，I+)，為一個基本著色Petri網，但是去除了初始標記M0，CN是協議活動的核心網。
Σ={ε1，ε2，ε3，…，εr}，表示為DES系統信號輸入表，εi∈Σ為輸入信號，在協議活動中，該信號表示數據包到、超時觸發等信號。
λ:T→Σ∪{ε′} ，一個變遷命名關系，該關系需滿足以下約束條件：ti，tj∈T，i≠j，p∈P，如果I-(p，ti)=I-(p，tj)≠C(0)MS同時λ(ti)，λ(tj)≠ε′則λ(ti)≠λ(tj)。ε′為系統內部事件，在DES中為非觀測事件。具體到協議活動中，λ關系將數據包與時間等事件與該事件的處理流程相綁定，其約束條件是表達了事件處理的惟一性。
O=(o1，o2，o3，…，os)，信號輸出表，可描述協議活動中數據包發送、啟動超時機制等信號。
δ:T→O∪{o′}，信號輸出的變遷命名關系，不要求信號輸出的惟一性，o′為1信號，該信號將不被DES觀測。
φ：R(CN，M0)→{Z+}q:系統輸出函數，本文使用單色托肯作為系統事件表述，此處R(CN，M0)是著色Petri網從初始標記M0開始的可達集，q為可觀測信號的數目。
針對協議行為分析，系統輸出函數φ有兩種定義方式，表達了對網絡協議分析的兩種模式：
φ′:R(CN，M0)→{O∪Σ}q，q=|O∪Σ|，白盒模式，對協議中所有的信號進行觀察。
φ″:R(CN，M0)→{O∩Σ}q，q=|O∩Σ|，黑盒模式，與白盒模式的區別在于縮小了觀測信號集。O∩Σ是協議數據包，因此黑盒模式是以一種類似Sniffer竊聽的方式來進行網絡協議分析的。
本文假設φ是一個線性關系，則φ能以q×n矩陣形式表示：φ=[φij]，n=|P|。第i行分量φi表示與第i個信號相關的庫所單色托肯數量，φij=1…M(pj)≥10…M(pj)≥0。
2CIPN的形式化分析
21CIPN的運行機制
CIPN中的CN如果滿足Mk(pi)[＞tj，即pj∈·tj→Mk(pi)≥I-(pi，tj)。如果λ(tj)=εn≠ε′，則變遷tj將確定發生；如果λ(tj)=ε′，則變遷tj以概率性發生，帶有一定的不確定性，這將由CN的具體實例決定，此時系統的輸出信號為yk=φ·Mk。當變遷tj發生時，后續標記及其輸出信號為
Mk+1=Mk+AT·tj
yk+1=φ·Mk+1
其中：AT是一個n×m×|R(C)MS|的立方陣，為CN的關聯矩陣
ATtj=[AT*1tj，AT*2tj，…，AT*mtj]T=
[ni=1Ai1tj(i)，ni=1Ai2tj(i)，…，ni=1Aimtj(i)]T
22CIPN的事件可觀測性分析
定義2CIPN中，一個變遷t在白盒模式下是可觀測的，當且僅當λ(t)≠ε′∨δ(t)≠o′；若變遷t在黑盒模式下可觀測，當且僅當λ(t)≠ε′∧δ(t)≠o′。
定義關系Γ:T→Boolean來表示T的可觀測性。如果Γ(t)=true，則t可觀測；否則，t不可觀測。
進一步，定義變遷觸發語言。
定義3給定一個CIPN，定義s(CIPN)={σ|σ=titj…tk…，M0[ti＞M1[tj…Mn[tk…}，為CIPN的變遷觸發語言。
基于變遷T集的可觀測性，語言s被分解為可觀測部分與不可觀測部分：σ∈s， σ=t可通過系統的輸出信號進行區分，則說明該CIPN具有事件可觀測性。
通過此定義，容易得到如下性質及相關定理。
性質1具有事件可觀測性的CIPN不存在不可觀測變遷。
定理1給定一個CIPN，該Petri網具有n個變遷，m個單色觀測信號，如果該CIPN具有事件可觀測性，則變遷與觀測信號之間須滿足不等式n≤3m-1。
證明t∈T觸發時，對單色信號θ∈(ORΣ)（R::∪|∩）的可能影響有三種，即產生一個θ、消耗一個θ或者對θ沒有影響，記為(1，-1，0)，因此m個觀測信號可以表述3m個不同的信號序列，但一個全0的序列意味著一個不可見或者多個不可觀測的變遷發生。要觀測n個不同的變遷，觀測信號的數量m必須滿足3m-1≥n。
定理2一個CIPN=(CN，Σ，λ，O，δ，φ)是事件可觀測的，當且僅當φ·AT產生的列分量矩陣Φm=φ·AT*m(m={1，2，…，|T|)為非零矩陣且兩兩各異。
證明(充分性)若CIPN事件可觀測，則必不存在一個不可觀測變遷，因為不可觀測變遷對觀測信號沒有影響，輸出信號必然保持與前一變遷一致，或為零矩陣。對任意兩個可觀測變遷ti、tj而言，不失一般性，設Mk[ti＞Mi[tj＞Mj，其輸出信號為
如果φ·Φm=φ·Φj={0}，則變遷tj、tm為不可觀測變遷，這表明CIPN不具備事件可觀測性。
這表明由tj、tm變遷引發的輸出信號無法區分，該CIPN不具有事件可觀測性。
3MACA協議的CIPN構建與分析
MACA協議是繼CSMA/CA協議后提出的一個較為完善的自組網接入控制協議。該協議提出的基于RTS/CTS控制信號能較好地避免所謂的隱藏終端和暴露終端的問題，該握手機制隨后得到了廣泛的應用。本文以MACA協議為樣本來示例CIPN的分析方法。
31MACA的CPN模型
MACA的CPN模型假設如下：
a）兩節點參與，使用MACA協議進行數據收發；
b）無線網絡是可靠的，不引入丟包概率；
c）節點RF元件可靠，不引入調制誤差；
d）模型中忽略數據包格式和內容；
e)模型中忽略具體MAC地址。
模型如圖1所示;庫所定義和意義如表1所示。模型顏色集定義如下所示:
變遷意義比較明確，在此不再贅述。發送節點與接收節點通過wireless network 庫所的融合（如圖1的“Fusion1”融合標記）實現模型的連接。此處，使用基于一種復合色的庫所p融合和對t∈·p輸出的弧上描述（inscription）加以限定，以及t∈p·加以守衛（guard）條件，能夠很好地模擬網絡，特別是廣播式網絡。該方法筆者也在文獻[9]中使用過，得到了很好的效果。通過對該CPN模型在CPNTOOLS[10]中加以軟件仿真運行，所得到的可達圖如圖2所示，各方塊為MACA的系統狀態，弧表示各狀態間的轉換路徑。狀態1是系統初態M0，其余各態均滿足M0]＞。例如，圖2中狀態6為系統狀態M5，狀態分量如圖3所示。不難看出該標記表述了發送節點正在發送用戶數據（TRANSMIT），而接收節點正在準備接收數據（WFDATA）這一系統狀態。
通過對狀態圖的遍歷，MACA協議的死鎖、變遷活性與家態庫所等重要性質容易得到驗證，本文在此不作過多描述。
盡管CPN模型已經足以用來分析MACA協議，但是該模型尚與通常意義的DES系統有一定距離，難以映射到基于DES的常用協議仿真工具，如NS2、OPNET等。因此需要對該模型擴展為CIPN。
32MACA的CIPN模型
同原始的CPN模型相比，CIPN模型（圖4）增添了幾個單色庫所，刪除了復合色的wireless network庫所，但兩個Petri網等價，筆者將在稍后給出證明。作為一個CIPN網絡，需要定義系統的輸入與輸出信號/事件，及其變遷與信號之間的命名關系。首先完成發送節點的
則協議MACA的系統觀測信號在本例中無論采用白盒還是黑盒模式，都有
下面證明該CIPN與MACA的CPN模型的等價性：
證明若兩個Petri網等價，則其可達圖是同構的，并且Mi∈R(P1，M0)，MiMi′，Mi′∈R(P2，M′0)，Mi、Mi′對系統的描述是一致的。現在MACA的CPN可達圖（圖2）已知，只需對MACA的CIPN計算其可達圖。通過CPNTOOL的狀態分析器，得到MACA的CIPN可達圖如圖5所示。
顯而易見，CIPN的可達圖與CPN的可達圖同構。同時，可對可達圖中每個對應的標記進行對比說明。以標記6為例：CPN和CIPN皆在發送節點的TRANSIMIT庫所持有1′node(1)托肯，在接收節點的WFDATA庫所中持有1′node(2)托肯，這表明CIPN和CPN中描述的MACA協議狀態一致。同理，逐個比較標記1～9可以發現，CIPN和CPN模型描述的MACA狀態具有一致性，因此兩個Petri網等價。
33MACA協議的變遷可觀測性分析
首先，注意到變遷tReady對任何系統輸出信號不產生影響，因此，在不引入新的系統信號下（如加上定時器信號，但必須在白盒模式下觀測），觸發tReady不能從系統輸出信號中觀測出，MACA的CIPN此時不能基于T集觀測。但可以經過對發送節點的CIPN進行網歸約(圖6)，從而實現T集可觀測性。
對于tReady，由于C(·tReady)=C（t·Ready），同時tReady保持了局部的S不變量特性，歸約后不會改變原CPN語意。
命題：歸約tReady后的MACA的CIPN具有T集的可觀測性。
證明目前使用三個單色信號{RTS|CTS|USERDATA}對六個變遷進行監控，顯然滿足T集觀測性的不等式3m-1≥n。
顯然，各分量非零且兩兩互異，故該CIPN為T集可觀測。同理可證接收節點的CIPN的T集可觀測性。
4結束語
協議工程的質量在很大程度上取決于在工程過程中抽象模型的一致性，這樣才能保障協議工程各環節，特別在協議分析、驗證、仿真環節的分析對象具有連貫性和一致性。在目前協議仿真工具都基于DES驅動的情況下，建立一個基于DES的協議形式化模型是保持模型一致性最為有效的方法。本文將CPN和IPN結合，提出了一種適合用于網絡協議行為分析的CIPN，并對CIPN運行機制和觀測性作了相應的分析。一個基于MACA協議的示例展示了如何從一個CPN模型構造一個與之等價的CIPN模型，并使用CIPN的事件可觀測性定理對該模型進行了事件可觀測性分析。具有事件可觀測性的Petri網模型能夠較為容易地轉換為通用協議仿真工具中的對應模型，如OPNET的Process模型，在保持模型一致的基礎上可以實現對協議行為和性能的同步分析。
參考文獻：
［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/.
