基于Alloy的服务组合验证

摘要：

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

关键词： Web服务 服务组合 有限状态机 Alloy 验证

作者: 吴江林 曹玖新 杨鹏伟 董丹 王国进

作者单位: 东南大学 计算机科学与工程学院 ,南京 江苏 210096 东南大学 计算机网络与信息集成教育部重点实验室,南京 江苏 210096

会议类型: 国内会议

会议名称: 第十九届全国网络与数据通信学术会议

会议地点: 长沙

会议语种:中文

页码: 1-7

在线出版日期: 2012-11-01（万方平台首次上网日期，不代表论文的发表时间）