王潔寧，姜高揚(yáng)

（中國民航大學(xué)空中交通管理研究基地，天津 300300）

長期以來，航行情報(bào)數(shù)據(jù)還是以紙質(zhì)航圖、AIP手冊、NOTAM電報(bào)的形式通過郵局和AFTN網(wǎng)進(jìn)行傳遞，各個(gè)航行情報(bào)系統(tǒng)彼此孤立而不能互相調(diào)用，所提供的航行情報(bào)服務(wù)在時(shí)效性和信息量方面逐漸不能滿足實(shí)際需求。為此國際民航組織提出要將傳統(tǒng)的航行情報(bào)服務(wù)（AIS）逐步過渡到航行情報(bào)管理（AIM）。AIM就是在全球范圍內(nèi)以交互方式提供滿足當(dāng)前及未來ATM系統(tǒng)和所有飛行階段需要的航空數(shù)據(jù)。它明確了航空信息的提供將以數(shù)據(jù)為中心而不是以產(chǎn)品為中心，其最終目標(biāo)是逐漸向SWIM——全系統(tǒng)信息管理過渡。

飛行程序作為航行情報(bào)的主要內(nèi)容之一，其發(fā)布也將由現(xiàn)在的紙質(zhì)產(chǎn)品、郵局傳送的方式轉(zhuǎn)變?yōu)閿?shù)字信息、網(wǎng)絡(luò)傳輸?shù)姆绞?，機(jī)場、空管和航空公司的航行情報(bào)室獲取情報(bào)的方式也將由被動等待郵局傳送轉(zhuǎn)變?yōu)橹鲃佑嗛喐信d趣的信息，因此建立合理的通信服務(wù)將是本次過渡所面臨的主要問題之一。

發(fā)布訂閱通信范型作為一種異步通信機(jī)制，在時(shí)間和空間上具有完全的解耦性，近年來得到了工業(yè)界和學(xué)術(shù)界的普遍關(guān)注，已經(jīng)成為研究的熱點(diǎn)。范洪亮[1]、張煜[2]等人研究了發(fā)布訂閱系統(tǒng)中的路由算法和匹配技術(shù)，但是如何將發(fā)布訂閱服務(wù)應(yīng)用在飛行程序數(shù)據(jù)共享方面尚未有人研究，因此本文在前人研究的基礎(chǔ)上，利用UML建立飛行程序發(fā)布訂閱服務(wù)概念模型，之后給出相應(yīng)的Petri網(wǎng)模型，利用可達(dá)樹和P不變量方法分析和驗(yàn)證模型的有效性，為搭建飛行程序發(fā)布訂閱服務(wù)系統(tǒng)奠定理論基礎(chǔ)。

1 發(fā)布訂閱服務(wù)概念模型

飛行程序發(fā)布訂閱服務(wù)可以抽象為一個(gè)六元組{P，S，B，P_operation，S_operation，B_operation}，其中P表示飛行程序的發(fā)布者，即中國民航局航行情報(bào)服務(wù)中心；S={S1，S2，…，Sn}表示飛行程序的訂閱者，即機(jī)場、航空公司和空管的航行情報(bào)室；B={B1，B2，…，Bk}表示k個(gè)中間代理；P_operation定義了航行情報(bào)服務(wù)中心具有的操作，如向外發(fā)布航行情報(bào)publish（）；S_operation定義了機(jī)場、航空公司和空管的航行情報(bào)室具有的操作，典型的有訂閱subscribe（）和取消訂閱unsubscribe（）；B_operation定義了中間代理具有的操作，比如匹配用戶訂閱條件操作match（）和通知操作notify（）。

飛行程序發(fā)布訂閱服務(wù)概念模型可用UML中的用例圖和順序圖描述，用例圖體現(xiàn)了系統(tǒng)的行為，即系統(tǒng)提供的外部可見的服務(wù)，可為系統(tǒng)的上下文及系統(tǒng)的需求建模；順序圖強(qiáng)調(diào)了消息的時(shí)間順序，可為發(fā)布和訂閱的具體過程建模[3]。

1.1 發(fā)布訂閱服務(wù)用例圖

飛行程序發(fā)布訂閱服務(wù)的用例圖如圖1所示，用戶發(fā)布或者訂閱信息之前必須登錄系統(tǒng)，通過身份驗(yàn)證以后方可進(jìn)行相應(yīng)的操作，這樣就保證了系統(tǒng)的安全性。登錄系統(tǒng)之后機(jī)場航行情報(bào)室向中間代理提交自己的訂閱條件，說明需要哪種飛行程序；航行情報(bào)服務(wù)中心連續(xù)地向中間代理發(fā)布最新的飛行程序數(shù)據(jù)；中間代理將所有發(fā)布的飛行程序數(shù)據(jù)與訂閱者的訂閱條件相匹配，篩選出符合用戶需求的數(shù)據(jù)通知給用戶。當(dāng)訂閱者對某些數(shù)據(jù)不再感興趣時(shí)可以取消之前的訂閱。

1.2 訂閱服務(wù)順序圖

訂閱服務(wù)順序圖描述了機(jī)場、航空公司和空管的航行情報(bào)室訂閱飛行程序的流程，如圖2所示。航行情報(bào)室首先調(diào)用entry（）函數(shù)登錄系統(tǒng)，之后系統(tǒng)通過validate（）函數(shù)驗(yàn)證用戶身份，如果是授權(quán)用戶則可以執(zhí)行subscribe（）操作。代理收到信息以后將信息解析為內(nèi)部數(shù)據(jù)結(jié)構(gòu)，根據(jù)用戶的訂閱和取消訂閱的條件，過濾出用戶想要取消的信息，更新用戶訂閱列表，最后調(diào)用add（）函數(shù)將最新的訂閱列表加入到匹配模塊中去。

1.3 發(fā)布服務(wù)順序圖

與訂閱服務(wù)相同，發(fā)布服務(wù)順序圖描述了發(fā)布服務(wù)消息傳遞的先后順序，如圖3所示。其中entry（）和validate（）函數(shù)與訂閱服務(wù)中的函數(shù)相同，parse（）函數(shù)是按照用戶的訂閱條件進(jìn)行發(fā)布內(nèi)容的解析，通過Match模塊將飛行程序數(shù)據(jù)從航行情報(bào)中剝離出來，生成訂閱用戶列表，之后中間代理依據(jù)用戶列表將不同的飛行程序數(shù)據(jù)通知給相應(yīng)的用戶。

2 發(fā)布訂閱服務(wù)Petri網(wǎng)建模

發(fā)布訂閱服務(wù)概念模型刻畫了系統(tǒng)需求和工作流程，但是模型的正確性和有效性尚不明確，因此需要采用合理的方法對概念模型的性質(zhì)進(jìn)行評估。Petri網(wǎng)是分布式系統(tǒng)的建模和分析工具，其特別適合于描述系統(tǒng)中進(jìn)程或部件的順序、并發(fā)、沖突以及同步等關(guān)系[4]，通過Petri網(wǎng)建模，可以對系統(tǒng)模型的性能和結(jié)構(gòu)進(jìn)行分析與評估，進(jìn)而可以反映出模型的正確性和有效性。

Petri網(wǎng)和P不變量的定義和性質(zhì)[5]：

定義1（Petri網(wǎng)）PN={P，T，I，O，m}，其中：

P={p1，…，pn}是庫所的有限集合，n>0 為庫所的個(gè)數(shù)；

T={t1，…，tm}是變遷的有限集合，m>0 為變遷的個(gè)數(shù)；

P∩T=?，且P∪T≠?，即庫所和變遷不相交且網(wǎng)中至少有一個(gè)元素；

I：P×T→N是輸入矩陣，其定義了從P到T的有向弧的權(quán)的集合，這里N={0，1，…}為非負(fù)整數(shù)集；

O：T×P→N是輸出矩陣，其定義了從T到P的有向弧的權(quán)的集合；

m：P→N是標(biāo)識，其為一列向量，其第i個(gè)元素表示第i個(gè)庫所里的Token數(shù)。

定義2（P不變量） 一個(gè)P不變量為一（n×1）非負(fù)整數(shù)向量x，并滿足xTC=0，其中C=O-I稱為關(guān)聯(lián)矩陣。

性質(zhì)1（P不變量） 若只要存在一個(gè)（n×1）正實(shí)數(shù)向量x，使得xTC≤0，則PN是結(jié)構(gòu)上有界的。

性質(zhì)2（P不變量） 若只要存在一個(gè)（n×1）正實(shí)數(shù)向量x，使得xTC=0，則PN是結(jié)構(gòu)上守衡的。

2.1 訂閱服務(wù)的Petri網(wǎng)模型

假設(shè)訂閱者有兩個(gè)訂閱條件和一個(gè)取消訂閱的條件，因此系統(tǒng)的初始條件為庫所p1中有2個(gè)托肯，代表用戶需要訂閱的兩條信息，p3中1個(gè)托肯，代表用戶取消某一條信息的請求，在變遷t3激發(fā)前，來自p3的取消訂閱條件和來自p4的訂閱條件一一比較，如果該信息是用戶指定要取消的，則放入庫所p5中，表示信息已經(jīng)取消，否則放入p6中，作為更新過的用戶訂閱列表，然后加入到匹配模塊p7中去。匹配模塊會接收發(fā)布者發(fā)來的各種信息，并與其中的用戶訂閱列表匹配。訂閱系統(tǒng)的Petri網(wǎng)模型如圖4所示。

庫所變遷的含義如表1所示。

表1 訂閱服務(wù)庫所變遷的含義Tab.1 Place and transition meaning of Sub-service

2.2 發(fā)布服務(wù)的Petri網(wǎng)模型

發(fā)布服務(wù)的Petri網(wǎng)模型如圖5所示，系統(tǒng)的初始條件為p1和p3中存在托肯，只有這樣變遷t2才能激發(fā)，其實(shí)際意義為只有當(dāng)系統(tǒng)中有發(fā)布信息且有用戶訂閱時(shí)，匹配模塊才開始工作。一旦發(fā)布的信息與用戶需求匹配成功，則生成訂閱用戶列表，中間代理根據(jù)訂閱用戶列表將信息通知給用戶。

庫所和變遷的含義如表2所示。

表2 發(fā)布服務(wù)庫所和變遷的含義Tab.2 Place and transition meaning of Pub-service

3 模型的分析和驗(yàn)證

Petri網(wǎng)的分析方法可分為基于可達(dá)樹與基于不變量兩種方法，前者為圖形分析方法，后者為數(shù)學(xué)分析方法。下面分別用可達(dá)樹和不變量分析方法對飛行程序發(fā)布訂閱服務(wù)Petri網(wǎng)模型進(jìn)行分析和驗(yàn)證。

3.1 訂閱服務(wù)Petri網(wǎng)模型的可達(dá)樹分析

從初始標(biāo)識m0開始，通過變遷將PN所有可能的標(biāo)識關(guān)聯(lián)起來，組成的樹狀結(jié)構(gòu)圖稱為可達(dá)樹。樹中的節(jié)點(diǎn)為標(biāo)識，節(jié)點(diǎn)之間用表示變遷的箭頭連接，箭頭起端所連接的標(biāo)識通過該箭頭所代表的變遷的激發(fā)，產(chǎn)生該箭頭末端所連接的標(biāo)識。

可達(dá)樹的構(gòu)造算法如下[6]：

步驟1：以初始標(biāo)識m0為樹根，并作上“new”的記號；

步驟2：若“new”標(biāo)識存在，則做以下事情，否則終止；

步驟3：選擇某一“new”標(biāo)識m；

1）若m與樹中間已有的其他標(biāo)識相同，則將其記為“old”，然后轉(zhuǎn)向其他“new”標(biāo)識；

2）若在m下無變遷使能，則將m記為“dead end”（死點(diǎn)）；

步驟4：對于m下使能的所有變遷t，做以下事情：

1）激發(fā) t，產(chǎn)生標(biāo)識 m′；

2）若在從樹根至m′的路徑上存在一標(biāo)識m″，使得m′＞m″，則對于那些m′（p）＞m″（p）成立的p，用w取代m′（p）；

3）以m′為一節(jié)點(diǎn)，從m至m′畫一有向線，將其記為 t，并將 m′記為“new”；

步驟5：除去m的“new”標(biāo)志，回到步驟2。

訂閱服務(wù)的可達(dá)樹如圖6所示。

圖6 訂閱服務(wù)Petri網(wǎng)模型的可達(dá)樹Fig.6 Reachability tree of Sub-service Petri net model

基于可達(dá)樹可作如下分析：

1）當(dāng)且僅當(dāng)樹中所有節(jié)點(diǎn)上均不出現(xiàn)w時(shí)，PN是有界的；

2）當(dāng)且僅當(dāng)樹中所有的節(jié)點(diǎn)上僅包含0或1時(shí)，PN是安全的；

3）若沒有任何死點(diǎn)包含w，則樹中死點(diǎn)的個(gè)數(shù)就是PN死標(biāo)識的數(shù)目；

4）若某變遷在樹中不出現(xiàn)，則該變遷是死變遷，死變遷從反面描述Petri網(wǎng)的活性。

根據(jù)上述分析，由圖6所示的可達(dá)樹可知，所建Petri網(wǎng)模型是有界的，除了 p1、p2、p4，其他庫所是安全的，PN死標(biāo)識的數(shù)目為1，即最后一個(gè)標(biāo)識為死標(biāo)識，對應(yīng)系統(tǒng)的結(jié)束狀態(tài)。由于所有變遷都在樹中出現(xiàn)，因此不包含死變遷。

3.2 訂閱服務(wù)Petri網(wǎng)模型的不變量分析

不變量分析方法是基于矩陣線性代數(shù)，其優(yōu)點(diǎn)是依據(jù)簡單的線性代數(shù)方程就能正確地確定Petri網(wǎng)的性能，進(jìn)而確定系統(tǒng)的結(jié)構(gòu)特性[4]。訂閱Petri網(wǎng)的不變量分析如下：

設(shè)輸入矩陣為I、輸出矩陣為O、關(guān)聯(lián)矩陣為C，則

求解xTC=0得

滿足該方程的一個(gè)解為

得到一個(gè) P 不變量（2 2 2 2 1 1 1）T。

據(jù)性質(zhì) 1 和性質(zhì) 2，存在 x=（2 2 2 2 1 1 1）T＞0，滿足xTC=0，因此該P(yáng)etri網(wǎng)模型是結(jié)構(gòu)上有界且守衡的。有界性說明系統(tǒng)中的托肯數(shù)沒有超過每個(gè)庫所的容量限制，在用程序?qū)崿F(xiàn)訂閱服務(wù)時(shí)計(jì)算機(jī)運(yùn)行的結(jié)果不會出現(xiàn)溢出；守衡性說明系統(tǒng)中包含的資源的數(shù)量是固定的，盡管系統(tǒng)的標(biāo)識在變化，但其所包含的托肯數(shù)維持不變，這遵循資源既不能產(chǎn)生又不能消失的法則，其實(shí)際意義在于一旦訂閱事件發(fā)生后，訂閱的信息不會無緣無故地產(chǎn)生和消失，因此可認(rèn)為系統(tǒng)的運(yùn)行是安全和穩(wěn)定的。

3.3 發(fā)布服務(wù)Petri網(wǎng)的可達(dá)樹分析

根據(jù)可達(dá)樹的構(gòu)造算法所構(gòu)造出的發(fā)布服務(wù)Petri網(wǎng)可達(dá)樹如圖7所示。

圖7 發(fā)布服務(wù)Petri網(wǎng)的可達(dá)樹Fig.7 Reachability tree of Pub-service Petri net model

由于所有節(jié)點(diǎn)上均不出現(xiàn)w，PN是有界的；樹中所有的節(jié)點(diǎn)上僅包含0或1時(shí)，PN是安全的；樹中最后一個(gè)標(biāo)識是死標(biāo)識，對應(yīng)系統(tǒng)的結(jié)束狀態(tài)；所有變遷都在樹中出現(xiàn)，因此不包含死變遷。

3.4 發(fā)布服務(wù)Petri網(wǎng)的不變量分析

輸入矩陣I、輸出矩陣O、關(guān)聯(lián)矩陣C分別為

求解xTC=0得

滿足該方程的一個(gè)解為

得到一個(gè)P 不變量（1 1 1 1 1）T。

根據(jù)性質(zhì)1和性質(zhì)2，存在一個(gè)P不變量x=（1 1 1 1 1）T＞0，滿足 xTC=0，因此該 Petri網(wǎng)模型是結(jié)構(gòu)上有界且守衡的，對應(yīng)的實(shí)際系統(tǒng)是安全和穩(wěn)定的。

4 結(jié)語

本文利用UML建立了飛行程序發(fā)布訂閱服務(wù)概念模型，根據(jù)概念模型中信息處理的流程設(shè)計(jì)了相應(yīng)的Petri網(wǎng)模型，通過可達(dá)樹分析和P不變量分析，得出所建的Petri網(wǎng)模型是結(jié)構(gòu)上有界且守衡的，不包含死變遷。由于Petri網(wǎng)模型是依據(jù)概念模型而建，因此可以證明本文所建立的概念模型是正確的、有效的，從而為飛行程序發(fā)布訂閱服務(wù)系統(tǒng)的構(gòu)建奠定了理論基礎(chǔ)。下一步的工作是引入賦時(shí)的概念，探討系統(tǒng)處理大量飛行程序發(fā)布訂閱信息時(shí)的工作效率問題，進(jìn)一步完善和優(yōu)化發(fā)布訂閱服務(wù)系統(tǒng)。

[1]苑洪亮.基于內(nèi)容的“發(fā)布/訂閱”若干關(guān)鍵技術(shù)研究[D].長沙：國防科技大學(xué)，2006.

[2]張 煜.發(fā)布/訂閱系統(tǒng)中信息訂閱匹配技術(shù)研究與實(shí)現(xiàn)[D].南京：南京理工大學(xué)，2009.

[3]冀振燕.UML系統(tǒng)分析與設(shè)計(jì)教程[M].北京：人民郵電出版社，2009：85-86.

[4]吳哲輝.Petri網(wǎng)導(dǎo)論[M].北京：機(jī)械工業(yè)出版社，2006：1-23.

[5]袁志娟.基于PSO的多跑道運(yùn)行優(yōu)化方法及仿真建模[D].天津：中國民航大學(xué)，2010.

[6]江志斌.Petri網(wǎng)及其在制造系統(tǒng)建模與控制中的應(yīng)用[M].北京：機(jī)械工業(yè)出版社，2004：50-55.