摘要
Web服务编排描述语言WS-CDL从全局的角度定义了一组Web服务之间的协作和交互必须遵守的规则。作为一个基于XML的描述性规范语言,WS-CDL缺乏形式化的模型和验证机制,难以保证协作和交互的正确性。本文针对WS-CDL规范提出了一个基于全局的形式化模型框架Abstract WS-CDL,包括语法、同构关系和操作语义,同时定义了一套从该模型框架到基于Pi-演算描述的局部模型的映射规则,最后通过案例分析给出了全局和局部2个层次的模型验证方法。
The Web Service Choreography Description Language（WS-CDL） defines a set of rules for the collaborations and interactions between a group of Web services from a global view. As a XML-based descriptive language, WS-CDL lacks a formal model and verification mechanism to guarantee the correctness of collaborations and interactions. This paper proposes a formal model framework Abstract WS-CDL for the WS-CDL specification that is based on global view, including syntax, structural congruence and operational semantics. The paper also defines a set of rules for mapping this global based formal model to local model depicted by Pi-calculus. At last the paper introduces the model verification methods at global level and local level through a case study.
出处
《计算机科学》
CSCD
北大核心
2007年第9期5-11,共7页
Computer Science
基金
国家自然科学基金(项目编号:60403027)
湖北省自然科学基金(项目编号:2005ABA258)
软件工程重点实验室开放基金(项目编号:SKLSE05-07)
