基于Alloy的服务组合验证

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