Research Of Web Service Composition Based On Pi-Calculus

Recently, with the widely and deeply uses of the SOA architecture and Web services, how to composite services in accordance with the different objectives and approaches has became the focus of attention. Although the research on the Web services and service composition has been investigated and put into practice relatively well, from the perspective of status of their research, still remain on non-formal or semi-formal basis to a large extent. On the contrary, formal methods themselves guideline and support the Web service composition well throughout the life cycle (i.e., service definition, service discovery, service composition, and service verification). Also, formal methods, it needs to some appropriate scenarios to be developed and improved in the applied research.This dissertation dedicats to describe and analysis the key issues during the life cycle of Web service composition with some extensions of Pi calculus, including modeling of the design-time, verification in run-time, service selection in select-time, etc. Concretely, main work and innovations involve the following several aspects:(1) With the characteristics of Web service composition, the traditional Pi calculus has been extended to Pi-beam, with the expansion of grammar, semantics and type system. In the expansion of grammar, there exist the constrained beam channel, logic parallels and logic choices; while the expansion to semantics involve the beam channel linkage rules, logic parallels from/to logic choices transforming rules etc.; type of expansion include increasing the beam channel type with constraints and associated typing rules and error rules.(2) In order to utile the relevant features of Pi-beam and denote the static characteristics of composition system intuitively, we developed a notation of diagram, annotated process link diagram and its simplified version, to modeling the basic control flow patterns of service composition uniformly.(3) With the helps of the type system and form of derivations in reductions, the verification problem of service composition is discussed. The type correctness verification mainly depends on whether a composite process is well-typed or may be derived into a type of error. According to the form of the process after evolutions, the composition can be judged right or wrong of control flow. In the flow-error cases, deadlock and livelock is focus. Especially for the deadlock, by extending the type system of process, the deadlock can be found and even to avoid deadlock.(4) In addition, a flow-correct-based automatic composition algorithm has been proposed. As it base on the pattern matching of semantic rules of Pi-beam, so it not needs the involvements of theorem provers and inference tools. With regards of the time complexity, due to the introduction of the type system, the search space is significantly reduced.(5) The QoS-aware service composition has been proved to be NP-hard problem, so a large number of heuristic algorithms have been used on it. Partical Swarm Optimization (PSO) is better than more other recent methods. However, most studies only limited use of these algorithms and discuss how the efficiency of the algorithm, the method itself is rarely discussed in formal models. In this dissertation, inspired by another process algebra,$-calculus, the author introduce a non-functional expansion to evaluate QoS, some primitives and rules to choice according to QoS, and a meta-search procedure as a built-in primitive. Based on this algebra, the author developed a QoS evaluation algorithm based on AST, and carried out simulation experiments.(6) Considering the needs of practice in the cloud and cloud-based service, the author expands the Pi-beam calculus to a distributed higher-order version of Pi-calculus, DHoPi-beam, which supports the abstraction and application similar to the Lambda calculus and the mobility of code. Based on this the concepts of Higher-Order Web Service and Higher-Order Web Service Composition are proposed, and the related formal description and associated architecture.