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