Study Of Formal Model Of Web Services Composition

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.