在研究Web服务组合中存在着一个重要问题是怎么样使用进程代数形式化的描述Web服务组合并且证明Web服务组合的正确性。用Pi-演算建模Web服务组合的模型可以用来检查、验证Web服务组合以保证服务组合的正确性。因为Web服务组合关联到很多的Web服务通信协作，这一特征让Web服务组合的验证工作更加艰难。同时Web服务语言是一种基于业务流程的服务组合方法（BPEL4WS），建模理论基础比较薄弱，组合正确性的保证较弱。所以流程的无死锁性、正确性等问题，在它正式被实施前必须得到形式上的建模与检验。对于建模和验证软件系统来说，形式化方法是一种有效的方法，所以对Web服务组合的形式化验证和描述是一个关键的研究领域。保证Web服务组合的正确性以实现服务增值对于Web服务及其组合来说是非常重要的。本文通过Pi-演算来形式化建模和描述Web服务及其组合。文中涉及了Web服务协议栈与Pi-演算的对应关系，同时通过使用Pi-演算建模Web服务组合的规则，说明了怎么样发现通道和代理。文章最后建立了一个实际的模型，并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证。同时运用了Pi-演算互模拟理论对Web服务组合的相容性、行为等价性进行了验证。