随着开放分布式计算的快速发展，中间件技术已经从面向对象计算的阶段发展到了面向服务计算(Service-Oriented Computing)的阶段。SOC更加靠近应用层的业务逻辑，具有敏捷性、动态适应性等特性，可与模型驱动的体系结构(Model Driven Architecture)相结合，形成相当灵活的应用构造方式。SOC在其发展过程中，逐渐形成了较为完整的概念。面向服务的体系结构(Service-Oriented Architecture)作为SOC的特征之一，在服务计算方式的应用实现过程中发挥了巨大的作用。虽然三方模型并不是SOA的创新性贡献，但是SOA使依托服务的理念达到了和前所未有的程度。除此之外，SOC形成了自己独特的建模和开发语言。不同于面向对象的方法，这些建模和开发语言多数集中在与业务流程相关的工作流技术上。SOC也形成了自己的各种开发框架和环境，使其实现能够标准化、可视化地进行。SOC有很多新的问题需要解决，其中如何由小粒度的基本服务组合出完成业务逻辑的大粒度服务是最基本的问题之一。服务组合有很多方法，其中应用最广泛的是依靠与工作流技术有关的流程描述语言来完成。为了保证服务组合的正确性，有许多形式化和非形式化方法应用于服务组合的描述和验证中。基于流程的方法和基于语义Web的方法是最常见的两种途径。基于流程的方法可以使用许多形式化方法作为其基础，如Petri网和进程代数方法；而进程代数方法则由于其组合式的特性更加适合于描述服务组合。进程代数中的Pi演算是一种较好的形式化方法，专门用于描述移动并发系统，适用于建模动态变化的服务系统。本论文从理论研究和实践结合两个方面着手，探索服务组合的形式化建模和验证。作者在本论文中的主要工作如下：1．分析了服务组合的形式化基础，并选择Pi演算作为建模工具；2．研究了服务组合描述语言和Pi演算元素之间的对应关系，给出了建模服务组合的规则和步骤；3．在说明服务描述一致性概念的基础之上，使用Pi演算作为保证一致性的形式化基础，并说明了如何对一致性进行保证；4．研究了服务兼容性和可替换性的概念，并使用Pi演算来验证可替换性；5．提出了PiFF服务组合形式化框架，并基于UESTC-PLATFORM服务计算平台，提出了将PiFF融合进实用平台的方法；