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

袁曉月，萬珍珍，馮 星

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

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

袁曉月，萬珍珍，馮 星

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

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

WS-CDL；進程代數；形式化方法

0 引言

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

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

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

1 WS-CDL簡介

WS-CDL模型是為達到一個共同的目標，多個服務間的協作的描述。基于文獻[6]，圖1給出了WS-CDL核心層的結構。

圖1 WS-CDL核心結構

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

2 相關工作與討論

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

3 基于進程代數的Web服務編排PA-4WS模型

3.1PA4WS語法

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

定義1：PA4WS語法如下：

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

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

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

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

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

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

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

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

2)C1;C2表示執行完C1后再執行C2的串行復合。

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

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

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

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

9)0表示進程終止。

定義2：PA4WS中的自由名，進程代數中的自由名是其與外界的接口，其具有重要的作用。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：結構化同余，符號≡表示PA4WS最小同余關系，其定義如下：C≡C′，當C可以語法變換為C′；(C,|,+,0)是在同余關系下≡的滿足交換律的獨異點。

3.2PA4WS語義

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

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

定義5：歸約關系，歸約關系是形如→?(σ,C′)×(σ′,C′)的二元關系。其是表示格局變換的函數。即在狀態σ下的進程C在完成如賦值、交互等計算后，其狀態變為σ′，進程變為C′。

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

圖2 PA4WS語義

4 PA4WS交互模式描述和應用

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

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

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

表2 WS-CDL代碼和其對應的PA4WS描述

表2(續)

5 總結和后續工作

基于進程代數，本文對WS-CDL定義了形式化模型PA4WS，并給出了語法、語義和其應用。相比已有的工作，本文主要是通過定義工作單元原語，對WS-CDL的常見基于信息對齊和異步調用工作模式給出了說明，并對其復合方法給出了例子。后續工作包括：1)PA4WS對應的類型理論；2)基于模式描述的自動復合前置條件；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.

敬告作者·讀者

《江西科學》期刊著作權聲明

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

本刊為中國知網、萬方數據、重慶維普、華藝數位數據、博看網全文收錄期刊。

《江西科學》編輯部

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