论文部分内容阅读
WS—CDL从全局的观点定义了P2P协作实体通用的外部行为，这些外部行为以消息交换序列的形式来达到一个共同的交易目的。尽管WS—CDL声称是基于Pi-演算的，但是证明Pi-演算在建模WS—CDL的效力上做的实质性工作并不多。因此，提出了一种基于Pi-演算的方法来形式化并且验证WS—CDL编舞。该方法可以保证WS—CDL编舞的正确性以降低由于web服务执行的失败带来的开销。这一方法提高了部署的效率，降低了实现和调用不合适Web服务的风险。论文的贡献可以归纳为以下三点：首先，用Pi-演算形式化WS—CDL的语