胡 靜，饒國政，馮志勇

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

胡 靜，饒國政，馮志勇

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

可替換性的定義表明：

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

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

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

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

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

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

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

規(guī)則1

規(guī)則2

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

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

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

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

(2) 假設(shè)條件．設(shè)Web服務(wù)S和T均為去掉了內(nèi)部交互動作之后的服務(wù)描述，服務(wù)S經(jīng)過n個動作α1, α2,…,αn之后變遷為終止的服務(wù)0，服務(wù)T經(jīng)過m個動作α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)

}

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

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

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

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

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

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

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

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

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

從BPEL4WS文檔得到的描述為

從WS-CDL得到的描述為

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

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

中動作的順序不同．

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

4 結(jié) 語

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

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

［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ù)自動組合研究[J]. 計(jì)算機(jī)學(xué)報，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é)報，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.

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

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

胡 靜，mavis_huhu@tju.edu.cn.