基于pi演算的web服务形式化描述模型＊

1、基于Pi-演算的Web服务形式化描述模型icularWebservicecompositionspecification.andcannottakeintoaccountbothglobalandlocaldesignmethod.A】SOallthecurrentmodelscannotdescribethedynamicarchitectureofWebservicecomposition.BesideofashortviewofrecentresearcheffortsofWebserviceformaldescription,为一个无限的名字集合,在7,上的小写字母如.,b,代表所有的

2、通信通道,变量和值;大写字母如P,p代表进程或进程表达式,具体表示如下:P:=OI.PI(y).PIr.Pl(w)PI=YPIyPIPIQIP+QI!PIA(Y.,Y)基于Pi一演算,本节给出了Web服务的形式化描述模型,分为基本概念定义,语法定义,同构规则以及操作语义几个部分进行详细说明.2.2Web服务形式化描述模型的概念定义在Web服务组合中,进行交互的双方是Web服务(单一的Web服务或者组合的Web服务),Web服务通过信道发送/接收信息,Web服务拥有的信道(内部信道以及与其他Web子服务进行交互的信道)以及其拥有的变量的作用域范围只是其所在的Web服务内部.因此,这些在形式化描述

3、模型中的语法定义中,所有名字都是受限的.本文将一个服务表示成四元组,记为S=(,0,V,B).其中:s为服务的名字,在同一个名字空间中,所有服务的名字两两不相同;,为服务拥有的输入信道集合;0为服务拥有的输出信道集合;V为服务所拥有的变量集合,代表服务当前的状态,这些变量都是在服务内部,外部不可见;B为服务拥有的行为集合,整个Web服务的结构就是通过行为的执行顺序来定义的.另外,在服务组合的描述中,需要用到各种各样的组合规则,这些规则不是简单地对名字的比较,基本都涉及到各种各样的命题.因此,使用P表示和服务_s相关的命题集合,对其中某一个具体命题P的引用记为P:P.本文将输出信道和输入信道分开

4、来定义,主要是因为在Web服务的实际应用中,除了那些可以用来在服务之间输入输出进行交互的信道之外,还存在那些只能用来接收信息的输入信道,或者只能用来返回输出结果的输出信道.由于信道对应着Web服务资源的访问,出于安全原因,需要将输入信道和输出信道的定义分开,区别其功能.对服务s所拥有的输入信道,输出信道,变量和行为集合的引用分别表示如下:Is,0,Vs和B.对这些集合中具体元素的引用分别表示为1s:i,0:o,:和B:6.2.3Web服务形式化描述模型的语法定义设服务s的行为集合为B,VbB,为如下之一:a)B:b是输出动作.B:b:=(y),是输出信道,Y是输出名字,为服务5的私有变量.b)

5、B:6是输入动作.B:6:=(Y),是输入信道,Y是输出名字,为服务-s的私有变量.e)B:b是内部动作.B:6:=Jr,是Web服务S的内部行为,在外界是无法看到的.d)B:6是服务的调用动作.B:b:=S(y一,Y).其中:Js(一,)s;,是发生Web服务调用时使用的实际参数;-,是定义Web服务S的形式参数.服务S的结构就是通过其行为的发生顺序和一些结构操作符来描述,这里只详细说明Web服务的结构和Pi一演算中进程结构的不同之处.Web服务S的结构定义如下:s:0IOs:0(:).SI05:o(Cs:c).SI,s:(Vs:).SIIs:i(Cs:c).SIr.SIPs:.PSIPs:

6、pSISl+S2ISlIS2I!SI!Ps:pSIs(Y.,Y)s(一,)sa)服务的语法定义的前缀形式中,需要说明的是:和C:C是服务拥有的变量和信道,其名字是在服务内部受限的,因此,在服务的前缀表达式中,输入输出前缀的客体都是受限制的.一般前缀r的出现是由于服务通过信道交互,发生了服务组合,两个组合的服务通过其交互信道发生的信息传递,是组合后的服务的外部不可见的.b)表达式lP:ps表示这样的服务:当命题Ps:p成立时,其行为表现为服务S,否则为0.表达式P:pS相类似.c)表达式!P:PS表示边界条件的命题P:p成立时,重复执行服务S,直至命题P:P为假.!P:pS是一个简写的形式,可以

7、用其他规则表示,如!(P:pS+Ps:plo).2.4Web服务形式化描述模型的同构规则设S,S,S和S,都表示服务,那么同构规则如下:如果服务S.和S2仅仅是命名不同(包括服务的命名,变量的命名和信道的命名),则S.=-S:.SlIS2ES2ISl(SIIS2)IS3;S1I(S2IS3)S10=SSl+S2iS2+Sl(Sl+S2)+S3三Sl+(S2+S3)S+0兰Ss();Sifs():=S2.5Web服务形式化描述模型的操作语义Web服务形式化描述模型的操作语义定义了Web服务之间如何发生交互,以及完成了交互动作之后的迁移规则.一部分与一演算中定义类似的操作语义如下:AS.STRUC

8、TAS,INPUTS1-=Sl ls2AS2;s2S.,|s,ASACT:T.S.+SIs:i(c:).5旦5/cs:.(EVs:v).ss/Vs:Os:0(Cs:c).S0s:O(cs:c)JsS?2170?计算机应用研究第28卷As_cH0lcE:兰!:Sl+S2三s1.Sl1Abn()n(cs2uVs2)=AS.PAR:一SlIS2三s1,IS2As.coM:SOsl:(1:y)J2:(vs2:)l-_SS_=S1IS2Js1IS2y/zt!SIlS2一sIIS2y/z上述操作语义中所有的名字都是某一个Web服务内部的变量,全部都是限定名.各个操作语义具体的含义不在这里详述.w

9、eb服务形式化描述模型修改了如下操作语义:Ss,t,:Psll!Ps:JDS=I!Ps:p修改后操作的含义如下:a)规则ASMATCH指如果服务s在执行了动作O/之后表现为服务S,则服务P:pS在命题P:p成立时,执行了动作之后表现为服务S.b)规则ASREP指如果服务S在执行了动作Ot之后表现为服务S,则服务P:p!S在命题P:p为真的情况下,执行了动作a之后表现为SIP:p!S.这个规则主要用来描述服务的循环执行.3WS.CDL规范和BPEL4WS规范向形式化描述模型的映射Web服务的开发者可以利用BPEL4WS语言的规范将业务逻辑相关的子服务组合成一个新的Web服务.组合之后的Web服务

10、作为一个中心协调者,负责与各个子服务交换信息,协调这些子服务问的交互以完成组合服务的功能.3.1WSCDL向形式化描述模型的映射WSCDL规范是W3C提出的一种Web服务编排描述语言,它从全局的角度定义一个彼此对等的,跨组织的,存在交互的并发系统,目的是描述服务之间进行协作时需要遵从的消息通信规则.本文涉及的WSCDL定义的主要行为以及其所代表的含义如表1所示.在WSCDL规范中最为重要的工作就是描述交互行为.一次交互行为会导致多个参与者之间发生一次信息交换,它包括了两个角色三类信息的交换过程:发送请求(request),响应请求(response),发送并要求响应(requestreh(1)

11、.0lch(v2).0表1WSCDL的主要行为及含义d)交互活动分为请求一应答交互,单向请求行为和单向应答行为.将交互活动参与的双方抽象为服务,将fromRole抽象为服务S,toRole抽象为服务S.它们两个通信的信道名称为c.如果channelType不包含passing子元素,那么可以得到S和S分别的输入输出信息都要经过c.进行传递,则有Is,:ch1,0s,:ch1,s,:ch1和0s:ch1;如果ehannelVariable包含passing子元素,那么应答就发生在passing子元素所指定的动态I临时信道(ch)上.c是s.的输出信道和S的输入信道,是S的输入信道和的输出信道,有

12、,:c,0s:ch1,:ch1和0s,:ch2.变量l和4是S1拥有的变量,和是S拥有的变量,有,:V,:,.-y:和,:.e)请求一应答交互描述了两个角色间的一次请求一应答交互.如果ehannelVariabte不包含passing子元素,则请求和应答都发生在同一个信道.上,其对应的描述为S=ch().ch1(4).Sl和S2:=chl(2).chl().;如果ehannelVariable包含passing子元素,那么S要通过信道ch将用于接收返回结果的信道:发送给,要从信道.接收如,那么fromRole描述为S=chl(1).chl(也).ch2(4).Sl,toRole描述为:=ch1

13、(1)2).chi(ch2).ch2().Sz.f)单向请求行为的信息从fromRole传递到toRole,其对应的描述为Sl:=ch1(131).ch1(ch2).c(4).S1和S2:=ch(2).S2.g)单向应答行为发生时,S.要通过信道c.将用于接收返回结果的信道c:发送给S:,S:要从信道c接收信道c:,其交换的信息从roRole传递到fromRole.对应的描述为Sc,(口4).l和:=chl(ch2).ch2(3).WSCDL序结构可以与其他序结构嵌套,把多个活动组合起来,从而描述编排所执行的多个活动之间的顺序.序结构可以是如下几种类型:顺序(sequence),并行(para

14、lle1)和选择(choice).a)顺序结构由sequence元素标记,其内部所包含的一系列活动必须顺序执行.将顺序结构行为抽象为服务S,设其包第6期胡静,等:基于Pi一演算的Web服务形式化描述模型?217l?含n个子活动,按照执行顺序分别抽象为服务S,S:,5.服务S的描述为S:=S,S,S.b)并行结构由parallel元素标记,包含的一个或多个子活动同时被激活,当标签中所有子行为执行完所有的活动之后,该并行活动成功结束.这些子活动活动时会发生交互,形成交互序列.其对应的描述为S:=S.lSI.?lS.C)选择结构由choice元素标记,描述内部包含的两个或多个活动,每次只能根据条件选

15、择其中一个执行.将选择结构行为抽象为服务S,设其包含n个进行交互的子行为,条件选择抽象为服务S中的一组命题,Ps:p,P:p:,:p,简写为P,P:,P.将这个选择序列中与n个命题一一对应的子行为分别抽象为服务S,S,S.服务S的描述为S:=p1Sl+p2s2+pSod)工作单元描述了一组有条件的迭代执行的子行为.Guard属性用来决定一个重复迭代是否执行;repeat属性决定迭代执行或终止的条件;block属性用于判定以上两种条件是否需要等待相关变量以决定是否继续执行,描述为S:=ch(.(Ps:gS.!Ps:rS+Ps:g0).3.2BPEL4WS规范向形式化描述模型的映射用Pi一演算对B

16、PEL4WS规范进行描述的工作已经比较成熟,利用这些描述,可以很方便地将BPEL4WS规范映射到Web服务形式化描述模型中.所有行为的描述里面,partnerLink,portType,operation指定了Web服务的访问点,inputVariable指定了发送的调用参数,outputVariable指定了接收的调用结果.将每个行为抽象为服务S.发送的调用参数抽象为:inVar,简写为inVar.接收的调用结果抽象为:outVar,简写为outVar.将由partner-Link,portType和operation指定的固定通信信道抽象为0s;chn,将其简写为chn,用来发送inVar

17、.用来接收调用结果的动态通信信道抽象为:let,简写为let.a)Invoke行为表示服务通过chn信道发送调用参数inVar,并提供一个接收返回结果outVar的信道.相应地描述为S:chn(inVar).ehn(1et).1et(outVar).0ob)Receive行为表示从chn信道接收调用参数inVar,若没有相应reply行为与其对应,但又需要输出返回结果时,receive还需要从chn接收一个输出结果的信道let,描述为S:=ehn(inVar).chn(1et).1et(outVar)0;如果receive行为有相应reply行为对应,则由对应的reply行为进行返回结果的输出

18、,那么相应地描述为S:=chn(inVar).0.C)Reply行为需要从chn信道接收一个用于接收返回结果outVar的信道let.描述为S:=chn(ret).1et(Var).0.d)Assign行为表示在服务内部变量间的赋值动作是在服务外界无法观察到的内部行为,只能用下面的方法来模拟变量间的赋值,其中的信道是外界不可见的.相应地描述为S:=ch(1).0Ich(2).0.e)Empty行为代表一个没有任何动作的行为,可以用已经结束了的服务对其进行描述,其对应的描述为S:=0.f)Sequence结构定义了一组顺序执行的子行为,其对应的描述为S:=S】.S2.S.g)Flow结构定义了一

19、组并发执行的子行为,其对应的描述为|s:1IS21.?lS.h)Switch结构根据一个或多个选择条件分支,从若干个子行为中选择一个执行,其中各个不同的命题对应多个选择分支.对应的描述为S:S+P-P2p.S.i)While结构表示其包含的子行为被重复执行,直到某个条件不再满足时停止.其相应的描述为5:=!p5+JD0.4WS.CDL规范和BPEL4WS规范在Web服务的形式化模型中的一致性上章将与Web服务组合结构相关的BPEIAWS规范的行为以及WSCDL规范的主要元素都在Web服务形式化描述模型中作了映射.基于这个映射,本章分析这两种基于不同角度对Web服务组合进行描述的规范的主要行为的

20、对应关系,而后通过第四方物流管理平台的例子说明用这两种不同规范描述的同一Web服务组合在Web服务形式化描述模型中是一致的.WSCDL和BPEIAWS规范的主要交互行为在Web服务形式化描述模型中的对应关系为:a)WSCDL规范的requestrespondinteraction中的fromRole对应BPEIAWS规范的invoke,在模型中描述为S=chl(1).chl(ch2).ch2(4).S1;toRole对应receive+reply,描述为S2:=ch1(2).chl(ch2).ch2(3).S2.b)WSCDL规范的requestinteraction中的fromRole对应B

21、PEL4WS规范的invoke,在模型中描述为S=ch】(】).cl(c).c2(V4).S1;toRole对应receive,在模型中描述为S2:=chl(口2).ch1(ch2).ch2().S2.e)WSCDL规范的respondinteraction中的fromRole对应BPEL4WS规范的receive,在模型中描述为S1:=ch2(4).Sl;toRole对应reply,描述为S2:=ch.(ch2).().S2.为了说明对同一个Web服务组合,采用上述两种规范进行描述之后,在Web服务形式化描述模型中的映射具有一致性,本节用一个第四方物流管理平台的例子进行说明.最后指出如果这一

22、管理平台的体系结构在实际应用中是动态的,那么上述两种规范均无法体现,但是直接使用Web服务形式化描述模型的行为结构就可以描述这一动态结构.4.1WSCDL规范描述的第四方物流管理平台本文从全局的角度考虑第四方物流管理平台的例子,其四个角色之间基于全局的交互如图1所示.图中每一个方框代表一个服务,实线为服务间固定的通信信道,虚线为动态信道,即从客户角度来看,与其交互的是一个组合服务,通信的信道是leq和ack,而组合服务内部的信道reqs,sresp,pay和payr对客户来讲是不可见的.一一一ER$!一图1第四方物流管理平台基于全局的交互协作?2172?计算机应用研究第28卷在wS.cDL描述

23、文档中,除了本文提到的与Web服务组合的结构相关的活动和结构之外,还有大量的其他属性信息,这些信息不是本文研究的重点,而且其存在会使得结构不明显.因此,用如下函数的形式对本文提到的WSCDL中的活动和结构进行简单说明,其中各个变量的说明与前面相同.a)Requestrespond行为:req?resp(fromRole,toRole,ch1,ch2,l,2,3,4).b)Requestinteraction行为:req(fromRole,toRole,ch1,ch2,l口2,4).e)Respondinteraction行为:resp(fromRole,toRole,chl,ch2,2,4).

24、d)两个活动顺序执行,用”.”连接;两个活动并发执行,用“连接;两个活动选择执行,用”+”连接,判断条件用命题表示.基于m,detMB,respondl,le一spondm)I1reqresp(Sc,S,req,ack2,NULL,NULL,billm,billc).req-resp(S,SB,pay,payr,paym,payb,billb,billm)+P2(reqresp(Sc,SM,req,ackl,searchc,searchm,gpsm,gpsc).reqresp(SM,SL,reqs,sresp,searchm,searchl,gpsl,gpsm)将以上描述对应成Web服务形式化

25、描述模型中的行为结构,可以分别得到SS,S和,这里取最复杂的用于后面的说明.Sreq(orderm).(P1(req(detailm).req(ack1).ack1(respondom).reqs(detailm).reqs(sresp).resp(respondm)Ireq(ack2).ack2(billm).pay(paym).pay(payr).payr(billm)+P2(req(searchm).q(ack1).ack1(gpsm).reqs(searchm).reqs(sresp).resp(gpsm)4.2BPEL4WS规范描述的第四方物流管理平台第四方物流管理平台用BPEIAW

26、S规范描述的业务流程如图2所示.一I.!一ilogistics1图2BPEL4WS规范描述的4PL业务流程可以采用自顶向下的方法将上述BPEIAWS描述的业务流程从根节点元素开始依次对应到Web服务形式化描述模型中,这个过程不在这里赘述.得到的描述如下:SM:req(orderm).(pl(req(detailm).reqs(detailm).reqs(sresp).sresp(respondm).req(ack1).ackl(respondm)Ipay(paym).pay(payr).(billm).req(ask2).ask2(billm)P2(req(searchm).reqs(sear

27、chm).reqs(sresp).resp(gpsm).req(ask1).ask1(gpsm)4.3两种规范的映射之间的比较将由BPEL4WS和WSCDL规范描述得到的映射用一演算的自动验证工具MWB进行deadlocks命令检查,发现由WSCDL规范描述得到的映射存在着死锁.其中一些动作的先后顺序需要进行调整.比如其映射的ack(respondm),表示要从信道ack1中发送信息respondm,但此时respondm是在后面的动作resp(respondm)中得到的.这种动作的前后顺序问题是由于严格按照了WSCDL规范映射中的动作顺序,但在实际的应用过程中,产生调用操作的服务应该是在执行

28、完了所有的动作之后再考虑返回结果的接收问题,也就是说产生调用操作的服务,其对应的动作序列S=ch().ch,(ch).ch().S在实际生成映射时,应该变为S=(,).s.两(c2).ch2(4).经过变化之后,两种描述的映射都不存在死锁,再运行weq命令,可以得到经过修改之后的两个Web服务组合的描述是弱相似的.前面的例子中只考虑了第四方物流管理平台的服务,没有考虑第三方物流的服务,银行的服务以及用户的操作.后面三个服务的结构比第四方物流管理平台的服务要简单许多,根据前面的映射原则,仍然可以得到两个规范描述的映射结果完全一致的结论.4.4动态体系结构的描述方法再回到前面说的第四方物流管理平台

29、的例子本身,无论是WSCDL规范描述的业务流还是BPEIAWS规范描述的业务流,都存在着如下事实:用户和第三方物流以及银行的所有交互数据都要通过第四方物流管理平台,这在实际应用上并不合理,尤其是当一些交换的数据涉及到用户个人隐私的时候.基于上述考虑,第四方物流管理平台应该在用户需要与银行(第三方物流)进行数据交互时,在用户和银行(第三方物流)之间建立一个临时通信的信道,使得用户可以直接与银行(第三方物流)进行交互,而不需要经过第四方物流管理平台的转发,这样可以避免个人隐私信息的泄露,保证了整个业务流程的数据安全性.而一旦这种动态连接信道建立起来,那么整个系统的体系结构也就发生了相应的变化.无论

30、是wsCDL还是BPEIAWS规范,都无法描述这种动态体系结构的建立.但是直接从Web服务形式化描述模型出发,可以直接用动作序列去描述这种动态的体系结构.这种动态体系结构的变化如图3所示,(a)表示没有建立动态信道的结构,(b)是第四方物流管理平台传递了信道之后形成的新的体系结构.进行了信道传递之后,临时信道ack,sresp和pay就断开了链接,而产生了ltoc和btoc两个临时的信道,分别连接用户和第三方物流以及银行,进行以后的数据交互.第四方物流管理平台在调用第三方物流以及银行服务之后,并不直接从临时信道sresp和payr接收第三方物流或者银行的数据,而是接收一个他们的通信信道,保存在

31、变量W.和W:中.而后,从用户接收临时信道ack.和ack:(保存在变量C和b中),并通过这两个信道将变量W,和W发送给用户.具体的描述如下:SM:req(orderm).(p1(req(detailm).郦(detailm).(sresp).sresp(W1).req(c1).第6期胡静,等:基于Pi一演算的Web服务形式化描述模型?2l73?(“1)I两(paym).一pay(payr).payrw2).req(c6).一cb(w2)+p2(req(searchm).而(searchm).诗(searchm).雨(sresp).sresp(w1).req一塑=_esp嚣目塞娶:ustome

32、rtreaLLlIpayr:Ipay闺(a】第四方物流管理平台静态体系结构(b)第四方物流管理平台动态体系结构图3体系结构相应的第三方物流,银行的服务和用户需求的具体描述如下:S=PI(reqs(detail1).reqs(cm).cfft(hoc)(reqs(search1).reqs(cm).em(1toc).hoc(gps1)互,组合成新的Web服务,因此,其功能和结构可以通过其交互行为来描述.b)用操作语义来描述Web服务发生组合时交互的规则.操作语义描述了Web服务发生相应的动作之后的迁移,以及发生交互行为之后整个系统体系结构的变化.e)给出现有的基于全局描述Web服务组合的WSCD

33、L规范和基于局部描述Web服务组合的BPEIAWS规范在本模型中的映射结构,使得用户可以将现有的基于组合规范的描述映射为本模型中的描述方法,使用Pi一演算的自动验证工具,在Web服务组合真正执行之前进行验证.而且这两种基于不同角度的描述在本模型中的映射结构具有一致性.d)利用此模型的描述方法直接描述具有动态体系结构的Web服务组合.已有的Web服务组合描述规范都无法描述由动态通信信道带来的Web服务组合体系结构的动态性.本文的模型可以方便地进行动态体系结构的描述.参考文献:1岳昆,王晓玲,周傲英.Web服务核心支撑技术:研究综述J.软件,2004,15(3):428.442.2BERARDID

34、,CALVANESED,DeGIACOMOG,eta1.AutomaticservicescompositionbasedonbehaviordescriptionsJ.InternationalJournalofCooperativeInformationSystems,2005,14(4):333.376.1而(respond1)+P23张文涛,彭泳,陈俊亮.会话类E-Service的接口兼容和服务组合SB=pay(payb).pay(cm).ca(btoc).btoe(billb)Sc=req(orderc).(pl(req(detailc).req(ack1).ack1(“1).wl(respondc)Ireq(ack2).ack2(w2).w2(billc)P2(req(searchm).req(ack1).ackl(w1).w1(gpsc)其中第三方物流通过变量cm保存从第四方物流管理平台接收的返回信道,其与用户交互的