摘要：基于Petri網(wǎng)的形式化建模方法是Web服務(wù)組合建模的一種重要的手段。Petri網(wǎng)是一種基于狀態(tài)的建模方法，具有直觀的圖形表示，形式化語義定義，豐富的分析技術(shù)等優(yōu)點(diǎn)。同時(shí)，由于Web服務(wù)的獨(dú)立性和自治性，通過多個(gè)Web服務(wù)組合完成的業(yè)務(wù)流程的正確性難以保證，因此必須要對(duì)服務(wù)組合進(jìn)行驗(yàn)證?；赑etri網(wǎng)的許多優(yōu)點(diǎn)，該文利用可達(dá)樹作為分析工具，對(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為庫所結(jié)點(diǎn)和變遷結(jié)點(diǎn)之間的有向弧集合，即流關(guān)系。

　　4) M0 為PN的初始標(biāo)識(shí)。

　　5) i為輸入庫所，即i=φ。

　　6) o為輸出庫所，即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)于庫所，其中，Web服務(wù)的狀態(tài)有五種，分別為“未實(shí)例化”、“就緒”、“執(zhí)行”、“暫停”、“完成”。操作與狀態(tài)之間的因果關(guān)系則作為變遷與庫所之間的流關(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ù)。基本的組合操作有順序，選擇，循環(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)行驗(yàn)證分析。

　　2 Web服務(wù)組合的驗(yàn)證

　　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é)點(diǎn)，葉子結(jié)點(diǎn)代表系統(tǒng)的最終狀態(tài)，弧代表相關(guān)的轉(zhuǎn)換。從根結(jié)點(diǎn)到一個(gè)確定的結(jié)點(diǎn)的路徑代表一個(gè)可執(zhí)行的序列。該文采用可達(dá)樹作為分析工具。通過對(duì)Petri網(wǎng)的性質(zhì)進(jìn)行驗(yàn)證，可以驗(yàn)證組合服務(wù)的正確性。具體的可達(dá)樹構(gòu)造算法這里不再列出，詳見文獻(xiàn)[7]。Petri網(wǎng)的主要性質(zhì)有：

　　3 Web服務(wù)組合的驗(yàn)證實(shí)例分析

　　某公司員工要到外地出差，由于目的地距離公司所在地較遠(yuǎn)，該員工打算乘坐高鐵或者飛機(jī)去往目的地。首先該員工要通過火車票查由上述分析可知，該服務(wù)組合模型是合理的，滿足正確性的要求。

　　4 結(jié)束語

　　本文提出了一種基于Petri網(wǎng)對(duì)組合服務(wù)進(jìn)行建模的方法，給出了Web服務(wù)的形式化定義，并給出了圖形化表示，最后結(jié)合具體的實(shí)例來進(jìn)行建模分析，并采用可達(dá)樹作為分析工具來驗(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ù)雜度是接下來的主要研究工作。