随着近年来服务计算和面向服务的架构(SOA)的迅速发展以及Web服务技术的成熟与完善，服务组合作为服务计算和SOA领域的核心问题已经越来越受到重视。WS-BPEL作为描述Web服务组合、编制和协调的语言，它提供了描述业务流程的丰富词汇，从而利用服务组合实现新的服务功能。但是WS-BPEL却缺乏对服务组合的正确性，有效性的验证机制。这就造成了利用WS-BPEL描述的服务组合可能会存在系统风险，并可能造成重大损失。为此，本文提出了基于Alloy建模语言的服务组合验证方案。　　 本文的研究工作可以总结为以下几个部分：　　 1.介绍了服务计算目前的发展情况，总结了服务计算领域服务组合的方法，并且根据目前服务组合验证领域的研究现状，完整总结了目前服务组合验证使用的四种方法和其中使用的技术。　　 2.提出了基于Alloy的服务组合验证方案，该方案利用Alloy描述服务组合，得到Alloy模型，然后根据系统需求将系统属性进行转换得到Alloy约束，最后两者作为Alloy Analyzer的输入用于服务组合的分析。这种方案综合了严谨性，增量性和可视化的优点，提供了完整、有效的分析方案。　　 3.本文提出了使用有限状态机来建模服务组合，描述系统的状态变化，并详细介绍了从WS-BPEL到Alloy的转换方法。使用有限状态机作为中间表示，方便了从WS-BPEL到Alloy的转换。接着，本文总结了使用Alloy Analyzer分析Alloy模型的理论基础——满足性理论和前提假设——“小范围假设”，提出了根据Alloy Analyzer提供的可视化特性分析服务组合的具体方法。　　 4.最后，本文实现了从WS-BPEL到Alloy转换的原型系统BPEL2Alloy，使得从WS-BPEL到Alloy的转换能够自动化完成，方便了以后对基于WS-BPEL服务组合的验证.