Web服务组合行为一致性的形式化描述和分析

1、Web 服务组合行为一致性的形式化描述和分析?7 ?要:Web服务编排和 Web服务编制从全局和局部分别定义了 Web 服务组合的全局交互 行为和每个参与者的局部行为 ,为了保证 Web 服务组 合实现的正确性， Web 服务组合的全局交互行为和每 个参与者的局部行为必须是一致的。首先利用进程代 数给出了对 Web 服务组合的全局交互行为、 局部行为 以及二者之间的映射关系的形式化描述，在此基础上 分别通过分析全局会话变迁和局部进程变迁的关系和 进程互相似理论给出了 Web 服务组合全局交互行为 和局部行为的一致性的两个形式化判定准则。同时通 过案例说明了如何形式化地检测 Web 服务组合的全

2、 局交互行为和局部行为之间的一致性。结果显示提出 的 Web 服务组合一致性形式化定义和检测方法能检 测组合行为的一致性， 从而能有效地保证 Web 服务组 合的正确性。2入、?词:Web 服务组合 ;一致性检查 ; Web 服务; 形式化方?、型挤掷嗪?:TP311.5文献标志码 :AFormal description and analysis of conformance of composite Web service behaviorLI Ji n1,2?1 ?*, ZHANG Huai, WU Haoxio ngl, XIANG Jun11.School of Informatio

3、n Engineering, Hubei University for Nationalities, Enshi Hubei 445000, China2.Department of Information and Management, Central China Normal University, Wuhan Hubei 430079, ChinaAbstract:Web service choreography and orchestration defines the global interaction of composite Web service and the local

4、behavior of each participant from global and local perspectives, respectively. The conformance of each participants local behavior to global interaction is the guarantee of the correctness of Web service composition. The paper firstly presented a set of definitions to formally describe the global in

5、teraction of composite Web service, the local behavior of each participant and the mapping rules between them based on process algebra. Accordingly, two formal judgmental rules for the conformance of each participants local behavior to global interaction were proposed. The two formal rules were base

6、d on the relationship between the transition of global interaction and local process and bisimulation theorem. At last, the conformance formal checking approach was described through a case study. The result of the case study shows that the proposed conformance definition of Web service composition

7、and conformance checking approach can formally check the conformance of Web service composition effectively. As a result, the correctness of Web service composition can be guaranteed.Key words:Web services composition; conformance test; Web services; formal method0 引言 云计算作为一种基于互联网、以服务方式提供的 新型计算模式，目前

8、已引起工业界和学术界的广泛关 注，其服务高度互操作、跨平台和松耦合等特点使得 服务之间能够组合形成功能强大的应用 1。云计算 中 Web 服务是基本的计算实体。但是，单一的 Web 服务功能是有限的，难以满足不断变化的业务需求， 因此有必要将现有的单个、 基本的 Web 服务组合起来， 以实现功能增值的 Web 服务来满足不断变化的业务 需求。因此， Web 服务组合已经成为实现云计算按需 服务的关键技术。Web服务组合的一个重要手段是基于工作流的方 法2,即将Web服务看成一个商业流程(business process)而Web服务组合则是不同商业流程的组合 执行。基于工作流的 Web 服务

9、组合可以从两个层次来 描述 3-4: Web 服务编排(choreography)的和 Web 服务编制(orchestration)。Web服务编排规范由 Web 服务编排描述语言 5 (Web Services Choreography Description Language WSCDL来定义，它从全局的角 度描述了 Web服务组合的全局交互行为；Web服务编 制规范则由 Web 服务商业流程执行语言 6 (BusinessProcess Execution Language for Web Servic，eBsPEL4WS)来定义，它从一个局部参与者的角度来定义该参与者 其他Web服务

10、的交互操作，即描述了 Web服务组合 参与者的局部行为Web服务组合的全局交互行为可以看作 Web服 务组合的设计时规范(specification),它规定了每个参 与者应该如何交互；而 Web 服务组合的实现 (implementation)则由 Web服务组合的每个参与者局 部行为来描述。 因此，对于一个正确实现的 Web 服务 组合，其每个参与者的局部行为应该遵守 Web 服务组 合的设计时规范，即必须和Web服务组合的全局交互 行为保持一致 (conformance)。WSCDL和BPEL4WS从两个不同层次上描述了 Web 服务组合的全局交互行为和局部行为。但是 WSCDL和BPE

11、L4WS都是基于XML的描述性语言，缺 乏形式化的验证机制来保证 Web 服务组合的参与者 之间的正确交互；特别是当用 WSCDL和BPEL4WS规 范分别定义了 Web 服务组合的全局交互行为和局部 行为后，仍然缺乏形式化的定义和验证方法以保证 Web 服务组合全局交互行为和局部行为的一致性。解决上述问题的一种有效方法是利用形式化 的方法分别对Web服务组合的全局交互行为和局部 行为建立形式化的描述，并利用形式化的验证方法和 工具来验证 Web 服务组合参与者的动态行为能正确 交互以及全局交互行为和局部行为的一致性，从而保 证 Web 服务组合的正确性。 相关的研究工作有： Samik 等7

12、针对Web服务在异步通信的情况下，Web服 务全局交互行为与局部行为的一致性难以判定的问题， 提出了在一定条件下 Web 服务之间的异步通信可以 被同步通信来替代而不会影响服务之间交互的一致性。 Kohei等8利用类型化理论，对 Web服务的全局 交互行为和局部行为， 特别是 Web 服务之间的会话建 立了类型化的形式化模型，给出了类型化操作语义， 并给出了全局到局部的类型化映射规则。Nadia等9 定义了简单的形式化语言来分别描述 Web服务全局 和局部行为，并在此基础上给出了 Web服务间全局交 互行为和局部行为一致性的形式化定义，但是有些 WSCD冲的行为在CL中不能描述，而且他们没有定

13、 义如何将基于全局的交互协作映射到参与协作的每个 角色上从而得到每个角色的局部行为。Fu等:10 利用Btchi自动机来形式化描述 Web服务的局部动态 行为和全局交互行为 （他们将之定义为全局会话 ），同 时将全局会话映射分解到每个角色的局部行为上。 Baldoni等11则利用有限状态自动机来描述服务组 合，并验证全局行为和局部行为的一致性。本文定义了形式化模型框架 Formalized WSCD来 描述 Web 服务组合的全局交互行为， 同时利用进程代 数Pi?惭菟阈问交？描述每个参与者局部行为，并给出 了从全局交互行为到局部行为的映射关系。在以上基 础上，给出了 Web 服务组合全局交互

14、行为和局部行为 一致性的两个形式化判定准则。最后通过案例给出了 Web 服务组合全局交互行为和局部行为一致性的判定 方法。1 Web 服务组合全局交互行为的形式化描述框 架 Formalized WSCDLWSCDL规范描述了 Web服务组合的全局交互行 为。为了形式化建模Web服务组合的全局交互，本章 定义了 WSCDL勺形式化模型框架 Formalized WSCDL 包括语法和操作语义以及从全局交互行为到局部行为 的映射。1.1 WSCD1基本概念的形式化描述在 WSCDL中定义的Activities元素描述了 Web服 务之间的相互交互和协作的动作。在 Formalized WSCDL

15、中 用一个交互 In teraction 来表示一个 Activity 或 Activities 的组合（如顺序，迭代、并发执行 ）。参与 一个交互的每个 Web服务在WSCDL规范里由元素 Role角色）来定义。对于一个In teraction I，其中一个参与角色r有以 下重要的属性：代表角色r状态的变量以及角色r同其他角色进行交互的通道。特别地，v(r)表示角色r所 拥有的一个变量 v。角色间的交互通过通道进行，通道由通道名来唯 一地标识。通道上的类型有： request、 respond、 requestrespond,分别对应了三种基本交互类型：请求、 响应、请求一响应。通道位于信息

16、的接受者上。如果 角色ra通过通道ch发送信息给rb，则通道ch位于角 色rb，记为ch:rb。？才？为?2期李劲等： Web 服务组合行为一致性的形式化描述 和分析?扑慊？应用?n ?32卷1.2 Formalized WSCD 的语法对一个 Interaction I ，其形式化描述的语法如下：l:= I? : ?B|I1+I2|I1 II S2|I1.I2 |(while A) do I |(if A) do I |I? : ?callIB:= I? : ?no |I? : ?silent |I? : ?assign |I? : ?req |I? :?resp|I? : ?rr|I? :

17、 ?rrs |NULLI? ?no:= r(0)I? : ?silent:= r(T )I? : ?assign:= e(r戸x(r)I? : ?req:= rlf r2 ch:r2, x(r1)f y(r2)I? : ?resp:= rlJr2 ch:r1, x(r1尸 y(r2)I? : ?rr:= r1 y(r2), s(r1)y(r2); ch:r1,s(r1) PurchaseOrder(S)lcredit=Sf C sc:C, CreditCheck(S) CreditCheck(C) .SB cb:B, CreditStatement(C戸 CreditStatement(B)l

18、inventory=SI si:l, InventoryCheck(SpInventoryCheck(l)B ib:B, Shippinglnfo(l严 ShippingInfo(B)Icho=BS bs:S, PurchaseOrder(B)PurchaseOrder(S) .(SC sc:C, CreditCheck(S) CreditCheck(C) .SB cb:B, CreditStatement(C戸 CreditStatement(B)| 41 si:l, InventoryCheck(Sp InventoryCheck(l)B ib:B, Shippinglnfo(l严 Shi

19、ppinglnfo(B)若这4个角色的局部行为的Pi?惭菟忝枋龇直鸺俏？PB(Buyer的局部行为)、PS(Seller的局部行为)、 PC(Credit Checking Servic的局部行为)、Pl(lnventory 的局部行为 )，且分别为：PB=bsPurchaseOrder.(cb(CreditStatement).0|ib(Shipping lnfo).0)PS=bs(PurchaseOrder).(scCreditCheck.O|?si lnventoryCheck.0)PC=sc(CreditCheck).cbCreditStatement.0PI=si(Inventory

20、Check).ibShippingInfo.0首先用定义6来判断该Web服务组合的全局交互 行为Icho是否和局部行为PB|PS|PC|PI 致。假设Icho? 氮？PC|PD|PB|PW,首先利用 Formalized WSCD操作 语义对 Icho 的一种可能的会话顺序作推导：1)基于规则 3(会话的顺序执行 )和 2(基本会话的原 子性)，可以推导出：Icho=I? : ?order.(lcredit II linventory)true, a NULL.(lcredit II linventory)其中：a =Bf S bs:S, PurchaseOrder(B PurchaseOrd

21、er(S)根据定义 46，对于全局基本交互 a ，I(a )=B, S， P(a , B)=bsPurchaseOrde，r P(a , S)=bs(PurchaseOrder。) 同时对于角色B、S的Pi?惭菟憬?程 PB和PS?可以推 导出：PBP(a ,B)PBPB =cb(CreditStateme nt).O|ib(Shippi ngl nfo).O PSPa ,C)PSPS =scCreditCheck.O|si Inven toryCheck.O 因此根据定义 6 和假设，有NULL.(Icredit I linventory) PB |PS |PC|PI2)基于规则 3 和 4

22、(会话的顺序执行 )、规则 2(基本 会话的原子性 )、规则 5(会话的并行执行 )，可以推导 出：NULL.(lcredit II linventory)true, a*NULL.(NULL II linven tory)其中：a *=Sf Csc:C, CreditCheck(S)CreditCheck(C) .C tB cb:B, CreditStatement(C戸CreditStatement(B)为了节省篇幅，这里a *代表两步连续的基本交互。 同样地根据定义 46，对于全局基本交互a *， l(a *)=S, C, B, Pa( *, S)=scCreditCheck, Pa(

23、*, C)=sc(CreditCheck).cbCreditStatement, Pa( *, B)=cb(CreditStatement)。同时对于这两步连续的基本交互的参与者S、C、B各自的Pi?惭菟憬？程，可以推导出：PB P(a *,B)PB , PB =ib(Shippinglnfo).OPS P(a *,S)PS , PS =si InventoryCheck.OPCP(a *,C)PC , PC =0 因此根据定义 6 和推导步骤 1)的结论，得到：NULL.(NULL I linventory) PB |PS |PC |PI3) 基于规则 3 和 4(会话的顺序执行 )、规则

24、2(基本 会话的原子性 )、规则 5(会话的并行执行 )，可以推导NULL.(NULd Iinventory)true, a *NULL.(NULL| ? ?NULL)其中：a *=Sf I si:I, InventoryCheck(S)InventoryCheck(l)B ib:B, Shippinglnfo(l严 ShippingInfo(B)同样地根据定义 46，对于全局基本交互 a *，I(a*)=S, I, B, Pa( *, S)=siInventoryCheck, Pa( *,I)=si(InventoryCheck).ibShippingInfo, Pa( *, B)=ib(S

25、hippi ngl nfo。同时对于这两步连续的基本交互 的参与者S、I、B各自的Pi?惭菟憬?程,可以推导出：PS si(InventoryCheck)PS, PS=0PIP(a *,I)PI , Pl =0PB P(a *,B)PB, PB=0因此根据定义 6和推导步骤 2)的结论，得到 :NULL.(NULL NULL)=NULLPB |PS |PC |PI =0|0|0|0=0而NULLO是成立的，因此推导步骤1)3)的结论以 及最初的假设lchoPC|PD|PB|PW也是成立的。对任何 一种其他可能的会话顺序用同样的方法作推导，都可以得出同样的2崧邸* ?根据定义 7，可以用另外一种

26、方式判断 Web 服务 组合的全局交互行为和局部行为是否一致：首先将会 话 Icho 根据第 4 章定义的映射规则对角色 B、 S、 C、 I 分解，得到：P(Icho, B)=bsPurchaseOrder.(cb(CreditStatement).0|ib(ShippingI nfo).0)P(Icho, S)=bs(PurchaseOrder).(scCreditCheck.0|? 指?si Inven toryCheck.O)P(Icho, C)=sc(CreditCheck).cbCreditStatement.0 P(Icho, I)=si(InventoryCheck).ibSh

27、ippingInfo.0 然后判断 P(Icho, B)、P(Icho, S、) P(Icho, C、) P(Icho, I)是否分别和这四个角色的局部交互行为PB PS PCPI互相似。这里采用的是一个用来分析基于Pi?惭菟忝枋龅牟7.(11)低车墓艺？Mobility Workbench(MWB) : 13 来判断Pi?惭菟憬？程的互相似性，在MWB下，利用 eq 命令，可以验证它们彼此之间都是互相似的。 因此， IchoPC|PD|PB。6 结语Web服务组合可以从全局和局部两个不同层次来 描述参与组合的角色间的全局交互行为和每个角色的 局部行为。为了保证 Web 服务组合全局交互行为和

28、局 部行为的一致性，本文通过对 Web 服务组合全局交互 行为和局部行为的形式化描述以及从全局到局部的映 射，给出了 Web 服务组合全局交互行为和局部行为的 一致性的形式化定义和验证方法， 以保证 Web 服务组 合设计的正确性。?厅慰嘉南?:1VOUK M A. Cloud computi n Issues, research and implementations J. Journal of Computing and Information Technology, 2008, 16(4):235-246? ?2SRIVASTAVA B, KOEHLER J. Web service c

29、ompositioncurrent solutions and open problems C / ICAPS03: Proceedings of the 13th International Conference on Automated Planning & Scheduling. Trento:s.n., 2003:28-35.? ?3BUCCHIARONE A, GNESI S. A survey on services composition languages and models C/ WSMaTe: Proceedings of the International Worksh

30、op on WebServices Modeling and Testing. Palermo, Italy: s.n., 2006:51-63.r.it/ws-mate/Bucchi arone_WS-MaTe.pdf? ?4DIJKMAN R, DUMAS M. Serviceoriented design: a multiviewpoint approach J . International Journal of Cooperative Information Systems, 2004, 13(4): 337-368.? ?5KAVANT

31、ZAS N, BURDETT D, RIZINGER G, et al. Web services choreography description language: Version 1.0 EB/OL.(200509)20110409. /TR/WSCDL10/.? ?6ANDREWS T, CUBERA F, DHOLAKIA H, et al. Business process execution language for Web services: Version 1.1 EB/OL.(200509)20110409. http:/www128.ibm

32、.com/developerworks/library/specifi cation/wsbpel/.? ?7SAMIK B, TEVFIK B. Choreography conformance via synchronizability C/ WWW 2011: Proceedings of the 20th International World Wide Web Conference. NewYork: ACM, 2011:795-804.?8KOHEI H, NOBUKO, AYNDI B, et al. Multiparty asynchronous session typesC

33、/ POPL 2008: Proceedings of the 35th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. New York: ACM, 2011:273-284.? ?9NADIA B, ROBERTO G, CLAUDIO G. Choreography and orchestration: A synergic approach for system design C/ ICSOC 2005: Proceedings of the third International C

34、onferrence on Service Oriented Computing, LNCS 3826. Berlin: SpringerVerlag, 2005: 228-240.? ?10FU X, BULTAN T, SU J. Conversation protocols: a formalism for specification and verification of reactive electronic servicesC/ CIAA 2003: Proceedings of the 8th International Conference on Implementation

35、and Application of Automata, LNCS 2759. Berlin: SpringerVerlag, 2003:188-200.? ?11BALDONI M, BAROGLIO C, MARTELLI A, et al. Verifying the conformance of Web services to global interaction protocols: a first step C / WSFM 2005: Proceedings of the 2th International Workshop on Web Services and Formal

36、Methods, LNCS 3670. Berlin: SpringerVerlag, 2005:257-271.?12MILNER R,PARROW J,WALKER D.A calculus of mobile process: Parts I and n Jnformation and Computation,1992,100(1):1-77.? ?13VICTOR B, MOLLER F. The mobility workbeA tool for the picalculus C / CAV94: Proceedings of the 6th International Conference on Computer Aided Verification, LNCS 818. London: SpringerVerlag, 1994: 428-440.(上接第田平平537页)2FENG D, WONG K,PWU CM, et al. A technique for extracting physiological par