近年来，随着互联网的普及与电子商务技术的发展，面向服务的计算(SOC)和面向服务的体系结构(SOA)正逐步变为未来软件发展的一种趋势，也已成为学术界和工业界共同关注的一个研究热点。作为一种全新的计算模式，SOC有效解决在分布、动态以及异构环境下分布式应用集成问题，而SOA作为一种新的软件开发模式，通过松耦合方式有效支持和实现软件资产的集成与复用。目前Web服务技术的不断成熟与发展使其成为SOA的主流实现方式，也为SOC提供了最佳技术支撑。Web服务是一种基于网络的自描述、自包含的软件构件，具有松耦合、独立性强等特点。它以SOAP、WSDL以及UDDI等标准协议为核心，采用面向服务的体系结构，通过服务发布、查找以及绑定等基本操作，实现分布式环境中动态、开放的互操作以及跨平台应用。由于单个Web服务的功能有限，通过将已有的服务构件以静态或动态的方式组合成一个新的服务来满足企业特定的个性化需求已成为目前动态电子商务领域的发展趋势，并且已影响到当今服务产业的产品开发方式。然而，由于网络环境的动态、异构以及分布式等特性，如何确保组合后的Web服务能够实现企业要求的业务功能，同时在运行过程中不会出现企业不期望的情况，已成为构建和运行面向服务架构系统、实现企业应用集成的根本。形式化技术作为软件质量保证的一种重要方法，为解决以上问题提供了有效途径。本文采用形式化技术，围绕服务组合研究领域所涉及的三个核心科学问题：Web服务组合的建模、静态验证及运行时动态验证展开研究。首先，以自动机理论为基础，建立一个可以有效刻画数据及时间等信息的Web服务组合形式化模型；其次，以模型检测技术为核心思想，提出一种能够对Web服务组合的行为属性、时间属性以及数据属性等进行静态验证的理论方法；最后，以运行时监控Web服务组合一般方法为基本思路，给出一套能够在Web服务组合动态运行过程中出现异常时进行有效处理的故障诊断机制。对服务组合建模与验证技术的深入研究可以有效提高Web服务组合的可信性，推动面向服务概念的发展。