摘要： 服务组合是服务计算的核心问题，而服务组合的正确性与可算性则是服务正确执行的前提保证。首先提出一种基于Alloy的服务组合验证方法，采用有限的状态机建模WS-BPEL业务流程的状态变迁，利用Alloy语言对待验证的属性进行描述，通过Alloy模型完成有限状态机的形式化，最后使用Alloy Analyzer分析组合服务是否满足验证属性要求。实验研究表明，所提出的基于Alloy的服务组合验证方法具有较好的可行性。