Research On Formal Verification And QoS-aware Composition Methods For Web Services Composition

The software service cooperation technology based on Web Services composition has become the critical technique to construct the circumstance of the dynamic cooperation and on-demand composition service interactions. Under the complicated application circumstance of Web Service composition, there exist two challenging and critical problems: one is how to eliminate the ill behaviors of the orchestration based on verifying the correctness of grammar and semantic, the other is how to guarantee QoS throughout the lifecycle of service composition.In order to achieve dynamic business cooperation and integration across different enterprises, this thesis mainly focuses on the two orthometric properties that are correctness verification and Qos guarantees of Web Service composition. Formalization verification of service composition based on Process Algebra and Discrete Time Ambient-Calculus, as well as combinatorial optimization and the partition method based on QoS mathematic model are deeply studied. The service composition architecture supporting formalization verification and QoS-aware composition has been also implemented. Furthermore, the architecture is applied to digital cartoon cooperation manufacturing in the Internet. The main work of this thesis is displayed as follows:(1) Aimed at the verification of Web Services composition, Pi-Calculus with type system for describing XML data structure is extended, then the dual mapping between BPEL4WS and Pi-Calculus is constructed. A verification algorithm with the function of tracking the error fractions for Web services composition is proposed, which includes Pi-Calculus verification based on open bisimulation, properties verification based on modalμ-Calculus and service compatibility verification based on Pi-Calculus with type. Moreover, we independently give the definition of compatibility and propose compatibility verification algorithm for Web services composition, and also introduce a novel method for discovering and composing services in the process of Web Services composition under the guidance of verifying compatibility of composite Web Services. Based on the above studies, a framework supporting formal verification of service composition, in which the verification tool called WebJetChecker is embedded, is proposed. WebJetChecker with the combination of three types of the verification techniques for verifying orchestration properties is implemented, by which the error fractions of the orchestration are automatically marked and the hints are given.(2) In order to describe distributed dynamic services composition with time-constrained mobile properties and complex structures of services composition, Discrete Timed Mobile Ambient (DTMA) is independently proposed. In the thesis, the semantics and syntax, properties and model logic of DTMA are given. Through combining two formalization models—time synchronous tree and Ambient graph, the time and mobile property are unified into a formal frame by Ambient synchronous tree. A model verification algorithm based on DTMA and the subset of DTMA modal logic is devised, and the decidability of the model verification is proved. According to the encoding of BPEL4WS activities on DTMA, the fault and compensation processing with multi-layer scope are modeled, and an instance of distributed service composition with time constraint and mobility is also described by DTMA and analyzed by the model verification method.(3) It is made our every effort to study optimal algorithms of QoS-aware Web service composition. On local optimal algorithms, an AHP approach is realized, which can automatically modify judgment matrix for selection of the component services. On global optimal algorithms, a heuristic 0-1 Integer Liner Programming algorithm is achieved, which combines heuristic enumeration method and revised simplex method. Simulation experiments show that the degree and optimization efficiency in our algorithm is obviously improved compared with the MATLAB 7 bintprog function that is a 0-1 integer programming algorithm. Moreover our algorithm isn't relevant to the scale changes of Web services composition and candidate service sets, thus it is applicable for the scenes that the scales of Web services composition changed dynamically. But for Web services composition with service alliance (service domain), the algorithm is unable because the non-linear global optimal model of the fitness function and QoS constraints can't be expressed in linear mode. Therefore, Tree-Coding Genetic Algorithm (TGA) is used to solve the QoS-aware global optimization with non-linear model. The results of simulation experiments show that TGA is capable of running faster than the one-dimension coding GA under the same conditions, and Tree-Coding has efficient capability for supporting re-planning. In conclusion, TGA has solved non-linear global optimization problems with service alliance.(4) Aimed at the application of data stream constraint, a Web services composition partition algorithm based on graphic clustering and service domain is put forward. Under the constraints of satisfying the data stream minimization between the clusters and the throughput maximization of the distributed system, multi-level algorithms based on graph clustering is used to partition BPEL service composition. Afterward, a way of distributed execution is employed to execute service composition. Furthermore the load of the distributed nodes transferring the BPEL fractions is adjusted to a balance.(5) According to the above studies, an infrastructure supporting QoS-aware service composition is proposed. The infrastructure includes the design and implement of Web services Composition Execution Engine with double feedback controlling loops, which can decouple flow execution and Web service invocation. From the simulation results, it can be concluded that QoS feedback controlling structure can make the engine supply the guarantee of service response time for different service classes when the workload of Web services composition varies significantly. Additionally, the method of decoupling flow execution and service invocation improves resource utilization and increases concurrence ability of flow execution and throughputs of the engine. This paper also presents run-time fault-tolerance processing framework supported by the infrastructure. Based on the framework, online fault-tolerance mechanism on the deviation detection between QoS measuring values and SLA estimated values is studied. A new concept—"fault-tolerance selection factor" and a mapping function which makes this factor map to the fault-tolerance processing are proposed. The simulation experiments also show that the "retry-substitute-reconfigure" processing strategy adopted at run-time fault processing can effectively support online self-resumption of service composition processes.On the basis of all of the above research results, a Web service composition prototype system supporting formal verification and QoS-aware service composition is designed and implemented. This architecture is applied to cooperation manufacturing across different digital cartoon enterprises in the Internet, through which the technologic process of cooperation manufacturing in digital cartoon is realized.