Typed formal model for WS-CDL specification of web services composition  

Web服务组合规范WS-CDL的类型化形式化模型(英文)

作　　者：辜希武[1] 李瑞轩[1] 卢正鼎[1] 

机构地区：[1]华中科技大学计算机科学与技术学院,武汉430074

出　　处：《Journal of Southeast University(English Edition)》2008年第3期300-307,共8页东南大学学报（英文版）

基　　金：The National Natural Science Foundation of China(No.60403027,60773191,70771043);the National High Technology Research and Development Program of China(863 Program)(No.2007AA01Z403)

摘　　要：In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description language）for WS-CDL specifications is proposed.In typed Abstract WS-CDL,the syntax of type and session,typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly,the concepts of type assumption set extension and type assumption set compatibility are proposed,and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model,typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules,orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels,respectively.The model is proved to have properties of type safety,and how the model can help to reason and verify web services composition is illustrated through a case study.为了形式化地推理和验证web服务编排规范WS-CDL所描述的web服务组合,提出了一个WS-CDL规范的类型化形式化模型——typed abstract WS-CDL.在typed abstract WS-CDL中,定义了类型和会话的语法、类型判定规则和操作语义;web服务间的协作由会话来描述;利用会话的操作语义能对web服务编排的执行进行推理;利用类型判定规则能检查web服务间交换信息类型一致性并捕获由于类型不一致导致的运行时错误.特别地提出了类型假设集的外延和类型假设集相容性的概念,并定义了类型假设集的合并算法以消除类型假设冲突.在该模型基础上,还定义了从choreography到orchestration的类型化映射规则,通过这组规则,可以从一个给定的web服务choreography得到orchestration桩代码及其类型假设集,因而web服务组合能在choreography和orchestration层被验证.提出的模型被证明具有类型安全性,并且通过一个案例分析说明了所提出的模型是有助于对web服务组合进行推理和验证的.

关 键 词：typed model web services composition web services choreography description language 

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