采用函數式語言的BPEL模型形式化驗證方法*

祝 義，黃志球，周 航

1.南京航空航天大學 計算機科學與技術學院，南京 210016

2.江蘇師范大學 計算機科學與技術學院，江蘇 徐州 221116

1 引言

面向服務的計算（service oriented computing）是互聯網上典型的分布式計算應用。在過去20年里，Web服務組合已經成為應用集成與互操作研究與開發中最活躍的領域之一。WS-BPEL（Web services business process execution language）是由OASIS組織為了規約Web服務中業務流程行為提出的標準執行語言。盡管已經對BPEL模型展開深入研究，然而其可靠性、普適性、個體性等仍需要被討論，尤其是諸如云計算、社交網絡以及物聯網技術迅速發展后，人們對BPEL模型的可靠性要求越來越高，如何進一步提高復雜BPEL模型的可靠性已經成為一個關鍵問題[1]。

形式化方法，源于Dijkstra和Hoare的程序驗證，其主要優點是具有精確性，可以驗證，并且便于機器支撐和自動處理等。這些特點對克服目前復雜BPEL模型的可靠性差，難以實現自動化的困境具有明顯的作用。進程代數是一種用來解決并發系統通信問題的形式化方法，可以描述和分析并發、異步、非確定等系統行為，具有良好的語義與可擴展性，使得它非常適合于BPEL模型的建模與分析。通信順序進程（communicating sequential process，CSP）是Hoare[2]在1978年提出的一種能夠對并發系統進行模型檢測的進程代數方法。CSPM是一種基于CSP的惰性函數式程序語言，可用于機器執行。FDR（failure divergence refinement）是一種基于CSPM描述的分析程序工具，牛津大學于2016年發布了最新版本FDR3.4[3]。

WS-BPEL結合了XLANG[4]和WSFL（Web services flow language）[5]的特征，可以建模多個服務共同參與的業務流程行為。WS-BPEL通過抽象業務流程和可執行業務流程來描述Web服務，其入口和出口信息通過唯一的Web服務接口來定義。其中，抽象業務流程描述業務流程中單個服務的接口行為，可執行業務流程描述業務流程中服務之間的交互以及業務流程的內部邏輯。

為了讓Web服務能夠組合在一起并順利執行，需要對來自不同組織的Web服務進行分析與驗證，主要是保證服務組合在執行過程中不會出現死鎖或沖突。這種分析與驗證工作主要包含三方面[6]：語法相容性、語義相容性以及行為相容性。其中，語法相容性是指各成員服務的交互接口應該是一致的，WSDL（Web services description language）已為Web服務提供了標準的接口規約方法；語義相容性是指各成員服務之間交互的信息應該是精確的、無二義的；行為相容性是指各成員服務應該在操作的執行上達成一致。當前很多研究工作者針對Web服務組合驗證開展了很多工作，一般都是基于某種形式化方法，例如通過進程代數、Petri網或自動機對Web服務組合建模，然后在形式化模型中進行分析與驗證。但是這些方法大多數不具備程序設計能力，因此直接通過形式化方法描述的Web服務組合很難在實踐中得以推廣。

本文貢獻在于將CSPM與BPEL進行了深度結合。首先在語言層次上建立BPEL到CSPM的映射，這樣能夠將通過BPEL建立的模型映射為CSPM模型；然后通過模型檢測工具FDR對CSPM模型的活性、安全性、確定性和無死鎖性分別進行模型檢測；最后將CSPM模型檢測的結果用于BPEL模型的修改，這樣能夠在很大程度上提高BPEL模型的可靠性。

本文組織結構如下：第2章提出了基于CSPM的BPEL模型建模與驗證框架；第3章給出了CSPM的進程代數定義；第4章詳細描述了BPEL到CSPM的映射方法；第5章以一個在線購物系統為例，討論了本文方法的使用效果；第6章進行相關工作比較；第7章總結全文并給出結論。

2 基于CSPM的BPEL模型建模與驗證框架

為了從根本上提高BPEL建模的可靠性，本文建立了基于CSPM的BPEL模型建模與驗證框架。如圖1所示。

Fig.1 Framework for modeling and verifying BPEL model based on CSPM圖1 基于CSPM的BPEL模型建模與驗證框架

該框架主要包含以下基本步驟：第1步在語言層次上建立BPEL到CSPM的映射機制，實現BPEL模型到CSPM模型的轉換；第2步將轉換得到的CSPM模型輸入到模型檢測工具FDR，保存為擴展名為.csp的模型文件，即實現（implementation），為進一步模型檢測做好準備；第3步根據要檢查的BPEL模型性質建立CSPM斷言，即規約（specification），例如安全性、活性、確定性和無死鎖性斷言；第4步將CSPM斷言逐個輸入到FDR進行模型檢測，如果正確，就表明該斷言通過模型檢測，如果錯誤，FDR則輸出反例，反例通過比較規約行為跡與實現行為跡來找出進程中的錯誤；第5步根據反例對CSPM模型（實現）進行修改，并重新輸入到FDR中進行模型檢測，如此循環，直至所有CSPM斷言（規約）都驗證通過；第6步根據模型檢測結果對BPEL模型進行修改，得到可信BPEL模型。

3 CSPM的進程代數定義

CSPM是基于CSP的惰性函數式編程語言，因此下面主要討論Web服務與CSP之間的關系。將Web服務映射為進程，并將Web服務的每條指令映射為進程中的事件，那么Web服務的組合特征表現為進程的并發特征。

定義1（通信順序進程）一個通信順序進程CSP可定義為：

Σ={a0,a1,…,an-1}是可觀察事件集合，ai∈Σ，0≤i＜n-1，A∈PΣ，PΣ為Σ的冪集；X是進程變量。定義解釋如下：

STOP：停止，表示進程不與外界發生任何通信，通常表示進程死鎖或不收斂；

SKIP：跳過，表示進程不做任何事情直到最后停止；

a→P：前綴操作，表示事件a執行后執行進程P；

P;Q：順序復合，表示進程P執行后執行進程Q；

P＜expr＞Q：條件復合，表示expr表達式為真時執行進程P，否則執行進程Q；

P□Q：外部選擇，表示執行進程P或Q依賴于進程執行的第一個事件；

P||Q：同步并發，P僅能執行α(P)中的事件，Q僅能執行α(Q)中的事件，α(P)?α(Q)的事件P與Q同步執行；

μX·F(X)：X是一個進程變量，F(X)是包含X的前綴表達式，該遞歸方程具有事件集A上的唯一解，其中A=αX。

此外，CSP提供通道表示一類事件的集合，例如channel a：Int，表示通道a能夠與任何帶有整型數據的事件通信，事件a.1是通道a聲明的一個元素。

4 BPEL語言到CSPM語言的映射方法

為了驗證BPEL模型的相關性質，首先要建立BPEL語言到CSPM語言的映射機制，實現BPEL模型到CSPM模型的轉換。在WS-BPEL2.0規約中，receive、reply、invoke、sequence、switch、pick、while和 flow 是描述BPEL控制邏輯的關鍵元素。本文主要關注Web服務行為的控制邏輯方面，因此不考慮BPEL中的 compensation、fault handler、assign、correlation set、link condition和variables等元素。下面介紹BPEL語言到CSPM語言的映射方法。

4.1 基本活動映射

（1）invoke活動

invoke活動主要用來獲取伙伴服務所提供的功能，它通過操作向伙伴服務發送服務調用消息。invoke活動分為單向調用和請求回復調用兩種類型。單向invoke活動只向伙伴服務發送服務調用請求，而不需回復，但是請求回復調用除了發送請求外同時還需回復。單向invoke活動的映射過程是將發送的請求對應到CSP的一個輸出動作。具體映射關系如圖2所示。

Fig.2 Mapping from action one-wayinvoketo CSP圖2 單向invoke活動到CSP的映射

對于請求回復invoke活動，將請求和回復消息分別對應到CSP的輸出和輸入活動，具體映射關系如圖3所示。

Fig.3 Mapping from action request-replyinvoketo CSP圖3 請求回復invoke活動到CSP的映射

單向invoke活動在CSPM中表示為op!message?P。雙向invoke活動在CSPM中表示為op!message1?op?message2?P。

（2）receive活動

receive活動主要是用戶接受伙伴服務的消息調用。它的映射規則是，將receive活動接受的消息對應到CSP的一個輸入動作。具體映射關系如圖4所示。

Fig.4 Mapping from actionreceiveto CSP圖4 receive活動到CSP的映射

receive活動在CSPM中表示為op?message?P。

（3）reply活動

reply活動主要對先前接受的receive活動發送相應的請求響應。它的轉換規則是，將reply活動發送的消息對應到CSP的一個輸出動作。具體映射關系如圖5所示。

Fig.5 Mapping from actionreplyto CSP圖5 reply活動到CSP的映射

reply活動在CSPM中表示為op!message?P。

4.2 組合活動映射

（1）sequence活動

sequence活動主要用于表示子活動之間的順序結構的控制流關系。它的映射規則是，將前面一個活動的進程P1中的阻塞狀態和后面一個活動的進程P2中的初始狀態融合成一個狀態，從而將兩個進程“串行”地聯接成一個進程，多個進程的順序結構依此類推。其中，Pi為執行完第i個子活動acti的系統后繼進程，i∈N且1≤i≤n。具體映射關系如圖6所示。

當αP={act}時，即子活動為原子活動時，上述進程表達式簡化為：

Fig.6 Mapping from actionsequenceto CSP圖6 sequence活動到CSP的映射

sequence活動在CSPM中可表示如下：

（2）switch活動

switch活動主要用于控制分支條件選擇，當執行某個活動的前提條件得到滿足時，該活動就被選擇，等到該活動執行完畢，switch活動結束。switch活動的映射過程是，首先獲得待選擇的各分支活動的進程P1,P2,…,Pn，然后將各分支進程的初始狀態融合為一個統一的初始狀態，同時將各分支進程的阻塞狀態融合為一個統一的阻塞狀態。具體映射關系如圖7所示。

Fig.7 Mapping from actionswitchto CSP圖7 switch活動到CSP的映射

switch活動在CSPM中可表示為：

（3）while活動

while活動定義了一種典型循環結構，只要條件為真，指定活動就反復執行，直到條件為假時while活動才結束。while活動的轉換過程是，首先獲得指定活動的進程，接著將該進程中指向阻塞狀態的遷移都改為指向初始狀態，最后再添加一個從初始狀態轉換到阻塞狀態的遷移，該遷移表示為一個空操作。具體映射關系如圖8所示。

Fig.8 Mapping from actionwhileto CSP圖8 while活動到CSP的映射

while活動在CSPM中表示為：

（4）pick活動

pick活動包含若干個onMessage元素，它等待特定的消息到達，當最先收到某個消息時，就觸發該消息對應的活動，當該活動執行完畢后，pick活動結束。pick活動的轉換過程是，首先將觸發每個活動所對應的消息看作一個receive活動，然后再將它們融合成一個順序執行活動。最后將各順序活動融合成一個分支選擇活動。具體映射關系如圖9所示。

pick活動在CSPM中表示為：

（5）flow活動

Fig.9 Mapping from actionpickto CSP圖9 pick活動到CSP的映射

Fig.10 Mapping from actionflowto CSP圖10 flow活動到CSP的映射

flow活動主要用于表示各個子活動的并發執行，可以用CSP中并發操作符來表示。具體映射關系如圖10所示。

flow活動在CSPM中表示為：

目前，已經通過基于MDE（model driven engineering）[7]的AMMA（ATLAS model management architecture）[8]平臺初步完成了原型系統設計。AMMA開發平臺為法國ATLAS（Atlantic data systems）研究組設計的通用模型轉換平臺，平臺的模型轉換語言ATL（ATLAS transformation language）是AMMA平臺的一部分，它是一種模型轉換語言和工具集，提供了從源模型產生目標模型的方法。ATL在Eclipse平臺上的集成開發環境（integrated development environment，IDE）提供了標準的用于模型轉換的開發工具。首先，基于AMMA平臺的KM3元模型體系，通過元建模構造BPEL元模型和CSP元模型；其次，利用ATL針對BPEL元模型和CSP元模型構造轉換規則，通過將對應的實例模型進行相互轉換，實現在MDE下BPEL模型到CSP模型的轉換；最后，通過建立模型到文本的轉換將CSP模型轉換為CSPM代碼，CSPM代碼可以直接導入到FDR工具中編譯執行。

5 實例

一個在線購物（online shopping）應用共涉及顧客（Buyer）、售貨商（Seller）、銀行（Banker）、郵局（Postoffice）和快遞公司（Shipper）5個協作服務。交易之初，Buyer向Seller發送訂單請求消息（ordreq），Seller接收到ordreq后，向Banker發送貨款支付請求消息（payreq），如果Buyer的銀行卡可用額度能夠支付所定貨物，則Banker向Seller返回支付成功消息（payok），否則返回支付失敗消息（payfail）。當Seller收到payok，則選擇Postoffice或者Shipper向Buyer發送貨物（postreq/shipreq），貨物發送完成后（postend/shipend），Seller再通知Buyer貨物運送完成(postsucc/shipsucc）。如果Buyer的銀行卡可用額度不能支付所定貨物，則Seller拒絕Buyer的本次訂單（rejection）。在線購物為了完成共同的業務目標，它們共享數據，通過發送和接收消息向合作伙伴請求并提供服務。通過以上分析，首先通過BPEL對該組合服務建模，如圖11所示。

Fig.11 BPEL model of online shopping圖11 在線購物BPEL模型

然后將建模結果通過第3章介紹的映射方法進行映射，得到的在線購物CSP模型表示如下：由于在CSPM中進程必須要標準化（normalize），因此OS（online shopping）進程按階段被劃分為BS（Buyer-Seller）、BSB（Buyer-Seller-Banker）、BSBS（Buyer-Seller-Banker-Shipper）以及BSBP（Buyer-Seller-Banker-Postoffice）4個進程，上述CSP在CSPM中代碼如下：

將上述CSPM代碼存為OnlineShoping.csp文件并通過FDR3打開，接下來通過FDR3分別對其安全性、活性、確定性以及無死鎖性進行模型檢測。在FDR3中建立的CSPM斷言以及模型檢測結果如下。

（1）安全性

以上斷言表示進程BS、BSB、BSBS、BSBP跡精化于進程OS，即trace(BS)?trace(OS)、trace(BSB)?trace(OS)、trace(BSBS)?trace(OS)、trace(BSBP)? trace(OS)。模型檢測結果如圖12所示。

（2）活性

該斷言表示進程BS、BSB、BSBS、BSBP失效/發散精化于進程OS，即failures(BS)?failures(OS)且divergences(BS)?divergences(OS)，failures(BSB)?failures(OS)且 divergences(BSB)?divergences(OS)，failures(BSBS)?failures(OS)且 divergences(BSBS)?divergences(OS)，failures(BSBP)? failures(OS)且 divergences(BSBP)?divergences(OS)。模型檢測結果如圖13所示。

（3）確定性

Fig.12 Safety checking of online shopping圖12 在線購物系統安全性檢測結果

Fig.13 Liveness checking of online shopping圖13 在線購物系統活性檢測結果

該斷言表示進程BS、BSB、BSBS、BSBP、OS都不會發散，不會出現任何既可接受又可拒絕的行為選擇。例如對于進程OS而言，OS是確定性進程表明divergences(OS)={}并且 s^＜a＞∈trace(OS)?(s,{a})?failures(OS)。模型檢測結果如圖14所示。

（4）無死鎖性

該斷言表示進程BS、BSB、BSBS、BSBP、OS都無死鎖。例如對于進程OS而言，OS無死鎖表明對于任意跡s而言，(s,∑)?failures(OS)。模型檢測結果如圖15所示。

以上實驗結果顯示所有進程都通過了FDR模型檢測，表明在線購物系統CSPM模型具有極高的可靠性。接下來根據模型檢測結果對BPEL模型進行修改，最后可以得到高可信的BPEL模型。

另外，還可以根據圖1中反例生成原理檢查系統單個行為以及組合行為的正確性。

（1）單個行為的正確性

假設Seller沒有收到Banker確認的payok消息，就可以選擇Postoffice或者Shipper向Buyer發送貨物（postreq/shipreq）。

在FDR中對SELLER進程進行相應的修改：

Fig.15 Deadlock freedom checking of online shopping圖15 在線購物系統無死鎖性檢測結果

編譯執行后發現斷言assert OS[T=BS，就不能通過模型檢測，通過Debug可以看到FDR產生的反例。BS進程在執行ordreq后可接受事件為payreq，但OS進程在執行ordreq后拒絕除了payok之外的所有事件，進程進入死鎖狀態。反例說明SELLER只有在收到Banker發來的payok之后才能發貨，否則系統就會因為沒有可同步的事件進入死鎖狀態。

（2）組合行為的正確性

假設Shipper或者Postoffice是并行關系。在FDR中對OS進程修改如下：

OS=BSBS[|{||}|]BSBP

編譯執行后發現斷言assert OS[FD=BS沒有通過模型檢測，通過Debug可以看到FDR產生的反例。BS進程在執行ordreq后可接受事件為payreq，OS進程在執行ordreq后可接受事件為payreq和ordreq，但BS進程拒絕連續執行兩次ordreq，因此進程進入死鎖狀態。反例說明OS進程在收到Buyer的訂單請求ordreq后沒有經過任何處理可以再次接受訂單請求，這與實際情況不符。出現這一狀況的原因是BSBS進程與BSBP進程是并行關系，也就是說既可以選擇Shipper，也可以選擇Postoffice運送貨物，因此OS進程允許連續執行兩次ordreq，而實際情況只能選擇Shipper和Postoffice兩者之一運送貨物，因此BSBS與BSBP不能是并行關系，必須是選擇關系。

參照以上反例產生的過程，能夠檢查系統其他行為的正確性，由于篇幅原因，此處不再贅述。

6 相關工作比較

目前關于BPEL業務流程形式化建模與驗證代表性的工作包括以下三方面：

（1）直接使用進程代數描述與驗證BPEL業務流程的相關性質。文獻[9]通過進程演算建模Web服務的編排與編制，將進程演算中互模擬的方法用于檢驗編排與編制之間的一致性。文獻[10]提出了一種代價概率進程代數（priced probabilistic process algebra，PPPA），并給出了基于PPPA統一建模和分析Web服務組合功能和QoS的方法。文獻[11]通過轉換WSCI（Web service choreography interface）標準到CCS來進行Web服務編排分析，并分析了參與編排的服務交互行為的相容性和可替換性，對于不相容的服務提供適配器實現通信。文獻[12]將任務映射為進程，任務間的連接映射為通道，通過Pi演算對Web服務之間的交互行為進行建模。

（2）直接使用自動機描述與驗證BPEL業務流程的相關性質。文獻[13-14]使用衛式自動機（guarded automata）對Web服務的BPEL流程進行建模，將服務組合看作服務之間通過異步消息傳遞的全局會話協議，并將會話協議的同步條件以及系統目標屬性用線性時序邏輯（linear temporal logic，LTL）描述，然后通過模型檢驗工具SPIN進行驗證。文獻[15]利用有限狀態機分別對Web服務和編排進行建模，使用有向圖描述Web服務的證書暴露策略，并通過匹配證書暴露以及訪問控制策略來驗證編排的所有可能會話。文獻[16]利用時間自動機對帶時間約束的Web服務行為進行建模，并在此基礎上分析了服務之間以及服務與規約之間的時間行為相容性和可替換性。

（3）直接使用Petri網描述與驗證BPEL業務流程的相關性質。文獻[17]提出了一種基于服務簇的服務組合方法，并應用邏輯Petri網對其進行形式化建模描述。文獻[18]針對如何有效評估服務系統的性能表現，提出了一種基于排隊Petri網的性能建模和分析方法。文獻[19]針對如何有效發現Web服務組合中性能瓶頸的問題，提出了一種基于隨機Petri網的Web服務組合性能分析模型。文獻[20]轉換抽象BPEL過程到有色Petri網，通過分析交互服務之間的行為相容性，將部分相容的服務進行了自動組合。

上述方法能夠描述與驗證BPEL業務流程的相關性質，但這些形式化方法不具備程序設計能力，沒有從程序語言層次上建立BPEL到形式化模型的映射關系，因此很難從實際應用中判斷這些方法的實用價值。與以上研究工作相比，本文在BPEL業務流程建模與驗證方面另辟新徑：從模型映射的角度來看，基于程序語言層面映射得到的CSPM模型保留了BPEL業務流程的完整語義，因此通過這種方法建立的BPEL模型具有極高的可靠性；從可追蹤性的角度來看，因為BPEL與CSPM之間的映射是一對一的，所以BPEL業務流程與CSPM模型之間保持了良好的可追蹤性，從而CSPM模型檢測結果可以直接用于BPEL業務流程建模與修改。此外，本文工作也為可信軟件設計提供了新的思路，給出了一套實踐中切實可行的解決方案。

7 總結與展望

本文在研究了BPEL業務流程形式化建模與驗證相關工作的基礎上，提出了一種基于CSPM的BPEL業務流程建模與驗證方法，為提高BPEL業務流程建模可靠性找到一條新的行之有效的途徑。主要工作為：給出基于CSPM的BPEL業務流程建模與驗證框架；根據BPEL業務流程特征給出了CSPM的進程代數定義；詳細描述了BPEL到CSPM的映射方法；通過在線購物系統建模實例說明了該方法如何應用于BPEL業務流程建模與驗證。

此外，本文沒有考慮BPEL業務流程建模中涉及到的時間、資源、隱私等非功能性質的驗證問題，因此進一步工作是在現有研究基礎上擴展CSPM的非功能性質，并將其應用于基于進程代數的BPEL業務流程的建模與驗證方法中。

[1]Sheng Q Z,Qiao Xiaoqiang,Vasilakos A V,et al.Web services composition:a decade's overview[J].Information Science,2014,280:218-238.

[2]Hoare CAR.Communicating sequential processes[J].Communications of theACM,1978,21(8):666-677.

[3]University of Oxford.fdr3-3702-windows-x86_64.msi[EB/OL].(2016).http://www.cs.ox.ac.uk/projects/fdr/.

[4]Microsoft.Web services for business process design(XLANG)[EB/OL].(2003).http://xml.coverpages.org/xlang.html.

[5]IBM.Web services flow language(WSFL)[EB/OL].(2003).http://xml.coverpages.org/wsfl.html.

[6]Li Xitong,Fan Yushun,Sheng Q Z,et al.APetri net approach to analyzing behavioral compatibility and similarity of Web services[J].IEEE Transactions on Systems,Man and Cybernetics:PartASystem and Humans,2011,41(3):510-521.

[7]Schmidt D C.Guest editor’s introduction:model-driven engineering[J].IEEE Computer,2006,39(2):25-31.

[8]ATLAS Team.ATLAS transformation language(ATL)home page[EB/OL].(2017).http://www.eclipse.org/atl/atlTransformations/.

[9]Ferrara A.Web services:a process algebra approach[C]//Proceedings of the 2nd International Conference on Service Oriented Computing,New York,Nov 15-19,2004.New York:ACM,2004:242-251.

[10]Xiao Fangxiong,Huang Zhiqiu,Cao Zining,et al.Unified formal modeling and analyzing both functionality and QoS of Web services composition[J].Journal of Software,2011,22(11):2698-2715.

[11]Brogi A,Canal C,Pimentel E,et al.Formalizing Web service choreographies[J].Electronic Notes in Theoretical Computer Science,2004,105:73-94.

[12]Kazhamiakin R,Pistore M.Choreography conformance analysis:asynchronous communications and information alignment[C]//LNCS 4184:Proceedings of the 3rd International Workshop on Web Services and Formal Methods,Vienna,Sep 8-9,2006.Berlin,Heidelberg:Springer,2006:227-241.

[13]Fu Xiang,Bultan T,Su Jianwen.Analysis of interacting BPEL Web services[C]//Proceedings of the 13th International Conference on World Wide Web,New York,May 17-20,2004.New York:ACM,2004:621-630.

[14]Fu Xiang,Bultan T,Su Jianwen.Synchronizability of conversations among Web services[J].IEEE Transactions on Software Engineering,2005,31(12):1042-1055.

[15]Paci F,Ouzzani M,Mecella M.Verification of access control requirements in Web services choreography[C]//Proceedings of the 2008 International Conference on Services Computing,Honolulu,Jul 8-11,2008.Washington:IEEE Computer Society,2008:5-12.

[16]Ponge J,Benatallah B,Casati F,et al.Analysis and applications of timed service protocols[J].ACM Transactions on Software Engineering and Methodology,2010,19(4):1-38.

[17]Wu Hongyue,Du Yuyue.A logical Petri net-based approach for Web service cluster composition[J].Chinese Journal of Computers,2015,38(1):204-218.

[18]Gu Jun,Luo Junzhou,Cao Jiuxin,et al.Performance modeling and analysis of service systems using queueing Petri nets[J].Chinese Journal of Computers,2011,34(12):2435-2455.

[19]He Yanxiang,Shen Hua.A stochastic Petri net-based performance bottleneck location strategy for Web services composition[J].Chinese Journal of Computers,2013,36(10):1953-1966.

[20]Tan Wei,Fan Yushun,Zhou Mengchu.A Petri net-based method for compatibility analysis and composition of Web services in business process execution language[J].IEEE Transactions on Automation Science and Engineering,2009,6(1):94-106.

附中文參考文獻：

[10]肖芳雄,黃志球,曹子寧,等.Web服務組合功能與QoS的形式化統一建模和分析[J].軟件學報,2011,22(11):2698-2715.

[17]吳洪越,杜玉越.一種基于邏輯Petri網的Web服務簇組合方法[J].計算機學報,2015,38(1):204-218.

[18]顧軍,羅軍舟,曹玖新,等.基于排隊Petri網的服務系統性能建模與分析方法[J].計算機學報,2011,34(12):2435-2455.

[19]何炎祥,沈華.一種基于隨機Petri網的Web服務組合性能瓶頸定位策略[J].計算機學報,2013,36(10):1953-1966.