计算机应用 ›› 2012, Vol. 32 ›› Issue (02): 545-550.DOI: 10.3724/SP.J.1087.2012.00545

• 计算机软件技术 • 上一篇    下一篇

Web服务组合行为一致性的形式化描述和分析

李劲1,2,张华1,吴浩雄1,向军1   

  1. 1. 湖北民族学院 信息工程学院,湖北 恩施 445000
    2. 华中师范大学 信息管理系,武汉 430079
  • 收稿日期:2011-07-13 修回日期:2011-09-23 发布日期:2012-02-23 出版日期:2012-02-01
  • 通讯作者: 李劲
  • 作者简介:李劲(1973-),男,湖北恩施人,副教授,博士研究生,主要研究方向:数据挖掘、Web服务;
    张华(1978-),男,湖北恩施人,讲师,硕士,主要研究方向:计算机网络;
    吴浩雄(1979-),男,湖北建始人,工程师,主要研究方向:网络安全;
    向军(1978-),男,湖北来风人,讲师,博士,主要研究方向:移动计算、实时数据库系统、软件测试。
  • 基金资助:
    国家自然科学基金资助项目(61040006);湖北省自然科学基金资助项目(2010CDZ027);湖北省教育厅科技项目(B20101909)

Formal description and analysis of conformance of composite Web service behavior

LI Jin1,2,ZHANG Hua2,WU Hao-xiong2,XIANG Jun2   

  1. 1. Department of Information and Management, Central China Normal University, Wuhan Hubei 430079, China
    2. School of Information Engineering, Hubei University for Nationalities, Enshi Hubei 445000, China
  • Received:2011-07-13 Revised:2011-09-23 Online:2012-02-23 Published:2012-02-01
  • Contact: LI Jin

摘要: Web服务编排和Web服务编制从全局和局部分别定义了Web服务组合的全局交互行为和每个参与者的局部行为,为了保证Web服务组合实现的正确性,Web服务组合的全局交互行为和每个参与者的局部行为必须是一致的。首先利用进程代数给出了对Web服务组合的全局交互行为、局部行为以及二者之间的映射关系的形式化描述,在此基础上分别通过分析全局会话变迁和局部进程变迁的关系和进程互相似理论给出了Web服务组合全局交互行为和局部行为的一致性的两个形式化判定准则。同时通过案例说明了如何形式化地检测Web服务组合的全局交互行为和局部行为之间的一致性。结果显示提出的Web服务组合一致性形式化定义和检测方法能检测组合行为的一致性,从而能有效地保证Web服务组合的正确性。

关键词: Web服务组合, 一致性检查, Web服务, 形式化方法

Abstract: Web service choreography and orchestration defines the global interaction of composite Web service and the local behavior of each participant from global and local perspectives, respectively. The conformance of each participant's local behavior to global interaction is the guarantee of the correctness of Web service composition. The paper firstly presented a set of definitions to formally describe the global interaction of composite Web service, the local behavior of each participant and the mapping rules between them based on process algebra. Accordingly, two formal judgmental rules for the conformance of each participant's local behavior to global interaction were proposed. The two formal rules were based on the relationship between the transition of global interaction and local process and bisimulation theorem. At last, the conformance formal checking approach was described through a case study. The result of the case study shows that the proposed conformance definition of Web service composition and conformance checking approach can formally check the conformance of Web service composition effectively. As a result, the correctness of Web service composition can be guaranteed.

Key words: Web services composition, conformance test, Web services, formal method

中图分类号: