Web服务组合是一种基于面向服务架构的技术,通过把功能单一的单个Web服务组合起来,实现了服务的重用与增值,解决了互联网异构应用的集成和协作问题。Web服务组合的特点包括松耦合,行业支持,高度可集成等。Web服务组合过程非常复杂,涉及多个Web服务的通信协作,导致对Web服务组合的正确性验证将是十分困难的。但是服务组合的正确性问题决定了Web服务组合能否被正确的实施,错误的实施则会给企业带来严重的损失,所以在Web服务组合被正式实施以前对其进行正确性验证是必须的。目前描述Web服务组合的语言使用最为广泛的是WSFL、XLANG、WS-CDL、BPEL等,它们有一个共同的缺点,缺乏形式化的工具对其进行正确性验证。所以对Web服务组合如何进行形式化的建模,以及如何验证模型的正确性成为Web服务组合研究领域的一个重要问题。对形式化建模方法进行了大量研究后,本文提出了一种基于π-演算的Web服务组合的建模方法,并对模型进行验证工作,研究成果包括以下三个方面：(1)基于π-演算的BPEL业务流程的建模本文给出了BPEL一系列关键元素到π-演算的建模方法,实现了π-演算对BPEL的自动化建模。(2)基于π-演算的BPEL业务流程模型验证本文给出了对模型的死锁验证、活锁验证、可达性验证等模型正确性验证的算法,实现了对Web服务组合的正确性验证。(3)WMV工具的设计与实现本文设计并实现了对Web服务组合的π-演算的自动化建模验证的工具—WMV工具。