胡 靜，饒國(guó)政，馮志勇

基于多元Pi-演算的Web服務(wù)組合描述與驗(yàn)證

胡 靜，饒國(guó)政，馮志勇

(天津大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，天津 300072)

驗(yàn)證問(wèn)題是Web服務(wù)發(fā)展中亟待解決的關(guān)鍵問(wèn)題之一，類型系統(tǒng)的加入以及Web服務(wù)動(dòng)態(tài)的體系結(jié)構(gòu)給問(wèn)題的解決增添了很多難度．針對(duì)上述問(wèn)題，在多元Pi-演算的基礎(chǔ)上給出Web服務(wù)的描述模型和子類型關(guān)系定義，并對(duì)Web服務(wù)的相容性進(jìn)行細(xì)化，給出Web服務(wù)可替換性定義；基于這些模型和定義，給出Web服務(wù)構(gòu)造時(shí)類型正確性的判定規(guī)則和運(yùn)行時(shí)可替換性的判定方法；最后用1個(gè)例子說(shuō)明上述規(guī)則和方法的可行性．結(jié)果表明上述模型、定義和方法為解決動(dòng)態(tài)的、類型化的Web服務(wù)驗(yàn)證問(wèn)題提供了理論依據(jù)和基礎(chǔ)．

多元Pi-演算；Web服務(wù)驗(yàn)證；Web服務(wù)可替換性

Web服務(wù)組合在面向服務(wù)的計(jì)算(serviceoriented computing，SOC)模型下，無(wú)縫地訪問(wèn)眾多分布式服務(wù)，滿足了日益復(fù)雜和精巧的業(yè)務(wù)需求．基于全局和局部?jī)蓚€(gè)不同視角產(chǎn)生的Web服務(wù)組合描述規(guī)范，使得驗(yàn)證問(wèn)題和合成問(wèn)題變得非常具有挑戰(zhàn)性[1]．驗(yàn)證問(wèn)題，即驗(yàn)證某一個(gè)編排或者編制在關(guān)鍵系統(tǒng)屬性方面是否正確或者他們是否互相一致；合成問(wèn)題，即決定一個(gè)編排是否可以由某個(gè)編制進(jìn)行實(shí)現(xiàn)，如果可能的話，合成一個(gè)編制的原型．

針對(duì)第1個(gè)問(wèn)題的建模和形式化驗(yàn)證的研究工作主要集中在使用有限狀態(tài)自動(dòng)機(jī)[2]、進(jìn)程代數(shù)[3]、 Petri網(wǎng)[4]、有向圖[5]等形式化方法方面．

一些驗(yàn)證工作將WS-BPEL和WS-CDL用形式化方法描述，并且使用已有的模型檢測(cè)工具進(jìn)行驗(yàn)證，這些工具有Uppaal[6]、Java Path Finder[7]或者是NusMVC[8]．然而這些形式化方法和驗(yàn)證工具并不是針對(duì)Web服務(wù)組合而設(shè)計(jì)的驗(yàn)證和優(yōu)化方法．

還有一些驗(yàn)證方法是專門針對(duì)Web服務(wù)組合的特性提出的．文獻(xiàn)[9]從全局和局部2個(gè)不同的視角提出形式化方法和基于符號(hào)模型檢測(cè)的一致性檢查．在文獻(xiàn)[10]中一致性的概念是通過(guò)自動(dòng)機(jī)定義的，而且僅限于2個(gè)服務(wù)之間的組合．文獻(xiàn)[11]用Petri網(wǎng)的方法對(duì)Web服務(wù)組合進(jìn)行形式化描述，其工作集中在檢查編排中的規(guī)范在運(yùn)行時(shí)是否被遵守．

Foster等建立Web服務(wù)有限狀態(tài)進(jìn)程(FSP)，并采用基于FSP的驗(yàn)證技術(shù)來(lái)對(duì)Web服務(wù)進(jìn)行驗(yàn)證，確定了在Web服務(wù)驗(yàn)證中的資源約束模型[12]和驗(yàn)證方法，并開(kāi)發(fā)了名為L(zhǎng)TSA-WS[13]的工具．

這些方法大多是針對(duì)在Web服務(wù)組合對(duì)服務(wù)的固定綁定前提之上的．而在實(shí)際應(yīng)用中，Web服務(wù)組合中各個(gè)Web子服務(wù)之間的綁定關(guān)系是松耦合的，允許人們可以隨時(shí)隨地根據(jù)業(yè)務(wù)流程的需要在網(wǎng)上動(dòng)態(tài)地發(fā)現(xiàn)和綁定Web子服務(wù)．

Pi-演算的特性使其可以很好地描述Web服務(wù)組合這種基于交互建立的動(dòng)態(tài)體系結(jié)構(gòu)．當(dāng)前，基于Pi-演算的Web服務(wù)組合形式化驗(yàn)證的工作主要是根據(jù)Pi-演算中定義的進(jìn)程弱等價(jià)性質(zhì)定義Web服務(wù)組合的相容性[14-15]，并通過(guò)相容性來(lái)驗(yàn)證Web服務(wù)組合的運(yùn)行過(guò)程和功能；或者是直接利用Pi-演算的自動(dòng)驗(yàn)證工具M(jìn)WB，通過(guò)對(duì)Web服務(wù)組合弱等價(jià)性的自動(dòng)驗(yàn)證來(lái)完成對(duì)Web服務(wù)組合的行為驗(yàn)證和功能驗(yàn)證[16]；或者基于類型化的Pi-演算對(duì)Web服務(wù)組合進(jìn)行形式化建模[17]和相容性分析．

上述工作存在3方面的問(wèn)題：①引入的類型系統(tǒng)不是強(qiáng)類型系統(tǒng)，即沒(méi)有描述信道類型和值類型之間的關(guān)系，使得當(dāng)Web服務(wù)組合描述中把信道作為輸入/輸出對(duì)象的動(dòng)作時(shí)，類型系統(tǒng)無(wú)法進(jìn)行類型相容性的判定；②定義的相容性驗(yàn)證的前提要求被驗(yàn)證的進(jìn)程輸入、輸出動(dòng)作的執(zhí)行順序和信道名稱都必須相匹配，而在實(shí)際的Web服務(wù)組合應(yīng)用中，有些動(dòng)作是用來(lái)建立臨時(shí)通信信道的，實(shí)現(xiàn)了Web服務(wù)組合動(dòng)態(tài)的體系結(jié)構(gòu)，但由于和具體的業(yè)務(wù)流程無(wú)關(guān)，其位置甚至發(fā)生的先后順序都不固定，就使得現(xiàn)有的Web服務(wù)的相容性驗(yàn)證方法無(wú)法得到正確結(jié)果；③針對(duì)全局和局部?jī)蓚€(gè)不同的視角提出不同的形式化描述方法，而這些描述方法還是基于全局或者局部的，并未降低由于視角不同造成的Web服務(wù)組合描述間相容性驗(yàn)證問(wèn)題的難度．

筆者針對(duì)驗(yàn)證問(wèn)題進(jìn)行研究，基于多元Pi-演算給出Web服務(wù)形式化描述模型的語(yǔ)法定義、子類型關(guān)系定義以及Web服務(wù)可替換性的定義；在以上定義的基礎(chǔ)上給出Web服務(wù)的驗(yàn)證規(guī)則，包括在Web服務(wù)組合構(gòu)造時(shí)的正確性驗(yàn)證規(guī)則和在Web服務(wù)組合運(yùn)行時(shí)的可替換性驗(yàn)證規(guī)則，并給出相應(yīng)的驗(yàn)證方法；最后通過(guò)第四方物流管理平臺(tái)的例子說(shuō)明上述規(guī)則和方法的可行性．

1 基于多元Pi-演算的Web服務(wù)描述模型

基于多元Pi-演算給出Web服務(wù)形式化描述模型的語(yǔ)法定義和子類型關(guān)系定義，并將Web服務(wù)的相容性進(jìn)行細(xì)化，給出Web服務(wù)可替換性的定義．

1.1 Web服務(wù)形式化描述模型的語(yǔ)法定義

服務(wù)可以表示成四元組S=＜I，O，V，B＞．其中，S為服務(wù)的名字；I為服務(wù)的輸入信道集合；O為服務(wù)的輸出信道集合；V為服務(wù)的變量集合；B為服務(wù)的行為集合．對(duì)服務(wù)S的輸入信道集合、輸出信道集合、變量集合和行為集合的引用分別表示為IS、OS、VS和BS，對(duì)相應(yīng)的具體元素的引用分別表示為[IS∶i]，[OS∶o]，[VS∶v]和[BS∶b]．用PS表示與服務(wù)S相關(guān)的命題集合，對(duì)其中某一個(gè)具體命題的引用表示為[PS∶p]．

定義1 Web服務(wù)形式化描述模型，即

其中![PS∶p]S是規(guī)則表達(dá)式!([PS∶p]S+(-[PS∶p]0))的簡(jiǎn)寫(xiě)形式，用來(lái)表示W(wǎng)eb服務(wù)循環(huán)．

1.2 Web服務(wù)形式化描述模型的“信道-變量”子類型關(guān)系定義

在子類型關(guān)系定義中，定義了“信道-信道”的子類型關(guān)系和“變量-變量”的子類型關(guān)系，而在Web服務(wù)體系結(jié)構(gòu)的動(dòng)態(tài)構(gòu)造中，存在著信道和變量的賦值，因此它們之間的子類型關(guān)系亟需定義．

定義2 “信道-變量”子類型關(guān)系Web服務(wù)形式化描述中信道和變量之間的子類型關(guān)系定義為

Web服務(wù)組合進(jìn)行描述時(shí)，服務(wù)之間傳遞的信息包括數(shù)據(jù)和信道．接受者需要用變量來(lái)存儲(chǔ)傳遞過(guò)來(lái)的信道，如果沒(méi)有這幾條規(guī)則，那么服務(wù)類型良好性判斷規(guī)則無(wú)法判斷信道和變量之間的子類型關(guān)系，而無(wú)法適應(yīng)Web服務(wù)組合體系結(jié)構(gòu)的動(dòng)態(tài)生成．1.3 Web服務(wù)可替換性定義

在之前的研究工作中，大部分是用Web服務(wù)的相容性來(lái)說(shuō)明當(dāng)Web服務(wù)組合中某個(gè)Web服務(wù)無(wú)法使用時(shí)，用來(lái)替換的Web服務(wù)是否能夠完成相同功能，并且和其原本環(huán)境交互良好．Web服務(wù)相容性的定義基于Pi-演算中進(jìn)程的弱相似性，相容關(guān)系是對(duì)稱的．Web服務(wù)相容性的定義和判斷方法中只考慮了在交互過(guò)程中能完成相似的功能，沒(méi)有考慮傳遞信息的類型兼容對(duì)相容性判斷造成的影響．在實(shí)際應(yīng)用中，類型不兼容往往是造成運(yùn)行時(shí)錯(cuò)誤的主要因素，為了能夠定義和避免這種由類型不兼容帶來(lái)的影響，就需要在原有的相容性定義中引入類型，將相容性定義進(jìn)行進(jìn)一步細(xì)化．

將Web服務(wù)相容性進(jìn)行細(xì)化，引入對(duì)類型兼容性的判斷，給出Web服務(wù)可替換性的定義，為后面在構(gòu)造時(shí)和運(yùn)行時(shí)進(jìn)行的Web服務(wù)可替換性驗(yàn)證提供理論依據(jù)和基礎(chǔ)．

定義3 Web服務(wù)可替換性T? 設(shè)服務(wù)S和R是弱相似的，去掉所有的內(nèi)部轉(zhuǎn)移之后，服務(wù)S經(jīng)過(guò)n個(gè)動(dòng)作α1，α2，…，αn之后變遷為終止的服務(wù)0，服務(wù)R經(jīng)過(guò)m個(gè)動(dòng)作α’1，α’2，…，α’m之后變遷為終止的服務(wù)0，其中m≥n，且S和R均為類型良好的服務(wù)，則ST?R意味著服務(wù)S可以被服務(wù)R替換，必須要滿足條件為

Web服務(wù)的可替換性是不對(duì)稱關(guān)系，Web服務(wù)的相容性可以通過(guò)可替換性進(jìn)行重新定義：Web服務(wù)S和R是相容的，當(dāng)且僅當(dāng)TS?R并且TR?S．

可替換性的定義表明：

(1) 當(dāng)比較的2個(gè)動(dòng)作同為輸出時(shí)，如果R可以替換S，就要求R的客體類型是S的客體類型的子類型，這樣才能夠保證S的周圍環(huán)境不會(huì)接收類型不兼容的變量；

(2) 比較的2個(gè)動(dòng)作同為輸入時(shí)，如果R可以替換S，就要求S的客體類型是R的客體類型的子類型，這樣才能夠使得R可以接收S周圍環(huán)境發(fā)出的所有類型的變量，而不會(huì)產(chǎn)生不兼容問(wèn)題．

2 基于多元Pi-演算的Web服務(wù)驗(yàn)證

基于多元Pi-演算的Web服務(wù)形式化描述模型不但可以描述Web服務(wù)的交互行為，而且擴(kuò)充了強(qiáng)類型系統(tǒng)，這就使得在對(duì)Web服務(wù)進(jìn)行驗(yàn)證時(shí)，需要同時(shí)考慮行為和類型的正確性和可替換性．

在Web服務(wù)的構(gòu)造時(shí)，行為的正確性和類型的正確性可以分開(kāi)進(jìn)行驗(yàn)證，其中行為正確性的驗(yàn)證規(guī)則可以直接使用Pi-演算對(duì)進(jìn)程正確性的驗(yàn)證規(guī)則，此處不再贅述；在Web服務(wù)的運(yùn)行時(shí)，基于可替換性的定義，行為和類型無(wú)法分開(kāi)進(jìn)行可替換性的驗(yàn)證，需要給出可替換性驗(yàn)證的具體方法．

綜上所述，本節(jié)給出Web服務(wù)構(gòu)造時(shí)的類型正確性驗(yàn)證規(guī)則以及Web服務(wù)運(yùn)行時(shí)可替換性驗(yàn)證方法．2.1 Web服務(wù)構(gòu)造時(shí)類型正確性的驗(yàn)證

在Web服務(wù)的構(gòu)造時(shí)，服務(wù)構(gòu)造符(符號(hào)“|”、“+”和“！”)、τ動(dòng)作以及命題條件并不會(huì)改變Web服務(wù)的正確性．構(gòu)造時(shí)的類型正確性主要是保證一般的輸入輸出動(dòng)作的主體和客體的類型符合如下的子類型關(guān)系．

規(guī)則1

規(guī)則2

規(guī)則指出為了保證服務(wù)的類型良好性，必須滿足：對(duì)于輸出行為(規(guī)則1)，其行為的客體的類型是行為主體可以輸出類型的子類型，對(duì)于輸入行為(規(guī)則2)，其行為的主體可以輸入的類型是行為客體類型的子類型．

2.2 Web服務(wù)運(yùn)行時(shí)可替換性的驗(yàn)證

對(duì)Web服務(wù)可替換性的定義，在Pi-演算進(jìn)程間弱等價(jià)性的基礎(chǔ)上加入了子類型判斷，無(wú)法再利用Pi-演算的自動(dòng)驗(yàn)證工具進(jìn)行可替換性驗(yàn)證．基于對(duì)Web服務(wù)可替換性的定義，將Web服務(wù)的描述動(dòng)作分為和業(yè)務(wù)流程相關(guān)以及和業(yè)務(wù)流程無(wú)關(guān)兩大類，主要對(duì)和業(yè)務(wù)流程相關(guān)的動(dòng)作進(jìn)行可替換性驗(yàn)證，如有名字不匹配，則根據(jù)和業(yè)務(wù)無(wú)關(guān)的動(dòng)作集合進(jìn)行對(duì)應(yīng)和代換．具體的可替換性驗(yàn)證方法描述如下：

(1) 驗(yàn)證前提．Web服務(wù)可替換性定義的基礎(chǔ)是多元Pi-演算中進(jìn)程的弱相似性，進(jìn)程內(nèi)部進(jìn)行數(shù)據(jù)交換的動(dòng)作全部轉(zhuǎn)換成τ．也就是說(shuō)，在對(duì)2個(gè)Web進(jìn)行可替換性判定之前，要完成每個(gè)Web服務(wù)內(nèi)部子服務(wù)間的交互操作，得到其和外部環(huán)境或其他Web服務(wù)進(jìn)行交互的操作序列．

(2) 假設(shè)條件．設(shè)Web服務(wù)S和T均為去掉了內(nèi)部交互動(dòng)作之后的服務(wù)描述，服務(wù)S經(jīng)過(guò)n個(gè)動(dòng)作α1, α2,…,αn之后變遷為終止的服務(wù)0，服務(wù)T經(jīng)過(guò)m個(gè)動(dòng)作α1′, α2′,…,αm′ 之后變遷為終止的服務(wù)0，其中m≥n．

(3) 可替換性算法．Web服務(wù)可替換性的判定算法如下，其中輸入是服務(wù)S和T的描述，輸出是服務(wù)T是否可以替換服務(wù)S．

If(StaticCheck(S)&& StaticCheck(T)

{

ActionDivision(S)；

ActionDivision(T)；

While(SL!=NULL)

{

αi=LS；

αi'=LT；

if(（xi=xi′&& T3≤T4)||(&& T4≤T3)）

LS=LS.next；

else if(（xi≠xi′)||(xi≠xi′)）

{

?aj∈Cs|obj(aj)=xi；

?a′j∈CT|sub(a′j)=sub(aj)；

LT=LT{obj(a′j)/xi}；

CS=CS{aj}；

CT=CT{a′j}；

continue；

}

else return(Err)

}

return(Replaceable)

}

上述算法的步驟和主要方法說(shuō)明如下：

(1) αi的表示形式是xi( y)或xi( y)．ΓS|-y: T3，a′j的表示形式是xi'(y')或xi'(y')．ΓT|-y':T4．

(2) 先要完成對(duì)服務(wù)S和T的構(gòu)造時(shí)正確性檢查，包括類型正確性和行為正確性．方法StaticCheck確保現(xiàn)有描述的類型完全符合Web服務(wù)的類型良好性判斷準(zhǔn)則，并且行為不存在死鎖．

(3) 根據(jù)是否和業(yè)務(wù)流程相關(guān)完成對(duì)服務(wù)S和T中動(dòng)作的劃分，用列表的形式保存和業(yè)務(wù)流程相關(guān)的動(dòng)作序列，和業(yè)務(wù)流程無(wú)關(guān)的動(dòng)作用集合保存即可．方法ActionDivision對(duì)S和T中的動(dòng)作進(jìn)行劃分，得到服務(wù)列表SL和TL，存儲(chǔ)S和T中所有與業(yè)務(wù)流程相關(guān)的動(dòng)作序列；得到集合SC和TC，存儲(chǔ)服務(wù)S和T中構(gòu)建臨時(shí)通信信道的動(dòng)作集合．

(4) 在進(jìn)行可替換性比對(duì)時(shí)，如果當(dāng)前的動(dòng)作同為輸入或者輸出，并且信道名稱相同，則只需要滿足Web服務(wù)可替換性中定義的子類型關(guān)系即可；如果當(dāng)前的動(dòng)作同為輸入或者輸出，但信道名稱不同，則表明在此位置之前可能有臨時(shí)信道的建立，通過(guò)通信信道主體和客體的對(duì)應(yīng)關(guān)系，找到在T中和S相應(yīng)的信道名稱，并完成對(duì)T中信道名稱的替換，而后進(jìn)入下一次的對(duì)比工作；如果當(dāng)前的動(dòng)作不同為輸入或者輸出，那么就說(shuō)明服務(wù)T一定不能替換服務(wù)S．

3 Web服務(wù)組合驗(yàn)證的實(shí)例說(shuō)明

以第四方物流管理平臺(tái)作為實(shí)例，主要說(shuō)明判斷Web服務(wù)的可替換性算法中動(dòng)作劃分的必要性．第四方物流管理平臺(tái)的體系結(jié)構(gòu)如圖1所示．每一個(gè)方框代表一個(gè)服務(wù)，實(shí)線為服務(wù)間固定的通信信道，虛線為動(dòng)態(tài)信道，即從客戶角度來(lái)看，與其交互的是一個(gè)組合服務(wù)，通信的信道是req和ack，而組合服務(wù)內(nèi)部的信道reqs、sresp、pay和payr對(duì)客戶來(lái)講是不可見(jiàn)的．

圖1 第四方物流管理平臺(tái)的全局交互協(xié)作Fig.1 Global interaction of 4,PL

用BPEL4WS和WS-CDL分別對(duì)第四方物流管理平臺(tái)的Web服務(wù)組合方式進(jìn)行描述，采用文獻(xiàn)[14]中描述的規(guī)范標(biāo)簽和Pi-演算中動(dòng)作的對(duì)應(yīng)關(guān)系，對(duì)具有嵌套結(jié)構(gòu)的描述文檔進(jìn)行自頂向下的掃描分析方法，可以得到2個(gè)從不同角度對(duì)同一服務(wù)組合進(jìn)行描述的Pi-演算描述方法．

從BPEL4WS文檔得到的描述為

從WS-CDL得到的描述為

首先，對(duì)Web服務(wù)MS和MS′進(jìn)行構(gòu)造時(shí)的正確性驗(yàn)證．使用Pi-演算的自動(dòng)驗(yàn)證工具M(jìn)WB中的deadlock命令驗(yàn)證可知MS和MS′均不存在死鎖，其構(gòu)造時(shí)動(dòng)作具有正確性；從WS-CDL和BPEL4WS文檔中解析得到每個(gè)名字的變量，根據(jù)子類型關(guān)系規(guī)則進(jìn)行判斷，可知其構(gòu)造時(shí)類型關(guān)系也具有正確性．

對(duì)Web服務(wù)MS和MS′進(jìn)行運(yùn)行時(shí)的可替換性驗(yàn)證．使用之前研究成果中對(duì)相容性驗(yàn)證的方法，在MWB中運(yùn)行weq命令，可知2個(gè)服務(wù)不是弱等價(jià)的，從而無(wú)法得到2個(gè)服務(wù)相容的結(jié)果．這是因?yàn)?個(gè)服務(wù)在用戶和銀行之間建立通信信道的動(dòng)作順序不相同．即MS的

中動(dòng)作的順序不同．

用可替換性算法對(duì)這2個(gè)服務(wù)重新進(jìn)行檢測(cè).在此重點(diǎn)描述以上2個(gè)出現(xiàn)問(wèn)題的分支．在SM的分支中，筆者將和業(yè)務(wù)無(wú)關(guān)的動(dòng)作進(jìn)行劃分，得到建立臨時(shí)信道的動(dòng)作集合為{reqs(sresp)，sresp(ask1)}，同樣的在SM′的分支中得到建立臨時(shí)信道的動(dòng)作集合為{reqs(sresp)，sresp(cl)}．在可替換性算法比對(duì)期間，用SM動(dòng)作集合中的ask1替換SM′的cl，然后再繼續(xù)進(jìn)行比對(duì)，可以得到服務(wù)SM可以被服務(wù)SM′替換．使用同樣的方法可以得到服務(wù)SM′也可以被SM替換，由此得到服務(wù)SM和SM′是相容的．

4 結(jié) 語(yǔ)

在實(shí)際的Web服務(wù)組合中，除了發(fā)生由于數(shù)據(jù)類型不匹配產(chǎn)生的錯(cuò)誤，由于發(fā)生交互的行為順序不同，而有些順序不同的動(dòng)作是和業(yè)務(wù)流程無(wú)關(guān)的，其動(dòng)作的位置順序是可以發(fā)生變化的，這就使得使用傳統(tǒng)的相容性驗(yàn)證方法會(huì)把很多原本可替換的服務(wù)判斷為不可替換．

基于多元Pi-演算提出Web服務(wù)的描述模型以及子類型關(guān)系的判定規(guī)則，對(duì)Web服務(wù)的相容性進(jìn)行細(xì)化，給出Web服務(wù)可替換性的定義；針對(duì)Web服務(wù)描述動(dòng)作的主體類型和客體類型之間的關(guān)系，給出在Web服務(wù)構(gòu)造時(shí)類型正確性驗(yàn)證規(guī)則；根據(jù)業(yè)務(wù)流的相關(guān)性將Web服務(wù)描述的動(dòng)作進(jìn)行劃分，針對(duì)業(yè)務(wù)流程相關(guān)動(dòng)作進(jìn)行運(yùn)行時(shí)的可替換性驗(yàn)證，期間，根據(jù)業(yè)務(wù)流程無(wú)關(guān)動(dòng)作，進(jìn)行Web服務(wù)描述名字的代換，而后在新的代換下進(jìn)行可替換性驗(yàn)證；最后第四方物流管理平臺(tái)的例子說(shuō)明了上述驗(yàn)證方法中動(dòng)作劃分和代換的可行性．

［1］ Sun Jun，Liu Yang，Jin Songdong，et al. Model-based methods for linking Web service choreography and orchestration[C] //The 17th Asia Pacific Software Engineering Conference. Sydney，Australia，2010：166-175.

［2］ Fu Xiang，Bultan Tevfik，Su Jianwen，et al. Analysis of interacting BPEL web services[C] //Proceedings of the 13th International Conference on World Wide Web 2004. New York，USA：ACM Press，2004：621-630.

［3］ Liu Fangfang，Zhang Liang，Shi Yuliang，et al. Formal analysis of compatibility of Web services via CCS[C] //Proceedings of the International Conference on Next Generation Web Services Practices. Washington，USA：IEEE Computer Society Press，2005：143-148.

［4］ 錢柱中，陸桑璐，謝 立. 基于Petri網(wǎng)的Web服務(wù)自動(dòng)組合研究[J]. 計(jì)算機(jī)學(xué)報(bào)，2006，29(7)：1057-1066.

Qian Zhuzhong，Lu Sanglu，Xie Li. Automatic composition of Petri net based Web services[J]. Chinese Journal of Computers，2006，29(7)：1057-1066(in Chinese).

［5］ Yun Yaoli，Jagadish H V. Compatibility determination in Web services[C]//Proceedings of the First International E-Services Workshop. Pittsburgh，USA，2003：7-15.

［6］ Dong J S，Liu Y. Verification of computation orchestration via timed automata[C]// ICFEM'06 Proceedings of the 8th International Conference on Formal Methods and Software Engineering．Berlin：Springer-Verlag，2006：226-245.

［7］ Pu Geguang，Shi Jianqi，Wang Zheng，et al. The Validation and verification of WSCDL[C] //14th Asia-Pacific Software Engineering Conference．Washington，USA，2007：81-88.

［8］ Kazhamiakin R，Pandya P，Marco Pistore. Representation，verification，and computation of timed properties in Web[C]//ICWS'06 Proceedings of the IEEE International Conference on Web Services．Washington，USA，2006：497-504.

［9］ Kazhamiakin R，Pistore M. Choreography conformanceanalysis：Asynchronous communications and information alignment[C]//WS-FM'06 Proceedings of the Third International Conference on Web Services and Formal Methods．Berlin：Springer-Verlag，2006：227-241.

［10］ Baldoni M，Baroglio C，Martelli A，et al. Verifying the conformance of web services to global interaction protocols：A first step[C] // EPEW'05/WS-FM'05 Proceedings of the 2nd International Workshop on Web Services and Formal Methods．Berlin：Springer-Verlag，2005：257-271.

［11］ Aalst W M P，Dramas M，Onyang C，et al. Conformance checking of service behavior[J]. ACM Transactions on Internet Technology(TOIT)，2008，8(3)：1-30.

［12］ Foster H，Emmerich W，Kramer J，et al. Model checking service compositions under resource constraints [C] //ESEC-FSE '07 Proceedings of the 6,th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering．New York，USA，2007：225-234.

［13］ Foster H，Uchitel S，Magee J，et al. LTSA-WS：A tool for model-based verification of Web service compositions and choreography[C]//ICSE'06 Proceedings of the 28th International Conference on Software Engineering． New York，USA，2006：771-774.

［14］ 胡 靜，馮志勇. 基于Pi-演算的Web服務(wù)形式化描述模型[J]. 計(jì)算機(jī)應(yīng)用研究，2011，28(6)：2168-2173.

Hu Jing，F(xiàn)eng Zhiyong. Pi-calculus based formal description model for Web services[J]. Application Research of Computers，2011，28(6)：2168-2173(in Chinese).

［15］ 辜希武，盧正鼎. Web服務(wù)相容性的形式化描述與分析[J]. 計(jì)算機(jī)工程與應(yīng)用，2007，43(27)：28-33(in

Chinese). Gu Xiwu，Lu Zhengding. Formal description and analysis of Web services compatibility[J]. Computer Engineering and Applications，2007，43(27)：28-33(in Chinese).

［16］ 廖 軍，譚 浩，劉錦德. 基于Pi-演算的Web服務(wù)組合的描述和驗(yàn)證[J]. 計(jì)算機(jī)學(xué)報(bào)，2005，28(4)：635-643.

Liao Jun，Tan Hao，Liu Jinde. Describing and verifying Web service using Pi-calculus[J]. Chinese Journal of Computers，2005，28(4)：635-643(in Chinese).

［17］ 辜希武，盧正鼎. 類型化的Web服務(wù)組合形式化模型[J]. 計(jì)算機(jī)科學(xué)，2008，35(1)：128-134.

Gu Xiwu，Lu Zhengding. A typed formal model for Web services composition [J]. Computer Science，2008，35(1)：128-134(in Chinese).

Polyadic Pi-Calculus Based Description and Verification for Web Service

Hu Jing，Rao Guozheng，F(xiàn)eng Zhiyong
(School of Computer Science and Technology，Tianjin University，Tianjin 300072，China)

Verification is one of the important issues to be addressed in the development of Web services，and type system and the dynamic architecture of Web services，add a lot more difficulty to it. This paper gives the description model of Web services and the subtype relationship defined on the basis of polyadic Pi-calculus，and defines replaceability to refine the concept of compatibility. Based on the above models and definitions，this paper addresses the rules to determining type correctness at construction time of Web services and the method of determining replaceability at run time. Finally，an example illustrates the feasibility of the above-mentioned rules and methods. All of the definitions and methods established in this paper provide a theoretical basis and foundation for solving dynamic and typed Web service verification.

polyadic Pi-calculus；Web service verification；Web services replace-ability

TP301

A

0493-2137(2013)06-0520-06

DOI 10.11784/tdxb20130609

2011-12-08；

2012-04-11.

國(guó)家自然科學(xué)基金資助項(xiàng)目(61003080)；教育部科技發(fā)展中心網(wǎng)絡(luò)時(shí)代科技論文快速共享專項(xiàng)研究課題資助項(xiàng)目(2011117).

胡 靜（1980——），女，講師．

胡 靜，mavis_huhu@tju.edu.cn.