近年来,随着SOA架构和Web服务的广泛深入,如何将Web服务组合按照不同的目标、方式进行组合成为了人们关注的热点。虽然人们对Web服务以及Web服务组合已经有比较充分的研究并且已经付诸实践,但是从Web服务及其组合的研究现状来开,在很大程度上都还停留在非形式化或者半形式化的基础上。另一方面,形式化方法本身对Web服务组合的整个生命周期(即服务定义,服务发现,服务组合,服务验证)都有很好的指导和支持作用。反之,对于形式化方法来说也需要找到其合适的应用场景,并且在对应用的研究中逐步发展和改进自身。本文致力于用扩展的Pi演算对Web服务组合生命周期中各个时期的关键问题进行形式化描述和分析,包括设计时刻的建模、运行时刻的验证、选择时刻的服务选择等。具体来说,主要工作和创新主要包括如下若干方面：(1)针对服务组合的特征,对传统的Pi演算扩展为Pi-beam,包括语法扩展、语义、类型系统等扩展方面。其中语法扩展有带约束的束通道、逻辑并行和逻辑选择；语义扩展有束通道链接语义规则、逻辑并行和逻辑选择的转化规则等；类型扩展包括增加带约束的束通道类型和相关的类型化规则和类型错误规则。(2)为了利用Pi-beam的相关特性并且直观地表示Web服务组合系统的静态特征,我们开发了带标注的进程链接图和它的简化版本,并用它们对Web服务组合中的基本控制流模式进行了统一化的建模。(3)利用Pi-beam的类型系统和规约特性,我们讨论了服务组合的验证问题。类型正确性验证,主要是以进程是否属于良好类型或者推导出错误为依据。根据Pi-beam演化后的形式,可以判断一个组合进程时候是流程正确或者错误。在流程错误的例子中,死锁和活锁问题被重点讨论。尤其是对死锁问题,笔者通过对Pi-beam演算中的进程类型进行进一步扩展,使得组合后的进程表达式的类型可以用于判断死锁甚至是避免死锁。(4)另外一种基于流程正确性的自动组合算法被提出。它基于Pi-beam演算的语义规则的模式匹配,但不需要复杂的定理证明器和推理工具的介入,在时间复杂度上,由于类型的引入,使得搜索空间大幅减少。(5)由于QoS感知的服务组合已经被证明是NP-困难问题,因此大量的启发式算法被用到其上。粒子群优化(PSO)算法是近年来研究得比较多的方法之一。然而大多数研究仅仅局限于怎样使用这类算法和讨论算法的效率,对方法本身的形式化模型讨论的很少。本文在$-代数的启发下,针对PSO这一具体的方法,对Pi-beam演算进行了非功能性扩展,引入了计算QoS和根据QoS进行选择的原语和规则,并且引入了PSO的元搜索过程作为原语。在这个代数的基础上,开发了在抽象语法树基础上的QoS估值算法,并进行了模拟仿真实验。(6)基于在云计算和云服务的实践需要,笔者对Pi-beam演算扩展成高阶分布式Pi演算,它支持类似Lambda演算中的抽象和应用,并且支持代码的移动性。在此基础上提出了高阶Web服务和高阶服务组合的概念,并且给出了形式化描述和相关的架构。