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

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

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

　　Web Services Composition Modeling and Verification Based on Petri Net
　　DING Chong-chong， LI Ting-ting
　　（College 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)的建模方法，具有直觀的圖形表示，形式化語(yǔ)義定義，豐富的分析技術(shù)等優(yōu)點(diǎn)。同時(shí)，由于Web服務(wù)的獨(dú)立性和自治性，通過(guò)多個(gè)Web服務(wù)組合完成的業(yè)務(wù)流程的正確性難以保證，因此必須要對(duì)服務(wù)組合進(jìn)行驗(yàn)證�；赑etri網(wǎng)的許多優(yōu)點(diǎn)，該文利用可達(dá)樹(shù)作為分析工具，對(duì)服務(wù)組合模型的可達(dá)性，活性，有界性等特性進(jìn)行驗(yàn)證分析，進(jìn)而驗(yàn)證服務(wù)組合模型的正確性。
　　1 基于Petri網(wǎng)的Web服務(wù)組合
　　1.1 Petri網(wǎng)的定義
　　2） T為變遷結(jié)點(diǎn)集合，代表引起系統(tǒng)狀態(tài)改變的事件。
　　3） W為庫(kù)所結(jié)點(diǎn)和變遷結(jié)點(diǎn)之間的有向弧集合，即流關(guān)系。
　　4） M0 為PN的初始標(biāo)識(shí)。
　　5） i為輸入庫(kù)所，即i=φ。
　　6） o為輸出庫(kù)所，即o=φ。
　　1.2 Web服務(wù)組合的Petri網(wǎng)模型
　　由于Web服務(wù)在行為上是操作的偏序集，所以可以直接將Web服務(wù)映射到Petri網(wǎng)上。
　　服務(wù)的操作對(duì)應(yīng)于變遷元素，服務(wù)的狀態(tài)對(duì)應(yīng)于庫(kù)所，其中，Web服務(wù)的狀態(tài)有五種，分別為“未實(shí)例化”、“就緒”、“執(zhí)行”、“暫停”、“完成”。操作與狀態(tài)之間的因果關(guān)系則作為變遷與庫(kù)所之間的流關(guān)系�；赑etri網(wǎng)，Web服務(wù)被定義為一個(gè)六元組，S=（Id，SName，SDesc，URL，CS，PN），其中：
　　1） Id為Web服務(wù)的唯一標(biāo)識(shí)。
　　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ù)�；镜慕M合操作有順序，選擇，循環(huán)，并行，調(diào)用這五種類型，這些組合操作可以由基本服務(wù)組合而成，其他更復(fù)雜的服務(wù)組合操作可以由這些基本的組合結(jié)構(gòu)組合而成�；痉⻊�(wù)的Petri網(wǎng)結(jié)構(gòu)如下，其中i，o分別表示服務(wù)的輸入和輸出庫(kù)所，s表示服務(wù)的操作。
　　給Web服務(wù)建模以后，接下來(lái)就可以應(yīng)用Petri網(wǎng)的分析方法來(lái)進(jìn)行驗(yàn)證分析。
　　2 Web服務(wù)組合的驗(yàn)證
　　Petri網(wǎng)提供了許多強(qiáng)大的分析工具，，如可達(dá)樹(shù)分析、可達(dá)圖分析、馬爾可夫分析、關(guān)聯(lián)矩陣與狀態(tài)方程、Petri網(wǎng)語(yǔ)言等。其中，可達(dá)樹(shù)是用來(lái)描述所有從初始狀態(tài)開(kāi)始的可達(dá)狀態(tài)。在可達(dá)樹(shù)中，M0代表樹(shù)的根結(jié)點(diǎn)，葉子結(jié)點(diǎn)代表系統(tǒng)的最終狀態(tài)，弧代表相關(guān)的轉(zhuǎn)換。從根結(jié)點(diǎn)到一個(gè)確定的結(jié)點(diǎn)的路徑代表一個(gè)可執(zhí)行的序列。該文采用可達(dá)樹(shù)作為分析工具。通過(guò)對(duì)Petri網(wǎng)的性質(zhì)進(jìn)行驗(yàn)證，可以驗(yàn)證組合服務(wù)的正確性。具體的可達(dá)樹(shù)構(gòu)造算法這里不再列出，詳見(jiàn)文獻(xiàn)[7]。Petri網(wǎng)的主要性質(zhì)有：
　　3 Web服務(wù)組合的驗(yàn)證實(shí)例分析
　　某公司員工要到外地出差，由于目的地距離公司所在地較遠(yuǎn)，該員工打算乘坐高鐵或者飛機(jī)去往目的地。首先該員工要通過(guò)火車(chē)票查由上述分析可知，該服務(wù)組合模型是合理的，滿足正確性的要求。
　　4 結(jié)束語(yǔ)
　　本文提出了一種基于Petri網(wǎng)對(duì)組合服務(wù)進(jìn)行建模的方法，給出了Web服務(wù)的形式化定義，并給出了圖形化表示，最后結(jié)合具體的實(shí)例來(lái)進(jìn)行建模分析，并采用可達(dá)樹(shù)作為分析工具來(lái)驗(yàn)證組合服務(wù)的正確性。Petri網(wǎng)提供了一種有效的手段去模擬、分析和驗(yàn)證Web服務(wù)組合，然而，在建立許多大型、復(fù)雜的系統(tǒng)模型時(shí)，Petri網(wǎng)也表現(xiàn)出了一些明顯的不足。 所以，如何在建立復(fù)雜Petri網(wǎng)模型時(shí)，盡量降低其復(fù)雜度是接下來(lái)的主要研究工作。