Web服务组合的正确性包括动态行为的匹配性和数据类型的一致性。本文定义了一个扩充的Pi2演算类型系统,同时利用该系统对BPEL4WS Web服务组合规范建立了一个类型化的形式化模型,通过该模型能够对Web服务组合的正确性进行验证。最后通过一个案例,给出了对Web服务组合动态行为的匹配性和数据类型的一致性的验证方法。
