Web服务组合形式化模型研究-智能与分布计算实验室

Web服务组合形式化模型研究

姓名	辜希武
论文答辩日期	2007.06.04
论文提交日期	2007.06.08
论文级别	博士
中文题名	Web服务组合形式化模型研究
英文题名	Web services;Web services composition;Formal model;Typed formal model;Process algebra;Pi-calculus
导师1	卢正鼎
导师2
中文关键词	Web服务;Web服务组合;形式化模型;类型化模型;进程代数;Pi-演算
英文关键词	Web services;Web services composition;Formal model;Typed formal model;Process algebra;Pi-calculus
中文文摘	随着Web服务技术的迅速发展，越来越多的的Web服务运行在Internet上，但单个的Web服务功能有限，难以满足日益增长和不断变化的用户需求。因此，如何将已有的、运行在异构平台上的Web服务组合起来，以提供给用户更为强大和增值的功能，成为Web服务研究领域中的一个热点。由于已有的Web服务可能是彼此独立地开发，以不同语言实现，运行在不同的、异构的平台上，因此Web服务组合存在的问题有：如何描述Web服务的动态行为，如何定义和描述Web服务间的交互的逻辑顺序以保证Web服务的动态行为的匹配性，如何保证Web服务之间传递消息的数据类型的一致性，如何对组合的Web服务进行验证和测试以确保执行结果的正确性。目前已经提出的Web服务组合规范如BPEL4WS、WS-CDL都是基于XML的描述性语言，缺乏一种形式化模型来表达语言的语义以及形式化验证方法来保证用这些规范所定义的Web服务组合的正确性。同时，由于参与Web服务组合的各个子服务都运行在分布式异构的环境下，因此想依靠组合的Web服务的实际运行来检测组合中的错误是代价昂贵的并且几乎是不可能的，因此对Web服务组合的形式化验证也是必须的而且是非常重要的。解决上述问题的一个行之有效的办法就是针对Web服务组合规范如BPEL4WS、WS-CDL建立合适的形式化模型，形式化地定义和描述Web服务组合的动态交互行为，利用Web服务组合的形式化模型对Web服务组合的性质如死锁避免、数据类型一致性和动态行为的匹配性进行检查和验证，以保证Web服务组合的动态行为的匹配和数据类型的一致性。因此，针对Web服务组合规范BPEL4WS和WS-CDL，研究了基于工作流的Web服务组合形式化模型以及如何利用Web服务组合的形式化模型对Web服务组合的动态行为的匹配和数据类型的一致性进行验证。针对Web服务组合规范BPEL4WS，分别建立了BPEL4WS到Pi-演算和CSP的概念映射，在此基础上，建立了基于Pi-演算和CSP的BPEL4WS形式化模型；同时给出了从BPEL4WS到Pi-演算和CSP进程的自动转换算法和模型的验证方法。针对Web服务组合规范WS-CDL，建立了基于全局的形式化模型框架Abstract WS-CDL，在此基础上利用Abstract WS-CDL对WS-CDL中各类行为进行了形式化描述；同时定义了将全局模型框架Abstract WS-CDL映射到基于Pi-演算的局部BPEL4WS模型的映射规则，并给出了全局模型框架和局部模型一致性的形式化定义；然后给出了全局和局部二个层次的模型验证方法以及全局模型框架和局部模型一致性的验证方法。利用基于Pi-演算的形式化方法研究和给出了二个Web服务的强互相容和弱互相容的形式化定义，在二个Web服务弱互相容定义的基础上，定义了二个Web服务之间互投影的算法，进而给出了多个Web服务互相容的形式化定义；然后给出了Web服务的可替换性的判断准则和二个Web服务相容性的检测算法。研究和给出了类型化的BPEL4WS形式化模型和类型化的Abstract WS-CDL形式化模型框架，特别是提出了进程类型假设集的外延和进程类型假设集相容性的概念，并且给出了进程类型假设集的合并算法；在此基础上，定义了全局会话和局部进程类型良好性的推理规则和捕获由于类型不一致而导致运行时错误的操作语义。同时，给出了从类型化的全局模型框架到类型化的局部模型的映射规则；然后，针对类型化的Abstract WS-CDL，给出了全局会话类型安全性质的证明。根据所建立的全局和局部模型，给出了一个自顶向下的Web服务组合实现框架iFrame4WS，在该框架中将Web服务组合的过程划分为描述层、抽象层和执行层，并通过抽象层的形式化模型和形式化验证来保证Web服务组合的的动态行为的匹配和数据类型的一致性。
英文文摘	With the rapid development of web services technology, increasing amounts of web services are running over Internet. But the limited function of single web service can not satisfy the growing and varying custom requirement. Therefore, how to compose existed web services running on heterogeneous platforms together so as to provide custom more powerful and valuable function has become hotspot of web service researching area. Because web services may be developed independently, implemented with different languages and running on heterogeneous platforms, there exist following problems about web services composition: how to describe the dynamic behavior of web service, how to define and describe the logical sequence of interaction between web services in order to guarantee the compatibility of web service’s dynamic behavior, how to verify and check web services composition in order to guarantee the correctness of composite web service’s execution. The proposed web service composition specifications such as BPEL4WS and WS-CDL so far are XML-based descriptive languages, lacking some kind of formal model to express the semantic of these languages accurately and formal verification mechanism to ensure the correctness of composite web service defined by such web service composition specifications. Moreover，it is cost expensive and nearly impossible to find out web service composition errors only depend upon composite web service’s actual running because the participates in the web services composition are all running in heterogeneous distributed environment. Therefore, it is important and necessary to formally verify the web services composition. An effective means to deal with the problems mentioned above is to present formal model according to web service composition specifications such as BPEL4WS, WS-CDL, et al respectively, formally define and describe the dynamic interaction behavior of web services composition, verify the properties of web service composition like deadlock avoidance, consistency of data type and dynamic behavior’s compatibility utilizing formal model of web service composition so that the compatibility of dynamic interaction behavior of web services composition and consistency of data type can be guaranteed. Accordingly, the workflow based formal model of web services composition specification BPEL4WS and WS-CDL and the verification of the web services composition based on the formal model is studied. Aiming at web service composition specification BPEL4WS, we define the conception mapping from BPEL4WS to Pi-calculus and CSP respectively. Furthermore, not only the formal models of BPEL4WS based on Pi-calculus and CSP but also the automatic translation algorithm from BPEL4WS to Pi-calculus and CSP are presented. The model verification method is also presented through case study. Aiming at web service composition specification WS-CDL, we propose a formal model framework Abstract WS-CDL that is based on global view and formally describe all activities defined in WS-CDL specification. A set of rules for mapping global based formal model framework Abstract WS-CDL to local model depicted by Pi-Calculus and formal definition of conformance between global model and local model are also defined. The model verification methods at global level and local level are presented through a case study. We analyzes web services compatibility using a formal approach based on Pi-calculus and present formal definitions of strong compatibility and weak compatibility between two web services. On the basis of weak compatibility between two web services, the projection operation algorithm between two web services is defined and the formal definitions of compatibility between multiple web services on the base of projection operation is proposed furthermore. According to the formal definitions of compatibility between multiple web services, the web service substitutability is characterized formally. The checking algorithm of compatibility between two web services is also taken into account. On the basis of presented formal model of BPEL4WS and WS-CDL, we study and present typed formal models of BPEL4WS and WS-CDL. Particularly, we propose the concepts of type assumption set extension and type assumption set compatibility, and define the merging algorithm of type assumption set accordingly. On the ground of merging algorithm of type assumption set, we define the reduction rules for well type judgments of global session and local process, and the operational semantics for capturing run-time error due to date type mismatch. A set of typed rules for mapping typed global model framework to typed local model are defined. The type safety property of Abstract WS-CDL session is also proved. On the basis of presented formal model of BPEL4WS and WS-CDL, we outline a Top-Down framework- iFrame4WS for web services composition implementation. In iFrame4WS, the process of web services composition is divided into description level, abstract level and execution level. The formal model and verification approach are defined in abstract level so as to ensure the compatibility of dynamic interaction behavior of web services composition and consistency of data type.