摘要：該文首先提出了基于Petri網(wǎng)的Web服務(wù)組合建模方法，對服務(wù)組合進(jìn)行形式化建模，然后采用可達(dá)樹作為分析工具，對服務(wù)組合模型的可達(dá)性，活性，有界性等特性進(jìn)行驗證分析。最后通過一個具體的實例說明此方法的應(yīng)用。

　　關(guān)鍵詞：Web服務(wù)；Petri網(wǎng)；可達(dá)樹；Web服務(wù)組合；驗證

　　中圖分類號：TP311 文獻(xiàn)標(biāo)識碼：A 文章編號：1009-3044（2014）15-3509-03

　　Web Services Composition Modeling and Verification Based on Petri Net
　　DING Chong-chong， LI Ting-ting
　�。–ollege of Information Engineering， Nanjing University of Finance and Economics， Nanjing 210046， China）
　　Abstract： This paper first puts forward Web services composition modeling method based on Petri net. The formal modeling for Web services composition is also the article research content. Then the paper uses the reachability tree as the analytical tool to analyse and verify the features of services composition model， such as accessibility， activity and boundedness. Finally， the article uses a specific example to illustrate the application of this method.
　　Key words： Web services； Petri net； reachability tree； Web services composition； verification
　　基于Petri網(wǎng)的形式化建模方法是Web服務(wù)組合建模的一種重要的手段。Petri網(wǎng)是一種基于狀態(tài)的建模方法，具有直觀的圖形表示，形式化語義定義，豐富的分析技術(shù)等優(yōu)點。同時，由于Web服務(wù)的獨立性和自治性，通過多個Web服務(wù)組合完成的業(yè)務(wù)流程的正確性難以保證，因此必須要對服務(wù)組合進(jìn)行驗證。基于Petri網(wǎng)的許多優(yōu)點，該文利用可達(dá)樹作為分析工具，對服務(wù)組合模型的可達(dá)性，活性，有界性等特性進(jìn)行驗證分析，進(jìn)而驗證服務(wù)組合模型的正確性。
　　1 基于Petri網(wǎng)的Web服務(wù)組合
　　1.1 Petri網(wǎng)的定義
　　2） T為變遷結(jié)點集合，代表引起系統(tǒng)狀態(tài)改變的事件。
　　3） W為庫所結(jié)點和變遷結(jié)點之間的有向弧集合，即流關(guān)系。
　　4） M0 為PN的初始標(biāo)識。
　　5） i為輸入庫所，即i=φ。
　　6） o為輸出庫所，即o=φ。
　　1.2 Web服務(wù)組合的Petri網(wǎng)模型
　　由于Web服務(wù)在行為上是操作的偏序集，所以可以直接將Web服務(wù)映射到Petri網(wǎng)上。
　　服務(wù)的操作對應(yīng)于變遷元素，服務(wù)的狀態(tài)對應(yīng)于庫所，其中，Web服務(wù)的狀態(tài)有五種，分別為“未實例化”、“就緒”、“執(zhí)行”、“暫停”、“完成”。操作與狀態(tài)之間的因果關(guān)系則作為變遷與庫所之間的流關(guān)系。基于Petri網(wǎng)，Web服務(wù)被定義為一個六元組，S=（Id，SName，SDesc，URL，CS，PN），其中：
　　1） Id為Web服務(wù)的唯一標(biāo)識。
　　2） SName為Web服務(wù)的名稱。
　　3） SDesc為Web服務(wù)的描述。
　　4） URL為服務(wù)的調(diào)用地址。
　　6） PN為Web服務(wù)的Petri網(wǎng)。
　　1.3 服務(wù)的組合結(jié)構(gòu)
　　Web服務(wù)組合的組件由原子服務(wù)和合成操作組合而成。其中，此處原子服務(wù)可能是基本服務(wù)，也可能是組合服務(wù)�；�本的組合操作有順序，選擇，循環(huán)，并行，調(diào)用這五種類型，這些組合操作可以由基本服務(wù)組合而成，其他更復(fù)雜的服務(wù)組合操作可以由這些基本的組合結(jié)構(gòu)組合而成。基本服務(wù)的Petri網(wǎng)結(jié)構(gòu)如下，其中i，o分別表示服務(wù)的輸入和輸出庫所，s表示服務(wù)的操作。
　　給Web服務(wù)建模以后，接下來就可以應(yīng)用Petri網(wǎng)的分析方法來進(jìn)行驗證分析。
　　2 Web服務(wù)組合的驗證
　　Petri網(wǎng)提供了許多強(qiáng)大的分析工具，，如可達(dá)樹分析、可達(dá)圖分析、馬爾可夫分析、關(guān)聯(lián)矩陣與狀態(tài)方程、Petri網(wǎng)語言等。其中，可達(dá)樹是用來描述所有從初始狀態(tài)開始的可達(dá)狀態(tài)。在可達(dá)樹中，M0代表樹的根結(jié)點，葉子結(jié)點代表系統(tǒng)的最終狀態(tài)，弧代表相關(guān)的轉(zhuǎn)換。從根結(jié)點到一個確定的結(jié)點的路徑代表一個可執(zhí)行的序列。該文采用可達(dá)樹作為分析工具。通過對Petri網(wǎng)的性質(zhì)進(jìn)行驗證，可以驗證組合服務(wù)的正確性。具體的可達(dá)樹構(gòu)造算法這里不再列出，詳見文獻(xiàn)[7]。Petri網(wǎng)的主要性質(zhì)有：
　　3 Web服務(wù)組合的驗證實例分析
　　某公司員工要到外地出差，由于目的地距離公司所在地較遠(yuǎn)，該員工打算乘坐高鐵或者飛機(jī)去往目的地。首先該員工要通過火車票查由上述分析可知，該服務(wù)組合模型是合理的，滿足正確性的要求。
　　4 結(jié)束語
　　本文提出了一種基于Petri網(wǎng)對組合服務(wù)進(jìn)行建模的方法，給出了Web服務(wù)的形式化定義，并給出了圖形化表示，最后結(jié)合具體的實例來進(jìn)行建模分析，并采用可達(dá)樹作為分析工具來驗證組合服務(wù)的正確性。Petri網(wǎng)提供了一種有效的手段去模擬、分析和驗證Web服務(wù)組合，然而，在建立許多大型、復(fù)雜的系統(tǒng)模型時，Petri網(wǎng)也表現(xiàn)出了一些明顯的不足。 所以，如何在建立復(fù)雜Petri網(wǎng)模型時，盡量降低其復(fù)雜度是接下來的主要研究工作。