Abstract: The Web Services Choreography Description Language（WS-CDL） provides a mode to describe peer-to-peer collaborations of parties by defining，from a global view，their common and complementary observable behavior；where ordered message exchanges result in accomplishing a common business goal.Though the WS-CDL is claimed to be based on pi-calculus，but little solid work have been done to prove the effectiveness of pi-calculus in modeling WS-CDL.This paper proposes a pi-calculus based approach to formalization and verification of the WS-CDL.The presented method will ensure the correctness of WS-CDL before executing it so that the cost induced by the failures of the web services executing will decrease.This approach increases efficiency during deployment and lowers the risk of implementing and activating noncompliant web services.The contribution of the work can be concluded in three points.First，the semantics of WS-CDL is fully formalized with Pi-calculus；Secondly，the soundness of the formalization is validated and important properties are proved to be preserved in the formalization；Third，a concrete scenario is illustrated to show how model checking is applied to verify the reliability of WS-CDL model designs.

Key words: verification, Pi-calculus, WS-CDL, Web services composition

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

关键词: 验证, Pi-演算, WS-CDL, Web服务组合