基于接口自動機的ＢＰＥＬ４ＷＳ Ｗｅｂ服務組合形式化模型
2009-01-01 00:00:00蘇煥程黃志球劉林源
計算機應用研究 2009年5期
（南京航空航天大學 信息科學與技術學院 南京 210016）
摘 要：介紹了接口自動機的基本語法，針對目前最主要的一種描述和執行基于工作流模式的Web服務組合的規范——Web服務商業流程執行語言 (business process execution language for Web services，BPEL4WS)，定義了接口自動機和BPEL4WS之間的概念映射，并給出了BPEL4WS的基于接口自動機的形式化模型，最后通過一個案例給出了BPEL4WS到接口自動機的映射及驗證的方法。
關鍵詞：接口自動機; Web服務; Web服務組合; Web服務商業流程執行語言
中圖分類號：TP311 文獻標志碼：A
文章編號：1001-3695(2009)05-1774-04
Interface automatabased formal model for BPEL4WS Web service composition
SU Huan-cheng HUANG Zhi-qiu LIU Lin-yuan
（College of Information Science Technology Nanjing University of Aeronautics Astronautics Nanjing 210016，China）
Abstract:This paper introduced basic syntax of interface automata. For the most important kind of specification of specifying and executing workflowbased Web service compositionbusiness process execution language for Web services(BPEL4WS) defined the conception mapping between interface automata and BPEL4WS and presented a interface automatabased formal model for BPEL4WS. Introduced the model verification method through a case study.
Key words：interface automata; Web service; Web service composition; BPEL4WS
0 引言
面向服務的計算(service oriented computing，SOC)[1]是一種新的分布式計算和電子商務模式。在這種計算模式中，自治、異構的服務是基本的計算單元，顯然Web服務技術能夠很好地適應和支持SOC。關于Web服務的研究包括很多令人感興趣的問題，如服務組合、服務同步、服務協作和服務驗證。Web服務組合是指：一個客戶或客戶代理的請求不能由單個 Web服務來滿足，而是由一些 Web服務的組合來完成。這些被組合的子Web服務會彼此并發地交互以完成客戶的請求，而彼此間的交互是通過通信和交換信息來完成。因此Web服務組合涉及到的問題包括被組合的服務間的并發、同步、通信。
目前有很多研究者利用各種形式化的工具來建模、驗證 Web服務組合以保證Web服務組合的正確性。主要的模型有通信順序進程[2](communicating sequential processes，CSP)、通信系統演算[3](calculus of communicating systems，CCS)、Pi演算[4]、Petri網等。Web服務流語言[5](Web services flow language，WSFL)是從工作流語言發展而來的基于網的語言，它可以被看成是著色 Petri網。Hamadi[6]提出了一種基于Petri網的代數來組合Web服務。通過將每個服務組合操作映射到Petri網的構造元素，每個Web服務組合操作的形式化語義可以被Petri網來表達。因而，任何一個用基于Petri網的代數來表達的服務均可以被翻譯成Petri網的表示形式。Brogi等人[7]提出了一個基于CCS的Web服務編排接口[8](Web service choreography interface，WSCI)的形式化模型。Salatin等人[9]提出了一個利用 CCS對BPEL4WS建模和推理的通用框架。Camara等人[10]利用CCS對 BPEL4WS建模，并且利用形式化模型來分析Web服務行為的兼容性和可替換性。Foster等人[11]將BPEL4WS所描述的商業流程翻譯成FSP(finite state process)，并且利用 LtTSA(labeled transition system analyzer)工具對 FSP進程進行模型檢查。
接口自動機是Alfaro等人提出的一種描述接口的理論[12]。與已有的各種方法不同，接口自動機描述了組件接口的時序性，即接口交互活動間的先后順序關系。接口自動機雖然基于傳統的自動機，但它將接口的輸出保證和輸入假設整合在一起，納入到該形式化系統中加以處理。輸出保證反映了本接口請求的各外部服務間的先后順序關系——相當于對環境所作的假設；輸入假設反映了本接口對外提供的各服務的先后順序關系——相當于自身行為的一種描述。此外，接口自動機還引入博弈思想來處理接口與環境的一種描述，即判別接口兼容性的新方法——樂觀方法。它與傳統的悲觀方法不同，認為只要存在一個可保證組合后的接口能在其中正確運行的環境，那么原接口解釋兼容的。同時，采用了樂觀方法來處理接口組合的問題，使得組合后的接口狀態大幅度減少，因而接口自動機又是一種輕量級的形式化模型。這也是接口自動機優于那些悲觀方法的形式化工具的所在。作為一個事實上的工業標準，BPEL4WS[13]成為了基于工作流模式的Web服務組合的重要規范。從技術上講，BPEL4WS缺乏一個形式化的模型來對組合的Web服務進行模型檢查和驗證。因此，本文提出了一個基于接口自動機的BPEL4WS的形式化模型，在該模型中，對BPEL4WS中用于描述一個商業流程的基本構造元素活動(activity)進行了形式化描述。與上述的工作相比，本文將BPEL4WS中主要元素映射到接口自動機有著獨特的優點:a)它將服務對環境的依賴考慮到了模型中而不用再單獨考慮環境的約束；b)接口自動機所采用的樂觀方法來處理服務組合問題，使得組合后的接口狀態大幅度減少；c)已有大量的基于接口自動機模型驗證的研究成果。
1 接口自動機的介紹
由于篇幅的限制，本章只簡單地介紹接口自動機及的基本概念，詳細內容可參考文獻[12]。
定義1 接口自動機是一個六元組P=〈VP，VinitP，AIP，AOP，AHP，ΓP〉。其中：VP表示狀態集，每一個狀態為vi(0≤i≤|VP|)；VinitP∈VP表示初始狀態集，VinitP至多包含一個狀態vinitP；如果VinitP為空集，則自動機P為空；AIP、AOP、AHP分別表示輸入﹑輸出和內部動作集，三者交集為空；當動作a∈AIP AOP或AHP時，相應的轉換(v，a，v′)分別稱為輸入﹑輸出或中間轉換；ΓP∈VP×AP×VP表示所有的轉換的集合；P的所有動作集表示為AP=AIP∪AOP∪AHP。對于某一狀態v∈VP，當存在轉換(v，a，v′)∈ΓP，v′∈VP時，稱動作a∈AP，都有AIP=AIP(v)。對于一個接口自動機P=〈VP，VinitP，AIP，AOP，AHP，ΓP〉，狀態轉換序列v0a0v1a1…an-1vnanvn+1是P的一個行為當且僅當v0∈VinitP且對每一個i(0≤i≤n)，有(vi，ai，vi+1)∈ΓP。
定義2 接口自動機P的一個執行片段是其狀態與活動交替排列的有限序列: v0a0v1a1…vn。其中 (vi，ai，vi+1)∈ΓP，0≤i≤n。任給兩個狀態v，u∈VP，若存在一個執行片段，其第一個狀態為v且最后一個狀態為u，則稱u從v可達。若u從某個初始狀態v∈Vinitρ可達，則稱v在P中是可達的。
定義3 兩個接口自動機P和Q若滿足如下條件則稱它們是可組合的：
AHP∩AQ=，AIP∩AIQ=
AQP∩AOQ=，AHQ∩AP=
兩個接口自動機是可組合的要滿足兩個條件：a)它們不能有相同的輸入或輸出活動;b)其中一方的內部活動不能與另一方的任何活動相同。
定義4 如果P與Q是兩個可組合的接口自動機，則它們組合后的接口自動機PQ定義如下：
VPQ=VP×VQ，VinitPQ=VinitP×VinitQ
AIPQ=(AIP∪AIQ)\\shared(P，Q)
AOPQ=(AOP∪AOQ)\\shared(P，Q)
AHPQ=(AHP∪AHQ)\\shared(P，Q)
2 基于接口自動機的BPEL4WS形式化描述
BPEL4WS作為一種描述和執行 Web服務組合工作流的語言，已經成為事實上的標準。BPEL4WS主要包括基元活動(basic activity)及結構活動(structured activity)兩類的基本元素。下面對BPEL4WS中定義的基元活動及結構活動分別給出基于接口自動機的形式化模型。為了便于表達，在給出每個行為的BPEL4WS定義時，只列出一些主要屬性和子元素，其他屬性和子元素均省略。
由于BPEL4WS的結構活動包括了不同的基元活動或結構活動，無法直接根據結構活動定義出相應的接口自動機的元素。針對這一問題，首先定義出IA函數：
定義5 函數IA(X)表示由參數X確定的接口自動機。其中參數X是BPEL4WS的基元活動或結構活動。
例如：IA(empty)=〈{a}，，，，，〉。
2.1 BPEL4WS基元活動到接口自動機的映射
基元活動是與外界進行交互最簡單的形式。它們是無序的個別步驟，與服務進行交互﹑操作﹑傳輸數據或處理異常等。BPEL4WS的基元活動包括如下:
a)Assign基元活動。可以將數據從一個變量復制到另一個變量，也可以使用表達式來構造和插入新數據。在接口自動機中assign活動被構造為一個節點向另一個節點發送所要賦值的數據變量。其中發送節點可以定義為初始節點(非必須)，assign被定義為接口自動機的內部動作。映射規則如下：
〈assign name =″assignmsg″〉
〈copy 〉fromspec
〈/copy 〉tospec
〈/assign〉
映射為
IA(assign)=〈{a，b}，，，，{assignmsg}，{(a，assignmasg，b)}〉
b)Empty基元活動。該活動不會執行任何動作，是個空活動，目的是為了結構的完整性。在接口自動機中empty活動被構造為一個單獨的狀態節點。
〈empty name =″x″〉
……
〈/empty〉
映射為
IA(empty)=〈{a}，，，，，〉
c)Receive基元活動。該活動主要用于(接收請求)等待客戶端通過發送消息調用業務流程。在接口自動機中receive活動被構造為一個輸入動作。映射規則如下：
〈receive operation=″op″variable=″opmsg″〉
……
〈/receive〉
映射為
IA(receive)=〈，，{opmsg}，，，〉
d)Reply基元活動。該活動被用來發送對先前通過receive活動被接收的請求響應。在接口自動機中receive活動被構造為一個輸出動作。映射規則如下：
〈reply operation=″op″ variable=″opmsg″〉
……
〈/reply〉
映射為
IA(reply)=〈，，，{opmsg}，，〉
e)Invoke基元活動。該活動主要用于調用其他Web服務。映射規則如下：
〈invoke operation=″op″
inputVariable=″inputmsg″
outputVariable=″outputmsg″〉
〈\\invoke〉
映射為
IA(invoke)=〈，，{inputmsg}，{outputmsg}，，〉
f)Throw基元活動。當業務流程需要顯示地發出故障信號時可以使用throw活動。在接口自動機中throw活動被構造為一個輸出動作。映射規則如下：
〈throw faultName=″faultmsg″ faultVariable=″faultmsg″ 〉
……
〈/throw〉
映射為
IA(throw)=〈{a，b}，，，，{opmsg}，{(a faultmsg b)}〉
g)Wait基元活動。該活動使流程能夠等待一段特定的時間間隔，或一直等到某個截止期限為止。由于在接口自動機中并不支持時間的特性，本文忽略BPEL4WS中的wait活動。在文獻[14]中對接口自動機的輸入/輸出活動增加了時間約束，提出了時間接口自動機。在未來的工作中，通過時間接口自動機對BPEL4WS建模時再考慮wait活動。其中IA(wait)=〈，，，，，〉。
h)Terminate基元活動。該活動用于終止整個流程。由于接口自動機中流程的結束就是一個接口自動機中執行片段的結束，不用專門為terminate活動構造相應的接口自動機的元素，即IA(terminate)=〈，，，，，〉。
i)Compensate基元活動。該活動被用來在已正常執行的內層作用域上調用補償。Compensate活動并不影響BPEL4WS流程的邏輯關系，所以也不用專門為compensate活動構造相應的接口自動機的元素，即IA(compensate)=〈，，，，，〉。
2.2 BPEL4WS結構活動到接口自動機的映射
結構化活動規定了一組活動發生的順序。它們描述了業務流程是怎樣通過把它執行的基元活動組成結構而被創建的，這些結構表達了涉及業務協議的流程實例間的控制形式﹑數據流程﹑故障和外部事件的處理以及消息交換的協調。BPEL4WS的結構化的活動如下:
a)Sequence結構活動。一個sequence活動包含一個或多個按順序執行的活動，執行順序是這些活動在sequence元素中被列出的先后順序。當sequence中的最后一個活動完成后，該sequence活動也就完成了。Sequence活動到接口自動機的映射規則如下：
〈sequence〉
activity1
activity2
〈/sequence〉
映射為
IA(sequence)=IA(activity1)
IA(activity2)〈{a，b}，，，，，〉
b)Switch結構活動。該活動是以各種不同形式的條件行為組成的結構化活動，即switch活動中可以根據不同的行為分成幾個活動分支。Switch活動到接口自動機的映射規則如下：
〈switch〉
〈case condition=″ ″〉 activity1〈/case〉
〈case condition=″ ″〉 activity2〈/case〉
〈/ switch〉
映射為
IA(switch)=IA(activity1)IA(activity2)〈{a，b，c}，，，，，〉
c)While結構活動。該活動支持指定活動的反復執行，直到給出的布爾條件不再被滿足。在工作流邏輯層只關心任務的依賴關系，不關心具體操作內容，所以判斷while活動執行的條件不是邏輯層需要考慮的內容。將while活動作為一個基本活動來考慮，其映射與基本活動一樣。While活動到接口自動機的映射規則如下：
〈whileCondition=″bool″〉
activity
〈/ while〉
映射為
IA(while)=IA(activity)IA(bool)
〈{a，b}，，，，，〉
d)Pick結構活動。該活動等待一組事件中的一個發生，然后執行與發生的事件關聯的活動。其形式是一組形式為事件與活動的分支且僅有一個分支被選擇，所選的分支與最先發生的事件關聯，當該分支的活動完成后，pick活動就完成了。Pick活動到接口自動機的映射規則如下：
〈pick〉
〈onMessage operation=″op1″ Variable=″op1msg″〉activity1
〈/onMessage〉
〈onMessage operation=″op2″ Variable=″op2msg″〉activity2
〈/onMessage〉
〈onMessage operation=″op3″ Variable=″op3msg″〉activity3
〈/onMessage〉
〈 /pick〉
映射為
IA(Pick)=IA(activity1)IA(activity2)IA(activity3)
〈a，b，c，d，e}，，，，{opmsg，op2msg，op3msg}，〉
e)Flow結構活動。該活動主要用于定義一組將并行調用的活動。Flow活動到接口自動機的映射規則如下：
〈flow〉
activity1
activity2
〈/ flow〉
映射為
IA(flow)=IA(activity1)IA(activity2)
〈{a，b，c，d}，，，，，〉
3 基于接口自動機的BPEL4WS服務組合模型的建模及驗證
3.1 實例分析
下面以一個雇員出差訂票業務過程為例給出用接口自動機對Web服務組合的建模方法。
一個典型的雇員出差訂票Web服務組合業務流程EmployeeOrder如下：客戶customer發出一個出差雇員的ID號，雇員出差狀態Web服務infoWS收到雇員ID號之后查詢該雇員的出差待遇是火車還是飛機然后將結果返回;客戶根據返回的結果向訂票Web服務系統orderWS訂票。這個組合的業務流程如圖 1所示。
由于篇幅原因這里不列出詳細的雇員出差訂票業務過程的BPEL4WS描述。下面給出雇員出差訂票業務過程BPEL4WS描述映射后的接口自動機。其模型如圖2所示。
根據BPEL4WS到接口自動機的映射規則，在雇員出差訂票Web服務組合業務流程的BPEL4WS映射后的接口自動機模型：
IA(Employeed Order)=〈VP，VinitP，AIP，AOP，AHP，ΓP〉
其中：VinitP={a}，VP={b，c，d，e};AIP={plane，train}， AOP={ID order} AHP={ticket} ;ΓP={(a，ID!，b)，(b，plane?，c)，…}。
3.2 基于接口自動機的模型驗證
Web服務組合模型的驗證是為了保證那些并發的子服務相互之間的正確性。驗證的內容主要包括模型的正確性，如是否存在死鎖、消息是否會丟失、是否有不可達的狀態？
在文獻[12]中已經對上述問題進行了研究，并給出了逆向可達算法，可以構造出只包含兼容組合狀態的IAN，即COMP(N)。在COMP(N)的狀態集中不再包含上述的非法狀態和那些從初始狀態不可達的狀態。針對Web服務組合模型的驗證，將需要驗證的Web服務組合的BPEL4WS映射為接口自動機模型然后通過逆向可達算法檢查出所有的非法狀態及不可達的狀態。
模型檢查另一個重要內容是驗證所設計的組合服務是否確實符合客戶要求。例如，在一個功能復雜的BPEL4WS業務過程中需驗證某一個客戶要求的功能是否能夠完成，以及某一個客戶要求的功能是否能保證在另一個功能完成前結束等。
文獻[15]將客戶需求通過UML時序圖進行建模，再結合接口自動機對功能需求與模型之間的一致性進行了驗證，并給出了相應的算法。在Web服務組合模型的驗證中，筆者將BPEL4WS映射為接口自動機，而將需要驗證的所有功能通過UML時序圖建模，按照文獻[15]的算法對BPEL4WS于功能的一致性進行檢查。
4 結束語
一個組合的Web服務由一組子Web服務組合。這些被組合的子Web服務會彼此地交互以完成客戶的請求，而彼此間的交互是通過通信和交換信息來完成。Web服務組合中一個很重要的問題是如何保證組合的正確性。解決這個問題的重要手段就是為Web服務組合提供一個形式化的模型以進行模型檢查和驗證。而接口自動機是一種特別適合于描述BPEL4WS的形式化工具。
本文利用接口自動機對Web服務組合建立形式化模型，對目前最為重要的Web服務組合規范BPEL4WS定義了接口自動機到BPEL4WS的概念映射，給出了基于接口自動機的形式化描述，并且通過案例分析給出了模型的建模及驗證方法。
將來的研究工作包括：如何通過時間接口自動機對BPEL4WS中的時間因素進行約束來處理Web服務組合中的時間因素和事務；如何設計出一個原型系統完成BPEL4WS到接口自動機的自動映射。
參考文獻：
[1]HUHNS M N，SINGH M P. Serviceoriented computing: key concepts and principles[J]. IEEE Internet Computing，2005，9（1）:75-81.
[2]HOARE C A R. Communicating sequential processes[M]. New York: Prentice Hall 2004.
[3]MILNER R. Communication and concurrency[M]. New York: Prentice Hall 1989.
[4]MILNER R. Communicating and mobile systems: the picalculus[M].Cambridge:Cambridge University Press，1999.
[5]LEYMANN F.Web services flow language[EB/OL]. (2005-10-20). http://www.ibm.com/software/solutions/Webservices/pdf/WSFL.pdf.
[6]HAMADL R BENATALLAH B. A Petri netbased model for Web service composition[C]//Proc of the 14th Australasian Database Conference on Database Technologies. 2003.
[7]BROGI A，CANAL C，PIMENTEL E，et al. Formalizing Web service choreographies[J]. Electronic Notes in Theoretical Computer Science 2004 105:73-94.
[8]ARKIN A ASKARY S FORDIN S et al. Web service choreography interface(WSCI)1.0[EB/OL].(2006-03-10).http://www.w3.org/TR/wsci.
[9]SALATIN G BORDEAUX L，SCHAERF M. Describing and reasoning on Web services using process algebra[C]//Proc of IEEE International Conference on Web Services (ICWS’04). 2004.
[10]CAMARA J，CANAL C，CUBO J.Issues in the formalization of Web service orchestrations[C]//Proc of the 12th International Workshop on Coordination and Adaptation Techniques for Software Entities(WCAT’05). 2005.
[11]FOSTER H，UCHITEL S，MAGEE J，et al.Modelbased verification of Web service compositions[C]//Proc of the 18th IEEE International Conference on Automated Software Engineering. 2003.
[12]DeALFARO L，HENZINGER T A. Interface automata[C]//Proc of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering. Vienna，Austria:[s.n.] 2001:109120.
[13]ANDREWS T CUBERA F DHOLOAKKIA H et al. Business process execution language for Web services version1.1[EB/OL]. http://www.ibm.com/developerworks/library/specification/wsbpel/.
[14]DeALFARO L，HENZINGER T A STOELINGA M. Timed interfaces[C]//Proc of the 2nd International Conference on Embedded Software(EMSOFT 2002).Berlin:SpringerVerlag，2002:108122.
[15]胡軍，于笑豐，張巖，等.基于場景規約的構件式系統設計分析與驗證[J].計算機學報，2006，29(4):513525.
