基于进程代数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