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

Formal description and analysis of conformance of composite Web service behavior

作　　者：李劲[1,2] 张华[1] 吴浩雄[1] 向军[1] 

机构地区：[1]湖北民族学院信息工程学院,湖北恩施445000 [2]华中师范大学信息管理系,武汉430079

出　　处：《计算机应用》2012年第2期545-550,共6页journal of Computer Applications

基　　金：国家自然科学基金资助项目(61040006);湖北省自然科学基金资助项目(2010CDZ027);湖北省教育厅科技项目(B20101909)

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

关 键 词：WEB服务组合 一致性检查 WEB服务 形式化方法 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]