面向服务计算是下一代基于互联网的全新软件体系结构。它具有分布、共享、健壮、可扩展、可移植、互操作等特性。这些特性主要来自服务的互操作特性和复合特性。面向服务计算目前主要实现方式是基于Web服务。Web服务是分布、独立的代码片断，通过相互交换信息来完成一个特定任务。不同于传统的软件组件，Web服务可以通过互联网进行交互。Web服务的实现得益于Web服务标准的发布，主要是三个基础协议：内容使用格式无关的XML;网络资源的命名使用URI;消息的传递使用HTTP或SOAP。Web服务标准包括：Web服务接口描述WSDL、语义Web服务等。然而，Web服务实现复杂功能的关键是将功能单一的多个Web服务复合为功能复杂的Web服务。因此，Web服务中关键技术是Web服务复合。目前W3C等组织主要有两种候选方案：WS-BPEL和WS-CDL。WS-CDL是交互描述语言，称为Web服务编排(Choreography)。它从全局的角度来看Web服务复合，通过WS-CDL描述可以保证多个Web服务交互的无死锁、活锁、公平等性质。其WorkUnit提供模块复用功能。WS-CDL的主要特色包括WorkUnit和基于信息对齐交互。WS-BPEL称为Web服务编制(Orchestration)执行语言。它是从一个参与者的角度来实现Web服务的复合功能。　　 Web服务标准中存在定义不严谨的情况，即没有给出WS-BPEL和WS-CDL的严谨语义，其结果可能导致几个简单Web服务间复合存在不兼容的情况，这样就有必要采用严密的形式化方法来描述验证Web服务编排复合性质。　　 进程代数是用代数方法对分布与并发系统进行研究。进程是进程代数的元素，进程代数可以通过给定公理和复合算子的方法来定义。常见复合算子包括：顺序、并行、随机选择、递归演算。这样就可以用功能强大的代数规格说明来描述系统，并可以验证系统性质。　　 本文以Web服务编排复合方法为研究对象，以Web服务编排复合为目标，研究基于进程代数的Web服务编排复合关键方法和技术。主要贡献与创新如下：　　 1)提出了基于进程代数的Web服务(Process Algebra for Web Service-PA4WS)形式化模型，给出了PA4WS的语法模型、语义模型、类型理论、子类型关系和递归类型的子类型关系四部分。　　 2)PA4WS语法模型中，和已有的研究成果相比，除常规的输入、输出等基本交互外，在借用服务（会话）通道概念描述基本交互基础上，新增WorkUnit算子。会话是对无限制、复杂交互进行封闭的较常规抽象方法，它的引入保证了服务中的数据无关性和数据能够被隐式创建；WorkUnit算子的引入可方便地描述Web服务交互的异步性质。更重要的是，就我们所知，这是首次借助WorkUnit算子形式化描述了Web服务编排中基于信息对齐的交互。　　 3)在PA4WS语义模型中，定义了其结构化小步操作语义，并给出PA4WS自由变量、受囿变量、结构化同余关系的定义、相关的代数性质及其证明。　　 4)在类型理论中，基于基础公理的类型描述框架，给出PA4WS类型环境推演构造规则、值推演规则和类型推演规则等理论体系。基于结构归纳法和规则归纳法等证明论方法给出PA4WS类型理论的健全性检查、进程项同余关系一致性和进程项归约关系一致性等相关性质证明。　　 5)在子类型关系和递归类型的子类型关系部分，基于（逆像）良基归纳法和余归纳法，证明了带递归算子的子类型关系与正则树子类型是一致的。　　 6)基于javacc和vizgraph，开发了简化版PA4WS到执行树的图形化表示Java原型系统，执行树图形化表示采用dot语言。　　 最后，通过一个电子商务实例建模和基于信息对齐的交互建模来说明PA4WS带来的优点。