基于多元Pi-演算的Web服務(wù)形式化描述模型及其驗(yàn)證

摘要：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)證方法。最后通過例子說明，提出的定義和判斷方法的有效性。