摘要：基于Petri網的形式化建模方法是Web服務組合建模的一種重要的手段。Petri網是一種基于狀態的建模方法，具有直觀的圖形表示，形式化語義定義，豐富的分析技術等優點。同時，由于Web服務的獨立性和自治性，通過多個Web服務組合完成的業務流程的正確性難以保證，因此必須要對服務組合進行驗證。基于Petri網的許多優點，該文利用可達樹作為分析工具，對服務組合模型的可達性，活性，有界性等特性進行驗證分析，進而驗證服務組合模型的正確性。

　　1 基于Petri網的Web服務組合

　　1.1 Petri網的定義

　　2) T為變遷結點集合，代表引起系統狀態改變的事件。

　　3) W為庫所結點和變遷結點之間的有向弧集合，即流關系。

　　4) M0 為PN的初始標識。

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

　　6) o為輸出庫所，即o=φ。

　　1.2 Web服務組合的Petri網模型

　　由于Web服務在行為上是操作的偏序集，所以可以直接將Web服務映射到Petri網上。

　　服務的操作對應于變遷元素，服務的狀態對應于庫所，其中，Web服務的狀態有五種，分別為“未實例化”、“就緒”、“執行”、“暫停”、“完成”。操作與狀態之間的因果關系則作為變遷與庫所之間的流關系。基于Petri網，Web服務被定義為一個六元組，S=(Id，SName，SDesc，URL，CS，PN)，其中：

　　1) Id為Web服務的唯一標識。

　　2) SName為Web服務的名稱。

　　3) SDesc為Web服務的描述。

　　4) URL為服務的調用地址。

　　6) PN為Web服務的Petri網。

　　1.3 服務的組合結構

　　Web服務組合的組件由原子服務和合成操作組合而成。其中，此處原子服務可能是基本服務，也可能是組合服務。基本的組合操作有順序，選擇，循環，并行，調用這五種類型，這些組合操作可以由基本服務組合而成，其他更復雜的服務組合操作可以由這些基本的組合結構組合而成。基本服務的Petri網結構如下，其中i，o分別表示服務的輸入和輸出庫所，s表示服務的操作。

　　給Web服務建模以后，接下來就可以應用Petri網的分析方法來進行驗證分析。

　　2 Web服務組合的驗證

　　Petri網提供了許多強大的分析工具，如可達樹分析、可達圖分析、馬爾可夫分析、關聯矩陣與狀態方程、Petri網語言等。其中，可達樹是用來描述所有從初始狀態開始的可達狀態。在可達樹中，M0代表樹的根結點，葉子結點代表系統的最終狀態，弧代表相關的轉換。從根結點到一個確定的結點的路徑代表一個可執行的序列。該文采用可達樹作為分析工具。通過對Petri網的性質進行驗證，可以驗證組合服務的正確性。具體的可達樹構造算法這里不再列出，詳見文獻[7]。Petri網的主要性質有：

　　3 Web服務組合的驗證實例分析

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

　　4 結束語

　　本文提出了一種基于Petri網對組合服務進行建模的方法，給出了Web服務的形式化定義，并給出了圖形化表示，最后結合具體的實例來進行建模分析，并采用可達樹作為分析工具來驗證組合服務的正確性。Petri網提供了一種有效的手段去模擬、分析和驗證Web服務組合，然而，在建立許多大型、復雜的系統模型時，Petri網也表現出了一些明顯的不足。 所以，如何在建立復雜Petri網模型時，盡量降低其復雜度是接下來的主要研究工作。