通信学报 ›› 2012, Vol. 33 ›› Issue (Z2): 1-8.doi: 10.3969/j.issn.1000-436x.2012.z2.001

• 学术论文 •    下一篇

基于Alloy的服务组合验证

曹玖新1,2,吴江林1,2,王国进3,刘波1,2,杨鹏伟1,2,董丹1,2   

  1. 1 东南大学 计算机科学与工程学院，江苏 南京 210096
    2 东南大学 计算机网络与信息集成教育部重点实验室，江苏 南京 210096
    3 华为技术有限公司，江苏 南京 210012
  • 出版日期:2012-11-25 发布日期:2017-08-03
  • 基金资助:
    国家自然科学基金资助项目;国家自然科学基金资助项目;国家自然科学基金资助项目;国家自然科学基金资助项目;国家重点基础研究发展计划（“973”计划）基金资助项目;国家科技支撑计划课题基金资助项目;教育部博士点基金课题基金资助项目;江苏省自然科学基金资助项目;国家科技重大专项课题基金资助项目;江苏省“网络与信息安全”重点实验室基金资助项目

Alloy-based verification of Web service composition

Jiu-xin CAO1,2,Jiang-lin WU1,2,Guo-jin WANG3,Bo LIU1,2,Peng-wei YANG1,2,Dan DONG1,2   

  1. 1 School of Computer Science and Engineering,Southeast University,Nanjing 210096,China
    2 Key Laboratory of Computer Network and Information Integration,Ministry of Education,Southeast University,Nanjing 210096,China
    3 Huawei Technologies Co.,Nanjing 210012,China
  • Online:2012-11-25 Published:2017-08-03
  • Supported by:
    The National Natural Science Foundation of China;The National Natural Science Foundation of China;The National Natural Science Foundation of China;The National Natural Science Foundation of China;The National Basic Research Program of China(973 Program);The National Key Technology R＆D Program;The Ph.D.Programs Foundation of Ministry of Education of China;The Natural Science Foundation of Jiangsu Province;The National Science and Technology Major Project of China;The Program of Jiangsu Province Key Laboratory of Network and Infermation Security

在线阅读

0

PDF下载

609

摘要：

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

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

Abstract:

Service composition was the core problem of service computing,the validity and reliability of service composition had become the premise of service execution.A method was presented which utilizes the finite state machine (FSM)to model the business process’s state transitions,and described the required properties with Alloy language.Then,Alloy model was used to formalize the service FSM and the required properties of the system.Finally,Alloy Analyzer was used to verify the model that whether the required properties were satisfied.It is shown that the method of Alloy-based verification of the service composition is of good feasibility.

Key words: Web service, service composition, finite state machine, Alloy, verification

No Suggested Reading articles found!