基于多元Pi演算的Web服务形式化描述模型及其验证*

Web服务组合在运行时多发生由于类型不匹配而产生的错误，为了有效地避免这种错误，在多元Pi-演算的基础上提出了Web服务形式化描述模型。通过基本类型定义、语法定义和判定规则说明单个Web服务的类型良好性，通过操作语义说明Web服务发生组合时的类型良好性；给出Web服务可替换性定义，并在此定义基础上说明如何进行Web服务组合的功能验证。提出的类型化Web服务形式化描述模型，准确说明了Web服务组合运行时的类型良好性，以及Web服务组合的功能验证方法。最后通过例子说明，提出的定义和判断方法的有效性。