基于pi演算的web服務(wù)形式化描述模型＊

1、基于Pi-演算的Web服務(wù)形式化描述模型icularWebservicecompositionspecification.andcannottakeintoaccountbothglobalandlocaldesignmethod.A】SOallthecurrentmodelscannotdescribethedynamicarchitectureofWebservicecomposition.BesideofashortviewofrecentresearcheffortsofWebserviceformaldescription,為一個(gè)無限的名字集合,在7,上的小寫字母如.,b,代表所有的

2、通信通道,變量和值;大寫字母如P,p代表進(jìn)程或進(jìn)程表達(dá)式,具體表示如下:P:=OI.PI(y).PIr.Pl(w)PI=YPIyPIPIQIP+QI!PIA(Y.,Y)基于Pi一演算,本節(jié)給出了Web服務(wù)的形式化描述模型,分為基本概念定義,語法定義,同構(gòu)規(guī)則以及操作語義幾個(gè)部分進(jìn)行詳細(xì)說明.2.2Web服務(wù)形式化描述模型的概念定義在Web服務(wù)組合中,進(jìn)行交互的雙方是Web服務(wù)(單一的Web服務(wù)或者組合的Web服務(wù)),Web服務(wù)通過信道發(fā)送/接收信息,Web服務(wù)擁有的信道(內(nèi)部信道以及與其他Web子服務(wù)進(jìn)行交互的信道)以及其擁有的變量的作用域范圍只是其所在的Web服務(wù)內(nèi)部.因此,這些在形式化描述

3、模型中的語法定義中,所有名字都是受限的.本文將一個(gè)服務(wù)表示成四元組,記為S=(,0,V,B).其中:s為服務(wù)的名字,在同一個(gè)名字空間中,所有服務(wù)的名字兩兩不相同;,為服務(wù)擁有的輸入信道集合;0為服務(wù)擁有的輸出信道集合;V為服務(wù)所擁有的變量集合,代表服務(wù)當(dāng)前的狀態(tài),這些變量都是在服務(wù)內(nèi)部,外部不可見;B為服務(wù)擁有的行為集合,整個(gè)Web服務(wù)的結(jié)構(gòu)就是通過行為的執(zhí)行順序來定義的.另外,在服務(wù)組合的描述中,需要用到各種各樣的組合規(guī)則,這些規(guī)則不是簡單地對名字的比較,基本都涉及到各種各樣的命題.因此,使用P表示和服務(wù)_s相關(guān)的命題集合,對其中某一個(gè)具體命題P的引用記為P:P.本文將輸出信道和輸入信道分開

4、來定義,主要是因?yàn)樵赪eb服務(wù)的實(shí)際應(yīng)用中,除了那些可以用來在服務(wù)之間輸入輸出進(jìn)行交互的信道之外,還存在那些只能用來接收信息的輸入信道,或者只能用來返回輸出結(jié)果的輸出信道.由于信道對應(yīng)著Web服務(wù)資源的訪問,出于安全原因,需要將輸入信道和輸出信道的定義分開,區(qū)別其功能.對服務(wù)s所擁有的輸入信道,輸出信道,變量和行為集合的引用分別表示如下:Is,0,Vs和B.對這些集合中具體元素的引用分別表示為1s:i,0:o,:和B:6.2.3Web服務(wù)形式化描述模型的語法定義設(shè)服務(wù)s的行為集合為B,VbB,為如下之一:a)B:b是輸出動作.B:b:=(y),是輸出信道,Y是輸出名字,為服務(wù)5的私有變量.b)

5、B:6是輸入動作.B:6:=(Y),是輸入信道,Y是輸出名字,為服務(wù)-s的私有變量.e)B:b是內(nèi)部動作.B:6:=Jr,是Web服務(wù)S的內(nèi)部行為,在外界是無法看到的.d)B:6是服務(wù)的調(diào)用動作.B:b:=S(y一,Y).其中:Js(一,)s;,是發(fā)生Web服務(wù)調(diào)用時(shí)使用的實(shí)際參數(shù);-,是定義Web服務(wù)S的形式參數(shù).服務(wù)S的結(jié)構(gòu)就是通過其行為的發(fā)生順序和一些結(jié)構(gòu)操作符來描述,這里只詳細(xì)說明Web服務(wù)的結(jié)構(gòu)和Pi一演算中進(jìn)程結(jié)構(gòu)的不同之處.Web服務(wù)S的結(jié)構(gòu)定義如下: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)服務(wù)的語法定義的前綴形式中,需要說明的是:和C:C是服務(wù)擁有的變量和信道,其名字是在服務(wù)內(nèi)部受限的,因此,在服務(wù)的前綴表達(dá)式中,輸入輸出前綴的客體都是受限制的.一般前綴r的出現(xiàn)是由于服務(wù)通過信道交互,發(fā)生了服務(wù)組合,兩個(gè)組合的服務(wù)通過其交互信道發(fā)生的信息傳遞,是組合后的服務(wù)的外部不可見的.b)表達(dá)式lP:ps表示這樣的服務(wù):當(dāng)命題Ps:p成立時(shí),其行為表現(xiàn)為服務(wù)S,否則為0.表達(dá)式P:pS相類似.c)表達(dá)式!P:PS表示邊界條件的命題P:p成立時(shí),重復(fù)執(zhí)行服務(wù)S,直至命題P:P為假.!P:pS是一個(gè)簡寫的形式,可以

7、用其他規(guī)則表示,如!(P:pS+Ps:plo).2.4Web服務(wù)形式化描述模型的同構(gòu)規(guī)則設(shè)S,S,S和S,都表示服務(wù),那么同構(gòu)規(guī)則如下:如果服務(wù)S.和S2僅僅是命名不同(包括服務(wù)的命名,變量的命名和信道的命名),則S.=-S:.SlIS2ES2ISl(SIIS2)IS3;S1I(S2IS3)S10=SSl+S2iS2+Sl(Sl+S2)+S3三Sl+(S2+S3)S+0蘭Ss();Sifs():=S2.5Web服務(wù)形式化描述模型的操作語義Web服務(wù)形式化描述模型的操作語義定義了Web服務(wù)之間如何發(fā)生交互,以及完成了交互動作之后的遷移規(guī)則.一部分與一演算中定義類似的操作語義如下: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?計(jì)算機(jī)應(yīng)用研究第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上述操作語義中所有的名字都是某一個(gè)Web服務(wù)內(nèi)部的變量,全部都是限定名.各個(gè)操作語義具體的含義不在這里詳述.w

9、eb服務(wù)形式化描述模型修改了如下操作語義:Ss,t,:Psll!Ps:JDS=I!Ps:p修改后操作的含義如下:a)規(guī)則ASMATCH指如果服務(wù)s在執(zhí)行了動作O/之后表現(xiàn)為服務(wù)S,則服務(wù)P:pS在命題P:p成立時(shí),執(zhí)行了動作之后表現(xiàn)為服務(wù)S.b)規(guī)則ASREP指如果服務(wù)S在執(zhí)行了動作Ot之后表現(xiàn)為服務(wù)S,則服務(wù)P:p!S在命題P:p為真的情況下,執(zhí)行了動作a之后表現(xiàn)為SIP:p!S.這個(gè)規(guī)則主要用來描述服務(wù)的循環(huán)執(zhí)行.3WS.CDL規(guī)范和BPEL4WS規(guī)范向形式化描述模型的映射Web服務(wù)的開發(fā)者可以利用BPEL4WS語言的規(guī)范將業(yè)務(wù)邏輯相關(guān)的子服務(wù)組合成一個(gè)新的Web服務(wù).組合之后的Web服務(wù)

10、作為一個(gè)中心協(xié)調(diào)者,負(fù)責(zé)與各個(gè)子服務(wù)交換信息,協(xié)調(diào)這些子服務(wù)問的交互以完成組合服務(wù)的功能.3.1WSCDL向形式化描述模型的映射WSCDL規(guī)范是W3C提出的一種Web服務(wù)編排描述語言,它從全局的角度定義一個(gè)彼此對等的,跨組織的,存在交互的并發(fā)系統(tǒng),目的是描述服務(wù)之間進(jìn)行協(xié)作時(shí)需要遵從的消息通信規(guī)則.本文涉及的WSCDL定義的主要行為以及其所代表的含義如表1所示.在WSCDL規(guī)范中最為重要的工作就是描述交互行為.一次交互行為會導(dǎo)致多個(gè)參與者之間發(fā)生一次信息交換,它包括了兩個(gè)角色三類信息的交換過程:發(fā)送請求(request),響應(yīng)請求(response),發(fā)送并要求響應(yīng)(requestreh(1)

11、.0lch(v2).0表1WSCDL的主要行為及含義d)交互活動分為請求一應(yīng)答交互,單向請求行為和單向應(yīng)答行為.將交互活動參與的雙方抽象為服務(wù),將fromRole抽象為服務(wù)S,toRole抽象為服務(wù)S.它們兩個(gè)通信的信道名稱為c.如果channelType不包含passing子元素,那么可以得到S和S分別的輸入輸出信息都要經(jīng)過c.進(jìn)行傳遞,則有Is,:ch1,0s,:ch1,s,:ch1和0s:ch1;如果ehannelVariable包含passing子元素,那么應(yīng)答就發(fā)生在passing子元素所指定的動態(tài)I臨時(shí)信道(ch)上.c是s.的輸出信道和S的輸入信道,是S的輸入信道和的輸出信道,有

12、,:c,0s:ch1,:ch1和0s,:ch2.變量l和4是S1擁有的變量,和是S擁有的變量,有,:V,:,.-y:和,:.e)請求一應(yīng)答交互描述了兩個(gè)角色間的一次請求一應(yīng)答交互.如果ehannelVariabte不包含passing子元素,則請求和應(yīng)答都發(fā)生在同一個(gè)信道.上,其對應(yīng)的描述為S=ch().ch1(4).Sl和S2:=chl(2).chl().;如果ehannelVariable包含passing子元素,那么S要通過信道ch將用于接收返回結(jié)果的信道:發(fā)送給,要從信道.接收如,那么fromRole描述為S=chl(1).chl(也).ch2(4).Sl,toRole描述為:=ch1

13、(1)2).chi(ch2).ch2().Sz.f)單向請求行為的信息從fromRole傳遞到toRole,其對應(yīng)的描述為Sl:=ch1(131).ch1(ch2).c(4).S1和S2:=ch(2).S2.g)單向應(yīng)答行為發(fā)生時(shí),S.要通過信道c.將用于接收返回結(jié)果的信道c:發(fā)送給S:,S:要從信道c接收信道c:,其交換的信息從roRole傳遞到fromRole.對應(yīng)的描述為Sc,(口4).l和:=chl(ch2).ch2(3).WSCDL序結(jié)構(gòu)可以與其他序結(jié)構(gòu)嵌套,把多個(gè)活動組合起來,從而描述編排所執(zhí)行的多個(gè)活動之間的順序.序結(jié)構(gòu)可以是如下幾種類型:順序(sequence),并行(para

14、lle1)和選擇(choice).a)順序結(jié)構(gòu)由sequence元素標(biāo)記,其內(nèi)部所包含的一系列活動必須順序執(zhí)行.將順序結(jié)構(gòu)行為抽象為服務(wù)S,設(shè)其包第6期胡靜,等:基于Pi一演算的Web服務(wù)形式化描述模型?217l?含n個(gè)子活動,按照執(zhí)行順序分別抽象為服務(wù)S,S:,5.服務(wù)S的描述為S:=S,S,S.b)并行結(jié)構(gòu)由parallel元素標(biāo)記,包含的一個(gè)或多個(gè)子活動同時(shí)被激活,當(dāng)標(biāo)簽中所有子行為執(zhí)行完所有的活動之后,該并行活動成功結(jié)束.這些子活動活動時(shí)會發(fā)生交互,形成交互序列.其對應(yīng)的描述為S:=S.lSI.?lS.C)選擇結(jié)構(gòu)由choice元素標(biāo)記,描述內(nèi)部包含的兩個(gè)或多個(gè)活動,每次只能根據(jù)條件選

15、擇其中一個(gè)執(zhí)行.將選擇結(jié)構(gòu)行為抽象為服務(wù)S,設(shè)其包含n個(gè)進(jìn)行交互的子行為,條件選擇抽象為服務(wù)S中的一組命題,Ps:p,P:p:,:p,簡寫為P,P:,P.將這個(gè)選擇序列中與n個(gè)命題一一對應(yīng)的子行為分別抽象為服務(wù)S,S,S.服務(wù)S的描述為S:=p1Sl+p2s2+pSod)工作單元描述了一組有條件的迭代執(zhí)行的子行為.Guard屬性用來決定一個(gè)重復(fù)迭代是否執(zhí)行;repeat屬性決定迭代執(zhí)行或終止的條件;block屬性用于判定以上兩種條件是否需要等待相關(guān)變量以決定是否繼續(xù)執(zhí)行,描述為S:=ch(.(Ps:gS.!Ps:rS+Ps:g0).3.2BPEL4WS規(guī)范向形式化描述模型的映射用Pi一演算對B

16、PEL4WS規(guī)范進(jìn)行描述的工作已經(jīng)比較成熟,利用這些描述,可以很方便地將BPEL4WS規(guī)范映射到Web服務(wù)形式化描述模型中.所有行為的描述里面,partnerLink,portType,operation指定了Web服務(wù)的訪問點(diǎn),inputVariable指定了發(fā)送的調(diào)用參數(shù),outputVariable指定了接收的調(diào)用結(jié)果.將每個(gè)行為抽象為服務(wù)S.發(fā)送的調(diào)用參數(shù)抽象為:inVar,簡寫為inVar.接收的調(diào)用結(jié)果抽象為:outVar,簡寫為outVar.將由partner-Link,portType和operation指定的固定通信信道抽象為0s;chn,將其簡寫為chn,用來發(fā)送inVar

17、.用來接收調(diào)用結(jié)果的動態(tài)通信信道抽象為:let,簡寫為let.a)Invoke行為表示服務(wù)通過chn信道發(fā)送調(diào)用參數(shù)inVar,并提供一個(gè)接收返回結(jié)果outVar的信道.相應(yīng)地描述為S:chn(inVar).ehn(1et).1et(outVar).0ob)Receive行為表示從chn信道接收調(diào)用參數(shù)inVar,若沒有相應(yīng)reply行為與其對應(yīng),但又需要輸出返回結(jié)果時(shí),receive還需要從chn接收一個(gè)輸出結(jié)果的信道let,描述為S:=ehn(inVar).chn(1et).1et(outVar)0;如果receive行為有相應(yīng)reply行為對應(yīng),則由對應(yīng)的reply行為進(jìn)行返回結(jié)果的輸出

18、,那么相應(yīng)地描述為S:=chn(inVar).0.C)Reply行為需要從chn信道接收一個(gè)用于接收返回結(jié)果outVar的信道let.描述為S:=chn(ret).1et(Var).0.d)Assign行為表示在服務(wù)內(nèi)部變量間的賦值動作是在服務(wù)外界無法觀察到的內(nèi)部行為,只能用下面的方法來模擬變量間的賦值,其中的信道是外界不可見的.相應(yīng)地描述為S:=ch(1).0Ich(2).0.e)Empty行為代表一個(gè)沒有任何動作的行為,可以用已經(jīng)結(jié)束了的服務(wù)對其進(jìn)行描述,其對應(yīng)的描述為S:=0.f)Sequence結(jié)構(gòu)定義了一組順序執(zhí)行的子行為,其對應(yīng)的描述為S:=S】.S2.S.g)Flow結(jié)構(gòu)定義了一

19、組并發(fā)執(zhí)行的子行為,其對應(yīng)的描述為|s:1IS21.?lS.h)Switch結(jié)構(gòu)根據(jù)一個(gè)或多個(gè)選擇條件分支,從若干個(gè)子行為中選擇一個(gè)執(zhí)行,其中各個(gè)不同的命題對應(yīng)多個(gè)選擇分支.對應(yīng)的描述為S:S+P-P2p.S.i)While結(jié)構(gòu)表示其包含的子行為被重復(fù)執(zhí)行,直到某個(gè)條件不再滿足時(shí)停止.其相應(yīng)的描述為5:=!p5+JD0.4WS.CDL規(guī)范和BPEL4WS規(guī)范在Web服務(wù)的形式化模型中的一致性上章將與Web服務(wù)組合結(jié)構(gòu)相關(guān)的BPEIAWS規(guī)范的行為以及WSCDL規(guī)范的主要元素都在Web服務(wù)形式化描述模型中作了映射.基于這個(gè)映射,本章分析這兩種基于不同角度對Web服務(wù)組合進(jìn)行描述的規(guī)范的主要行為的

20、對應(yīng)關(guān)系,而后通過第四方物流管理平臺的例子說明用這兩種不同規(guī)范描述的同一Web服務(wù)組合在Web服務(wù)形式化描述模型中是一致的.WSCDL和BPEIAWS規(guī)范的主要交互行為在Web服務(wù)形式化描述模型中的對應(yīng)關(guān)系為:a)WSCDL規(guī)范的requestrespondinteraction中的fromRole對應(yīng)BPEIAWS規(guī)范的invoke,在模型中描述為S=chl(1).chl(ch2).ch2(4).S1;toRole對應(yīng)receive+reply,描述為S2:=ch1(2).chl(ch2).ch2(3).S2.b)WSCDL規(guī)范的requestinteraction中的fromRole對應(yīng)B

21、PEL4WS規(guī)范的invoke,在模型中描述為S=ch】(】).cl(c).c2(V4).S1;toRole對應(yīng)receive,在模型中描述為S2:=chl(口2).ch1(ch2).ch2().S2.e)WSCDL規(guī)范的respondinteraction中的fromRole對應(yīng)BPEL4WS規(guī)范的receive,在模型中描述為S1:=ch2(4).Sl;toRole對應(yīng)reply,描述為S2:=ch.(ch2).().S2.為了說明對同一個(gè)Web服務(wù)組合,采用上述兩種規(guī)范進(jìn)行描述之后,在Web服務(wù)形式化描述模型中的映射具有一致性,本節(jié)用一個(gè)第四方物流管理平臺的例子進(jìn)行說明.最后指出如果這一

22、管理平臺的體系結(jié)構(gòu)在實(shí)際應(yīng)用中是動態(tài)的,那么上述兩種規(guī)范均無法體現(xiàn),但是直接使用Web服務(wù)形式化描述模型的行為結(jié)構(gòu)就可以描述這一動態(tài)結(jié)構(gòu).4.1WSCDL規(guī)范描述的第四方物流管理平臺本文從全局的角度考慮第四方物流管理平臺的例子,其四個(gè)角色之間基于全局的交互如圖1所示.圖中每一個(gè)方框代表一個(gè)服務(wù),實(shí)線為服務(wù)間固定的通信信道,虛線為動態(tài)信道,即從客戶角度來看,與其交互的是一個(gè)組合服務(wù),通信的信道是leq和ack,而組合服務(wù)內(nèi)部的信道reqs,sresp,pay和payr對客戶來講是不可見的.一一一ER$!一圖1第四方物流管理平臺基于全局的交互協(xié)作?2172?計(jì)算機(jī)應(yīng)用研究第28卷在wS.cDL描述

23、文檔中,除了本文提到的與Web服務(wù)組合的結(jié)構(gòu)相關(guān)的活動和結(jié)構(gòu)之外,還有大量的其他屬性信息,這些信息不是本文研究的重點(diǎn),而且其存在會使得結(jié)構(gòu)不明顯.因此,用如下函數(shù)的形式對本文提到的WSCDL中的活動和結(jié)構(gòu)進(jìn)行簡單說明,其中各個(gè)變量的說明與前面相同.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)兩個(gè)活動順序執(zhí)行,用”.”連接;兩個(gè)活動并發(fā)執(zhí)行,用“連接;兩個(gè)活動選擇執(zhí)行,用”+”連接,判斷條件用命題表示.基于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)將以上描述對應(yīng)成Web服務(wù)形式化

25、描述模型中的行為結(jié)構(gòu),可以分別得到SS,S和,這里取最復(fù)雜的用于后面的說明.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規(guī)范描述的第四方物流管理平臺第四方物流管理平臺用BPEIAW

26、S規(guī)范描述的業(yè)務(wù)流程如圖2所示.一I.!一ilogistics1圖2BPEL4WS規(guī)范描述的4PL業(yè)務(wù)流程可以采用自頂向下的方法將上述BPEIAWS描述的業(yè)務(wù)流程從根節(jié)點(diǎn)元素開始依次對應(yīng)到Web服務(wù)形式化描述模型中,這個(gè)過程不在這里贅述.得到的描述如下: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兩種規(guī)范的映射之間的比較將由BPEL4WS和WSCDL規(guī)范描述得到的映射用一演算的自動驗(yàn)證工具M(jìn)WB進(jìn)行deadlocks命令檢查,發(fā)現(xiàn)由WSCDL規(guī)范描述得到的映射存在著死鎖.其中一些動作的先后順序需要進(jìn)行調(diào)整.比如其映射的ack(respondm),表示要從信道ack1中發(fā)送信息respondm,但此時(shí)respondm是在后面的動作resp(respondm)中得到的.這種動作的前后順序問題是由于嚴(yán)格按照了WSCDL規(guī)范映射中的動作順序,但在實(shí)際的應(yīng)用過程中,產(chǎn)生調(diào)用操作的服務(wù)應(yīng)該是在執(zhí)行

28、完了所有的動作之后再考慮返回結(jié)果的接收問題,也就是說產(chǎn)生調(diào)用操作的服務(wù),其對應(yīng)的動作序列S=ch().ch,(ch).ch().S在實(shí)際生成映射時(shí),應(yīng)該變?yōu)镾=(,).s.兩(c2).ch2(4).經(jīng)過變化之后,兩種描述的映射都不存在死鎖,再運(yùn)行weq命令,可以得到經(jīng)過修改之后的兩個(gè)Web服務(wù)組合的描述是弱相似的.前面的例子中只考慮了第四方物流管理平臺的服務(wù),沒有考慮第三方物流的服務(wù),銀行的服務(wù)以及用戶的操作.后面三個(gè)服務(wù)的結(jié)構(gòu)比第四方物流管理平臺的服務(wù)要簡單許多,根據(jù)前面的映射原則,仍然可以得到兩個(gè)規(guī)范描述的映射結(jié)果完全一致的結(jié)論.4.4動態(tài)體系結(jié)構(gòu)的描述方法再回到前面說的第四方物流管理平臺

29、的例子本身,無論是WSCDL規(guī)范描述的業(yè)務(wù)流還是BPEIAWS規(guī)范描述的業(yè)務(wù)流,都存在著如下事實(shí):用戶和第三方物流以及銀行的所有交互數(shù)據(jù)都要通過第四方物流管理平臺,這在實(shí)際應(yīng)用上并不合理,尤其是當(dāng)一些交換的數(shù)據(jù)涉及到用戶個(gè)人隱私的時(shí)候.基于上述考慮,第四方物流管理平臺應(yīng)該在用戶需要與銀行(第三方物流)進(jìn)行數(shù)據(jù)交互時(shí),在用戶和銀行(第三方物流)之間建立一個(gè)臨時(shí)通信的信道,使得用戶可以直接與銀行(第三方物流)進(jìn)行交互,而不需要經(jīng)過第四方物流管理平臺的轉(zhuǎn)發(fā),這樣可以避免個(gè)人隱私信息的泄露,保證了整個(gè)業(yè)務(wù)流程的數(shù)據(jù)安全性.而一旦這種動態(tài)連接信道建立起來,那么整個(gè)系統(tǒng)的體系結(jié)構(gòu)也就發(fā)生了相應(yīng)的變化.無論

30、是wsCDL還是BPEIAWS規(guī)范,都無法描述這種動態(tài)體系結(jié)構(gòu)的建立.但是直接從Web服務(wù)形式化描述模型出發(fā),可以直接用動作序列去描述這種動態(tài)的體系結(jié)構(gòu).這種動態(tài)體系結(jié)構(gòu)的變化如圖3所示,(a)表示沒有建立動態(tài)信道的結(jié)構(gòu),(b)是第四方物流管理平臺傳遞了信道之后形成的新的體系結(jié)構(gòu).進(jìn)行了信道傳遞之后,臨時(shí)信道ack,sresp和pay就斷開了鏈接,而產(chǎn)生了ltoc和btoc兩個(gè)臨時(shí)的信道,分別連接用戶和第三方物流以及銀行,進(jìn)行以后的數(shù)據(jù)交互.第四方物流管理平臺在調(diào)用第三方物流以及銀行服務(wù)之后,并不直接從臨時(shí)信道sresp和payr接收第三方物流或者銀行的數(shù)據(jù),而是接收一個(gè)他們的通信信道,保存在

31、變量W.和W:中.而后,從用戶接收臨時(shí)信道ack.和ack:(保存在變量C和b中),并通過這兩個(gè)信道將變量W,和W發(fā)送給用戶.具體的描述如下:SM:req(orderm).(p1(req(detailm).酈(detailm).(sresp).sresp(W1).req(c1).第6期胡靜,等:基于Pi一演算的Web服務(wù)形式化描述模型?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】第四方物流管理平臺靜態(tài)體系結(jié)構(gòu)(b)第四方物流管理平臺動態(tài)體系結(jié)構(gòu)圖3體系結(jié)構(gòu)相應(yīng)的第三方物流,銀行的服務(wù)和用戶需求的具體描述如下:S=PI(reqs(detail1).reqs(cm).cfft(hoc)(reqs(search1).reqs(cm).em(1toc).hoc(gps1)互,組合成新的Web服務(wù),因此,其功能和結(jié)構(gòu)可以通過其交互行為來描述.b)用操作語義來描述Web服務(wù)發(fā)生組合時(shí)交互的規(guī)則.操作語義描述了Web服務(wù)發(fā)生相應(yīng)的動作之后的遷移,以及發(fā)生交互行為之后整個(gè)系統(tǒng)體系結(jié)構(gòu)的變化.e)給出現(xiàn)有的基于全局描述Web服務(wù)組合的WSCD

33、L規(guī)范和基于局部描述Web服務(wù)組合的BPEIAWS規(guī)范在本模型中的映射結(jié)構(gòu),使得用戶可以將現(xiàn)有的基于組合規(guī)范的描述映射為本模型中的描述方法,使用Pi一演算的自動驗(yàn)證工具,在Web服務(wù)組合真正執(zhí)行之前進(jìn)行驗(yàn)證.而且這兩種基于不同角度的描述在本模型中的映射結(jié)構(gòu)具有一致性.d)利用此模型的描述方法直接描述具有動態(tài)體系結(jié)構(gòu)的Web服務(wù)組合.已有的Web服務(wù)組合描述規(guī)范都無法描述由動態(tài)通信信道帶來的Web服務(wù)組合體系結(jié)構(gòu)的動態(tài)性.本文的模型可以方便地進(jìn)行動態(tài)體系結(jié)構(gòu)的描述.參考文獻(xiàn):1岳昆,王曉玲,周傲英.Web服務(wù)核心支撐技術(shù):研究綜述J.軟件,2004,15(3):428.442.2BERARDID

34、,CALVANESED,DeGIACOMOG,eta1.AutomaticservicescompositionbasedonbehaviordescriptionsJ.InternationalJournalofCooperativeInformationSystems,2005,14(4):333.376.1而(respond1)+P23張文濤,彭泳,陳俊亮.會話類E-Service的接口兼容和服務(wù)組合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保存從第四方物流管理平臺接收的返回信道,其與用戶交互的