东南大学学报（英文版）2008，Vol.24Issue(3)：300-307,8.
Web服务组合规范WS-CDL的类型化形式化模型
Typed formal model for WS-CDL specification of web services composition
摘要
Abstract
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服务组合/web服务编排描述语言Key words
typed model/web services composition/web services choreography description language分类
信息技术与安全科学引用本文复制引用
辜希武,李瑞轩,卢正鼎..Web服务组合规范WS-CDL的类型化形式化模型[J].东南大学学报（英文版）,2008,24(3):300-307,8.基金项目
The National Natural Science Foundation of China (No. 60403027, 60773191, 70771043), the National High Technology Re-search and Development Program of China (863 Program) (No. 2007AA01 Z403). （No. 60403027, 60773191, 70771043）
