袁曉月，萬珍珍，馮 星

(江西省科學(xué)院應(yīng)用物理研究所，330029，南昌市)

基于進程代數(shù)WS-CDL交互模式建模研究

袁曉月，萬珍珍，馮 星

(江西省科學(xué)院應(yīng)用物理研究所，330029，南昌市)

基于WS-CDL的編排是從全局視角描述Web服務(wù)交互功能，但其缺乏形式化語義?；谶M程代數(shù)提出了PA4WS(Process Algebra for WS-CDL)來描述WS-CDL的形式化語法和語義。相比其他相關(guān)工作，PA4WS給出了WS-CDL編排的工作單元建模、基于信息對齊交互模式和異步交互建模。最后，通過一個例子給出了PA4WS帶來的好處。

WS-CDL；進程代數(shù)；形式化方法

0 引言

面向服務(wù)的計算(Service-Oriented Computing -SOC)是今后的主要計算模式，其主要實現(xiàn)形態(tài)是Web服務(wù)。而Web服務(wù)的復(fù)合則是關(guān)鍵問題[1-4]?，F(xiàn)在主要有服務(wù)編制(Orchestration)和服務(wù)編排(Choreography)兩大類2種Web服務(wù)復(fù)合方法，第1種方法是由WS-BPEL標準實現(xiàn)的Web服務(wù)編制，它由服務(wù)編制需要一個總控流程來控制涉及到的Web服務(wù)，并協(xié)調(diào)Web服務(wù)不同操作的執(zhí)行。第2種是由WS-CDL標準實現(xiàn)的Web服務(wù)編排，服務(wù)編排并不依賴中央的總控協(xié)調(diào)過程。相反，每個涉及其中的Web服務(wù)都知道何時執(zhí)行自己的操作，和誰交互。這2種方法在Web服務(wù)交互方面僅有幾個相同的模式，Web服務(wù)交互模式描述了多個Web服務(wù)間的通訊方法。就是說，一種Web服務(wù)交互模式描述了在一個特定上下文中發(fā)生的問題對應(yīng)的解決方案集，這些方案已經(jīng)被驗證是正確的。本文描述了Web服務(wù)編排中的工作單元和基于信息對齊的交互(Interaction Based Information Alignment-IBIA)的模式，并給出了這些模式應(yīng)用的場景。

Web服務(wù)交互模式主要關(guān)注下列幾方面：1)參與者或角色，即Web服務(wù)交互由哪些參與者；2)工作流次序，即消息發(fā)送或接收的次序是什么。

基于進程代數(shù)，本文給出一個稱為PA4WS(Process Algebra for WS-CDL)的代數(shù)系統(tǒng)，來對Web服務(wù)編排中的交互進行建模。相比Carbone等人的工作[5]，PA4WS除了具有會話建模，還對WS-CDL中的工作單元建模。工作單元在WS-CDL是模塊復(fù)合的重要元素，其首次在形式化模型中建立原語。需要注意WS-CDL描述的交互活動具有非對稱特性，它偏向接收方而非發(fā)送方[8]。

1 WS-CDL簡介

WS-CDL模型是為達到一個共同的目標，多個服務(wù)間的協(xié)作的描述?；谖墨I[6]，圖1給出了WS-CDL核心層的結(jié)構(gòu)。

圖1 WS-CDL核心結(jié)構(gòu)

WS-CDL模型中，交互活動是編排最基礎(chǔ)的構(gòu)件塊。通過交互可以實現(xiàn)多個參與者間的通訊，這樣可以使它們實現(xiàn)動作同步。多個動作通過封裝成為一個動作模塊，再通過順序、并行和分支的復(fù)合變成更大的模塊，這樣可以實現(xiàn)從簡單動作到復(fù)雜動作的擴展。WS-CDL中的工作單元(WorkUnit)就是這樣一個封裝多個動作的模塊。它體現(xiàn)了動作塊的可重用性，是WS-CDL中非常重要的重用機制。將工作單元考慮到形式化模型中，可以極大提高模型描述能力。

2 相關(guān)工作與討論

文獻[7-10]使用形式化方法討論了Web服務(wù)的交互。文獻[10]基于高層視角對Web服務(wù)模式進行研究，但其不夠精確。A Barros和M Dumas等論證了編排(編制)交互模式中的單(多)向發(fā)送和雙(多)旁通問題，其不足是非形式化方法[11]。A M S Filho和H K E Liesenberg等給出了面向服務(wù)應(yīng)用交互模式的通用但不精確的聚合和處理方法[12]?；谶M程代數(shù)的Web服務(wù)組合研究有重要的影響。R Lucchi和M Mazzara基于π演算描述了BPEL4WS的交互模式[13]。A Bracciali和A Brogi等在文獻[14]采用進程代數(shù)對編制交互模式。文獻[15]基于CCS給出了工作流模式。R Gorrieri和C Guidi等提出WS-CDLcore進程代數(shù)對Web服務(wù)模式建模[16]，其沒有對WS-CDL中的工作單元建模。不同于前述工作，本文在Carbone等人的工作基礎(chǔ)上[5]，提出的PA4WS對Web服務(wù)編制中的工作單元作為原語建模，并給出了基于信息對齊的例子。PA4WS可以在高層對WS-CDL的復(fù)合進行描述、組合和推理。本文給出了WS-CDL交互復(fù)合模式。

3 基于進程代數(shù)的Web服務(wù)編排PA-4WS模型

3.1PA4WS語法

采用符號η表示PA4WS中的有限原子動作集。

定義1：PA4WS語法如下：

η∷=A→Bsop,e,y|x@A:=e

ifx@AthenC1elseC2|while(x@A,C)|0

符號C,C1表示W(wǎng)eb服務(wù)編制，符號+,| 等表示進程復(fù)合操作。下面給出這些符號含義的解釋。表示原子動作的η其3種含義如下。

1)A→B表示在參與者A和B之間建立一個服務(wù)通道，并建立并初始化一個屬于B的會話向量需要注意，包含在內(nèi)的會話通道屬于其所在的服務(wù)通道，就是說從外部不可見。

2)A→Bsop,e,y表示參與者A經(jīng)過會話通道s發(fā)送一個具有操作op的消息給參與者B。僅包含參與者B變量的表達式e值賦給變量y。操作op的觸發(fā)時機是接收者收到從發(fā)射者發(fā)送的消息時。

3)x@A:=e表示和強制式語言相同的賦值語句。其中，x和表達式e中的變量均在參與者A。

PA4WS中的交互含義解釋如下。

1)η.C表示在完成基礎(chǔ)動作η后，再執(zhí)行后面的編制C。基礎(chǔ)動作η如前所述。

2)C1;C2表示執(zhí)行完C1后再執(zhí)行C2的串行復(fù)合。

3)C1|C2表示C1和C2的并行。和傳統(tǒng)的進程代數(shù)并行運算符不同，C1和C2沒有通訊，C1|C2僅表示2個獨立的編制運行。

6)[g,C,rec]表示工作單元原語。其中g(shù)是觸發(fā)條件，rec是循環(huán)條件。當g為真時，編制C開始執(zhí)行，否則編制C不執(zhí)行。如果rec條件為真，則編制C將循環(huán)執(zhí)行，直到rec為假。工作單元也可以表示為[g,C,rec]?ifgthen{C|while(rec,C)}。

7)ifx@AthenC1elseC2是確定性分支原語。當位于A的x為真則執(zhí)行C1，否則執(zhí)行C2。

8)while(x@A,C)是遞歸原語。其中while(x@A,C)=C[while(x@A,C)/x@A]。

9)0表示進程終止。

定義2：PA4WS中的自由名，進程代數(shù)中的自由名是其與外界的接口，其具有重要的作用。PA4WS自由名定義如下：

fn(A→B:sop,e,y)=y,fn(x@A:=e)=fn(e)∪{x@A}

fn(η.C)=fn(η)∪fn(C),fn(C1|C2)=fn(C1)∪fn(C2)

fn(ifx@AthenC1elseC2)=fn(C1)∪fn(C2){x@A}

fn(while(x@A,C))=x@A∪fn(C),fn([g,C,rec])=fn(C)∪rec∪g。

定義3：結(jié)構(gòu)化同余，符號≡表示PA4WS最小同余關(guān)系，其定義如下：C≡C′，當C可以語法變換為C′；(C,|,+,0)是在同余關(guān)系下≡的滿足交換律的獨異點。

3.2PA4WS語義

PA4WS采用小步語義，即PA4WS的計算是基于遷移序列。遷移由通訊、賦值或條件等語句表示。由于參與者有可能有自己的局部變量(使用符號σ表示)，因此，遷移可能涉及參與者的局部變量。符號σ[x@A=v]表示除了參與者A的變量x賦值為v外，其余局部變量保持原狀。

定義4：格局，格局是序偶對(σ,C)，符號C表示編制，σ表示所有參與者局部狀態(tài)集。局部狀態(tài)集σ的變化反應(yīng)了計算過程。若σ′是形如Var×P→Val的函數(shù)，其中P是參與者集合，Val是變量集合。則符號σ@A表示屬于A的狀態(tài)集，符號σ[x@A→v]則表示一個x@A的值為v的新狀態(tài)集。

定義5：歸約關(guān)系，歸約關(guān)系是形如→?(σ,C′)×(σ′,C′)的二元關(guān)系。其是表示格局變換的函數(shù)。即在狀態(tài)σ下的進程C在完成如賦值、交互等計算后，其狀態(tài)變?yōu)棣摇?，進程變?yōu)镃′。

定義6：語義，PA4WS語義如圖2所示。其中符號tt表示常量真，符號ff表示常量假。

圖2 PA4WS語義

4 PA4WS交互模式描述和應(yīng)用

雖然WS-CDL可以使用不同的方法來定義交互模式，但其可以分為基本交互模式和復(fù)合交互模式。復(fù)合交互模式也稱為結(jié)構(gòu)化交互模式。例如，單向通訊、賦值等屬于基本交互，而串行、并行和基于信息對齊的交互屬于復(fù)合模式。表1給出了WS-CDL同步操作、異步操作和基于信息對齊的PA4WS描述。為簡化，此處忽略了服務(wù)通道和會話通道。

表1 3種WS-CDL交互模式的PA4WS描述

表2給出了WS-CDL代碼片段和其對應(yīng)的PA4WS描述的對應(yīng)關(guān)系。通過例子可以看到，PA4WS具有很強的描述能力。

表2 WS-CDL代碼和其對應(yīng)的PA4WS描述

表2(續(xù))

5 總結(jié)和后續(xù)工作

基于進程代數(shù)，本文對WS-CDL定義了形式化模型PA4WS，并給出了語法、語義和其應(yīng)用。相比已有的工作，本文主要是通過定義工作單元原語，對WS-CDL的常見基于信息對齊和異步調(diào)用工作模式給出了說明，并對其復(fù)合方法給出了例子。后續(xù)工作包括：1)PA4WS對應(yīng)的類型理論；2)基于模式描述的自動復(fù)合前置條件；3)PA4WS特性驗證，如活性、安全性和公平性等[1-2]。

[1] Wang Y.A survey on formal methods for workflow-based web service composition[J].The Computing Research Repository (CoRR),2013,5535(10):21-46.

[2]Mazzara M,Ciavotta M.Issues about the adoption of formal methods for dependable composition of web services[J].The Computing Research Repository (CoRR),2013,2535(8):12-34.

[3]Decker G,Zaha J M,Dumas M.Execution semantics for service choreographies[C].Berlin:Springer,2006.

[4]Busi N,Gorrieri R,Guidi C,etal.Towards a formal framework for choreography[C].Linkoping,Sweden:IEEE Computer Society,2005.

[5]Carbone M,Honda K,Yoshida N.Structured Communication-Centred Programming for Web Serices[M].Braga,Portugal:ESOP,volume 4421 of LNCS,2012:2-17.

[6]C W.Web Services Choreography Description Language Version 1.0 2006/[2014-10-27].

[7]Ouyang C,Verbeek E,Aalst W M P V,etal.Formal Semantics and Analysis of Control Flow in WS-BPEL

[J].Science of Computer Programmin,2007,67(2/3):162-198.

[8]Zirpins C,Lamersdorf W,Baier T.Flexible coordination of service interaction patterns[C].New York,NY,USA:ACM,2004.

[9]Benatallah B,Dumas M,Fauvet M,etal.Patterns and skeletons for parallel and distributed computing[Z].2003:265-296.

[10]Benatallah B,Dumas M,Fauvet M C,etal.Overview of some patterns for architecting and managing composite web services[J].ACM SIGecom Exchanges,2002,3(3):9-16.

[11]Barros A,Dumas M,Hofstede A T.Service Interaction Patterns:Towards a Reference Framework for Service-Based Business Process Interconnection[EB/OL].Faculty of IT:Queensland University of Technology,2014.

[12]Filho A M S,Liesenberg H K E,Barros R S M.Interaction pattern gathering in service-oriented applications[C].2005.

[13]Lucchi R,Mazzara M.A pi-calculus based semantics for WS-BPEL[J].Journal of Logic and Algebraic Programming,2007,70(1):96-118.

[14]Bracciali A,Brogi A,Turini F.Coordinating Interaction Patterns[C].ACM,2001.

[15]Stefansen C.Expressing Workflow Patterns in CCS[EB/OL].http://www.stefansen.dk/papers/workflowpatterns.pdf,2014.

[16]Gorrieri R,Guidi C,Lucchi R.Reasoning about interaction patterns in Choreography[C].2005.

敬告作者·讀者

《江西科學(xué)》期刊著作權(quán)聲明

為適應(yīng)我國信息化建設(shè)，擴大本刊及作者知識信息交流渠道，作者在本刊發(fā)表之文章，其著作權(quán)使用費與本刊稿酬一次性給付(本刊所收版面費為與稿酬及所贈雜志對抵后的金額)，稿酬不再另付。如作者不同意，請在來稿時聲明，本刊將作適當處理。

本刊為中國知網(wǎng)、萬方數(shù)據(jù)、重慶維普、華藝數(shù)位數(shù)據(jù)、博看網(wǎng)全文收錄期刊。

《江西科學(xué)》編輯部

ModelingthePatternsofWS-CDLInteractionsBasedonProcessAlgebra

YUAN Xiaoyue,WAN Zhenzhen,FENG Xing

(Jiangxi Academy of Science.Institute of Applicative Physics,330029,Nanchang,PRC)

The description of choreography,WS-CDL,is an interactive description from global view which lacks formal semantics.The formal syntax and semantics,Process Algebra for WS-CDL (PA4WS),are proposed to describe WS-CDL.Particularly,the WorkUnit of WS-CDL is modeled in PA4WS.To model the composition of WS-CDL,the patterns of WS-CDL interaction including Interaction Based Information Alignment (IBIA) and asynchronous interactions are depicted.The benefits of PA4WS are exemplified by the snippets of WS-CDL and their descriptions of PA4WS.

WS-CDL;process algebra;formal methods

2014-10-27;

2014-11-28

袁曉月(1960-)，女，高級實驗師，從事熱處理工作。

10.13990/j.issn1001-3679.2014.06.030

TP301.2

A

1001-3679(2014)06-0878-06