随着网络技术的迅速发展,面向服务的体系架构(SOA)以其良好的可重用性、松耦合性和互操作性,已成为一种工业界和学术界广泛接受的网络化软件应用模式。Web服务作为SOA的主流实现方式,正逐步成为网络环境中资源封装的标准方式。目前,Web服务正逐步由单一的面向功能向面向业务流程转变,服务周期随之延长,使得同步通信模式的Web服务已无法满足用户需求,而无阻塞的异步Web服务成为研究热点。由于单个的Web服务提供的功能有限,为了更加充分地利用共享的Web服务构建企业级应用系统,Web服务组合技术变得愈加重要。Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合以及如何验证服务组合的正确性。在对Web服务组合的模型进行验证时,不仅要考虑组合服务是否满足功能需求,还需要检查是否存在时间冲突或数据不一致等问题,确保构建高效正确的服务组合。本文以异步Web服务为研究对象,分析相关时间和数据约束对服务交互的影响,对异步Web服务组合验证进行了深入研究。主要内容包括：(1)从软件体系结构的角度研究Web服务组合,分析基于时序逻辑的软件体系结构描述语言XYZ/ADL在描述Web服务组合方面的优势,采用XYZ/ADL来描述服务组合的交互行为,相关的时间和数据约束用XYZ/RE表示。(2)基于有限状态自动机理论,建立异步Web服务的形式化模型。针对仅涉及时间约束的Web服务建立时间异步通信模型(TACM),该模型符合UPPAAL规约,用消息队列模拟异步通信,用时间自动机中的标准时钟来表示时间约束；对于同时涉及时间和数据约束的情况,则建立异步Web服务模型(AWSM)。(3)分别提出基于TACM和基于AWSM的异步Web服务组合验证方法,并通过贯穿整个分析和验证过程的实例加以说明。