基于多元Pi-演算的Web服務形式化描述模型及其驗證

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