论文部分内容阅读
为了形式化地推理和验证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服务组合进行推理和验证的.
In order to formally reason and validate the web service composition described by the web service choreography specification WS-CDL, a typed formal WS-CDL formalized model --typed abstract WS-CDL is proposed. In the typed abstract WS-CDL, Defines the syntax of the type and session, the type of decision rules and operational semantics; the collaboration between web services is described by the session; the operation semantics of the session can be used to reason about the execution of the web service choreography; the type decision rules can be used to check the exchange between web services Information Type Consistency and Capturing Run-Time Errors Caused by Type Inconsistency In particular, the concept of type-extension-assumptions and type-hypothesis-sets compatibility is proposed and a type-hypothesis-based consolidation algorithm is defined to eliminate type-hypothetical conflicts. Based on the model, a typed mapping rule from choreography to orchestration is also defined. With this set of rules, the orchestration stub code and its type hypothesis set can be obtained from a given web service choreography, so the web service set can be used in choreography and The orchestration layer is validated. The proposed model has been proved to be type-safe and passed a case-by-case Description of the proposed model is helpful to web services composition reasoning and validation.