随着互联网和电子商务技术的发展,Web服务因其能解决Internet异构平台下服务的交互重用等问题引起了广泛关注。和传统的分布式计算模型相比,Web服务抽象程度更高、粒度更大、独立性更强,但是单一的Web服务功能有限,难以满足不断变化的业务需求,因此有必要对多个Web服务进行组合以提供更强大的功能。由于Web服务组合常用于描述跨平台跨组织的高层业务逻辑,因此保证其正确性就显得更为重要。Web服务组合是Web服务领域的研究热点,目前虽然有多种正确性验证方法,但从体系结构方面验证Web服务组合,则是一个新的研究方向。精化检验和模型检测是两种重要的形式验证技术,本文把两者应用到Web服务领域验证Web服务组合的正确性。基于上述思想,本文在课题组已有工作基础上,研究基于形式化方法和软件体系结构描述语言XYZ/ADL的Web服务组合验证问题。XYZ/ADL是时序逻辑语言XYZ/E的扩展,对有时间约束的系统而言,可由XYZ/E的实时扩展语言即XYZ/RE表示系统应满足的时间约束。考虑到多数Web服务具有实时特征,本文分析XYZ/RE和时间自动机组成元素的相似性,改进XYZ/RE到时间自动机的映射规则。针对Web服务组合系统,分别用XYZ/ADL描述其行为和性质,再将其中的XYZ/RE分别转换为对应的行为时间自动机和性质时间自动机,通过精化检验的方法判断Web服务组合系统的行为是否符合性质需求。另一方面,将单个Web服务XYZ/ADL描述中的XYZ/RE映射至单个时间自动机,多个Web服务组合XYZ/ADL描述中的XYZ/RE映射至时间自动机网络,组合后系统应满足的性质由CTL公式表示,将两者作为模型检测工具UPPAAL的输入,从而实现Web服务组合系统的正确性验证;最后分别通过网上旅游订票服务系统实例和股票分析服务系统实例说明了上述方法的可行性。