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

祝 義，黃志球，周 航

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

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

1 引言

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

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

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

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

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

本文組織結構如下：第2章提出了基于CSPM的BPEL模型建模與驗證框架；第3章給出了CSPM的進程代數(shù)定義；第4章詳細描述了BPEL到CSPM的映射方法；第5章以一個在線購物系統(tǒng)為例，討論了本文方法的使用效果；第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的映射機制，實現(xiàn)BPEL模型到CSPM模型的轉換；第2步將轉換得到的CSPM模型輸入到模型檢測工具FDR，保存為擴展名為.csp的模型文件，即實現(xiàn)（implementation），為進一步模型檢測做好準備；第3步根據(jù)要檢查的BPEL模型性質建立CSPM斷言，即規(guī)約（specification），例如安全性、活性、確定性和無死鎖性斷言；第4步將CSPM斷言逐個輸入到FDR進行模型檢測，如果正確，就表明該斷言通過模型檢測，如果錯誤，F(xiàn)DR則輸出反例，反例通過比較規(guī)約行為跡與實現(xiàn)行為跡來找出進程中的錯誤；第5步根據(jù)反例對CSPM模型（實現(xiàn)）進行修改，并重新輸入到FDR中進行模型檢測，如此循環(huán)，直至所有CSPM斷言（規(guī)約）都驗證通過；第6步根據(jù)模型檢測結果對BPEL模型進行修改，得到可信BPEL模型。

3 CSPM的進程代數(shù)定義

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

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

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

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

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

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

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

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

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

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

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

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

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

為了驗證BPEL模型的相關性質，首先要建立BPEL語言到CSPM語言的映射機制，實現(xiàn)BPEL模型到CSPM模型的轉換。在WS-BPEL2.0規(guī)約中，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活動主要用來獲取伙伴服務所提供的功能，它通過操作向伙伴服務發(fā)送服務調用消息。invoke活動分為單向調用和請求回復調用兩種類型。單向invoke活動只向伙伴服務發(fā)送服務調用請求，而不需回復，但是請求回復調用除了發(fā)送請求外同時還需回復。單向invoke活動的映射過程是將發(fā)送的請求對應到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活動主要是用戶接受伙伴服務的消息調用。它的映射規(guī)則是，將receive活動接受的消息對應到CSP的一個輸入動作。具體映射關系如圖4所示。

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

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

（3）reply活動

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

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

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

4.2 組合活動映射

（1）sequence活動

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

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

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

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

（2）switch活動

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

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

switch活動在CSPM中可表示為：

（3）while活動

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

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

while活動在CSPM中表示為：

（4）pick活動

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

pick活動在CSPM中表示為：

（5）flow活動

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

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

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

flow活動在CSPM中表示為：

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

5 實例

一個在線購物（online shopping）應用共涉及顧客（Buyer）、售貨商（Seller）、銀行（Banker）、郵局（Postoffice）和快遞公司（Shipper）5個協(xié)作服務。交易之初，Buyer向Seller發(fā)送訂單請求消息（ordreq），Seller接收到ordreq后，向Banker發(fā)送貨款支付請求消息（payreq），如果Buyer的銀行卡可用額度能夠支付所定貨物，則Banker向Seller返回支付成功消息（payok），否則返回支付失敗消息（payfail）。當Seller收到payok，則選擇Postoffice或者Shipper向Buyer發(fā)送貨物（postreq/shipreq），貨物發(fā)送完成后（postend/shipend），Seller再通知Buyer貨物運送完成(postsucc/shipsucc）。如果Buyer的銀行卡可用額度不能支付所定貨物，則Seller拒絕Buyer的本次訂單（rejection）。在線購物為了完成共同的業(yè)務目標，它們共享數(shù)據(jù)，通過發(fā)送和接收消息向合作伙伴請求并提供服務。通過以上分析，首先通過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失效/發(fā)散精化于進程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 在線購物系統(tǒng)安全性檢測結果

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

該斷言表示進程BS、BSB、BSBS、BSBP、OS都不會發(fā)散，不會出現(xiàn)任何既可接受又可拒絕的行為選擇。例如對于進程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模型檢測，表明在線購物系統(tǒng)CSPM模型具有極高的可靠性。接下來根據(jù)模型檢測結果對BPEL模型進行修改，最后可以得到高可信的BPEL模型。

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

（1）單個行為的正確性

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

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

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

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

（2）組合行為的正確性

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

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

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

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

6 相關工作比較

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

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

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

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

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

7 總結與展望

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

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

[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的形式化統(tǒng)一建模和分析[J].軟件學報,2011,22(11):2698-2715.

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

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

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