摘要:web服務(wù)組合在運(yùn)行時(shí)多發(fā)生由于類型不匹配而產(chǎn)生的錯(cuò)誤,為了有效地避免這種錯(cuò)誤,在哆元Pi-演算的基礎(chǔ)上提出了web服務(wù)形式化描述模型。通過基本類型定義、語法定義和判定規(guī)則說明單個(gè)web服務(wù)的類型良好性,通過操作語義說明web服務(wù)發(fā)生組合時(shí)的類型良好性;給出web服務(wù)可替換性定義,并在此定義基礎(chǔ)上說明如何進(jìn)行web服務(wù)組合的功能驗(yàn)證。提出的類型化web服務(wù)形式化描述模型,準(zhǔn)確說明了web服務(wù)組合運(yùn)行時(shí)的類型良好性,以及web服務(wù)組合的功能驗(yàn)證方法。最后通過例子說明,提出的定義和判斷方法的有效性。