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

祝 義，黃志球，周 航

1.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 210016

2.江蘇師范大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 徐州 221116

1 引言

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

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

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

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

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

本文組織結(jié)構(gòu)如下：第2章提出了基于CSPM的BPEL模型建模與驗(yàn)證框架；第3章給出了CSPM的進(jìn)程代數(shù)定義；第4章詳細(xì)描述了BPEL到CSPM的映射方法；第5章以一個(gè)在線購物系統(tǒng)為例，討論了本文方法的使用效果；第6章進(jìn)行相關(guān)工作比較；第7章總結(jié)全文并給出結(jié)論。

2 基于CSPM的BPEL模型建模與驗(yàn)證框架

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

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

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

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

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

定義1（通信順序進(jìn)程）一個(gè)通信順序進(jìn)程CSP可定義為：

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

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

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

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

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

P＜expr＞Q：條件復(fù)合，表示expr表達(dá)式為真時(shí)執(zhí)行進(jìn)程P，否則執(zhí)行進(jìn)程Q；

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

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

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

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

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

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

4.1 基本活動(dòng)映射

（1）invoke活動(dòng)

invoke活動(dòng)主要用來獲取伙伴服務(wù)所提供的功能，它通過操作向伙伴服務(wù)發(fā)送服務(wù)調(diào)用消息。invoke活動(dòng)分為單向調(diào)用和請(qǐng)求回復(fù)調(diào)用兩種類型。單向invoke活動(dòng)只向伙伴服務(wù)發(fā)送服務(wù)調(diào)用請(qǐng)求，而不需回復(fù)，但是請(qǐng)求回復(fù)調(diào)用除了發(fā)送請(qǐng)求外同時(shí)還需回復(fù)。單向invoke活動(dòng)的映射過程是將發(fā)送的請(qǐng)求對(duì)應(yīng)到CSP的一個(gè)輸出動(dòng)作。具體映射關(guān)系如圖2所示。

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

對(duì)于請(qǐng)求回復(fù)invoke活動(dòng)，將請(qǐng)求和回復(fù)消息分別對(duì)應(yīng)到CSP的輸出和輸入活動(dòng)，具體映射關(guān)系如圖3所示。

Fig.3 Mapping from action request-replyinvoketo CSP圖3 請(qǐng)求回復(fù)invoke活動(dòng)到CSP的映射

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

（2）receive活動(dòng)

receive活動(dòng)主要是用戶接受伙伴服務(wù)的消息調(diào)用。它的映射規(guī)則是，將receive活動(dòng)接受的消息對(duì)應(yīng)到CSP的一個(gè)輸入動(dòng)作。具體映射關(guān)系如圖4所示。

Fig.4 Mapping from actionreceiveto CSP圖4 receive活動(dòng)到CSP的映射

receive活動(dòng)在CSPM中表示為op?message?P。

（3）reply活動(dòng)

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

Fig.5 Mapping from actionreplyto CSP圖5 reply活動(dòng)到CSP的映射

reply活動(dòng)在CSPM中表示為op!message?P。

4.2 組合活動(dòng)映射

（1）sequence活動(dòng)

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

當(dāng)αP={act}時(shí)，即子活動(dòng)為原子活動(dòng)時(shí)，上述進(jìn)程表達(dá)式簡(jiǎn)化為：

Fig.6 Mapping from actionsequenceto CSP圖6 sequence活動(dòng)到CSP的映射

sequence活動(dòng)在CSPM中可表示如下：

（2）switch活動(dòng)

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

Fig.7 Mapping from actionswitchto CSP圖7 switch活動(dòng)到CSP的映射

switch活動(dòng)在CSPM中可表示為：

（3）while活動(dòng)

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

Fig.8 Mapping from actionwhileto CSP圖8 while活動(dòng)到CSP的映射

while活動(dòng)在CSPM中表示為：

（4）pick活動(dòng)

pick活動(dòng)包含若干個(gè)onMessage元素，它等待特定的消息到達(dá)，當(dāng)最先收到某個(gè)消息時(shí)，就觸發(fā)該消息對(duì)應(yīng)的活動(dòng)，當(dāng)該活動(dòng)執(zhí)行完畢后，pick活動(dòng)結(jié)束。pick活動(dòng)的轉(zhuǎn)換過程是，首先將觸發(fā)每個(gè)活動(dòng)所對(duì)應(yīng)的消息看作一個(gè)receive活動(dòng)，然后再將它們?nèi)诤铣梢粋€(gè)順序執(zhí)行活動(dòng)。最后將各順序活動(dòng)融合成一個(gè)分支選擇活動(dòng)。具體映射關(guān)系如圖9所示。

pick活動(dòng)在CSPM中表示為：

（5）flow活動(dòng)

Fig.9 Mapping from actionpickto CSP圖9 pick活動(dòng)到CSP的映射

Fig.10 Mapping from actionflowto CSP圖10 flow活動(dòng)到CSP的映射

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

flow活動(dòng)在CSPM中表示為：

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

5 實(shí)例

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

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

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

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

（1）安全性

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

（2）活性

該斷言表示進(jìn)程BS、BSB、BSBS、BSBP失效/發(fā)散精化于進(jìn)程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)。模型檢測(cè)結(jié)果如圖13所示。

（3）確定性

Fig.12 Safety checking of online shopping圖12 在線購物系統(tǒng)安全性檢測(cè)結(jié)果

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

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

（4）無死鎖性

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

以上實(shí)驗(yàn)結(jié)果顯示所有進(jìn)程都通過了FDR模型檢測(cè)，表明在線購物系統(tǒng)CSPM模型具有極高的可靠性。接下來根據(jù)模型檢測(cè)結(jié)果對(duì)BPEL模型進(jìn)行修改，最后可以得到高可信的BPEL模型。

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

（1）單個(gè)行為的正確性

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

在FDR中對(duì)SELLER進(jìn)程進(jìn)行相應(yīng)的修改：

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

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

（2）組合行為的正確性

假設(shè)Shipper或者Postoffice是并行關(guān)系。在FDR中對(duì)OS進(jìn)程修改如下：

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

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

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

6 相關(guān)工作比較

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

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

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

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

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

7 總結(jié)與展望

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

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

[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.

附中文參考文獻(xiàn)：

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

[17]吳洪越,杜玉越.一種基于邏輯Petri網(wǎng)的Web服務(wù)簇組合方法[J].計(jì)算機(jī)學(xué)報(bào),2015,38(1):204-218.

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

[19]何炎祥,沈華.一種基于隨機(jī)Petri網(wǎng)的Web服務(wù)組合性能瓶頸定位策略[J].計(jì)算機(jī)學(xué)報(bào),2013,36(10):1953-1966.