Research On Automatic Service Composition And Formal Verification

SOC (Service-Oriented Computing) and SOA (Service Oriented Architecture) represent the promising trend of distributed computing and software development. Their development and maturity will lead the software area to a new development climax and also without doubt will bring forward an important revolution to the software industry.The key of SOC& SOA is to utilize services as fundamental elements and to construct distributed, loose-coupled enterprise-level application systems on demand. On the other hand, with the development of Web service technology, it has been proven to be the optimal approach to apply and deploy SOC&SOA. Thus, the issue of Web service composition is carried out and quickly attracts many researchers' concern. It has been regarded as the key element in SOC as well as the most important precondition for SOA to come into application and implementation from concepts phase to benefit software industry finally.However, Web service composition is not an isolated topic but includes a serial of hot research issues such as Web service discovery, automatic Web service composition, verification of Web service composition and execution. All these issues construct the research framework of Web service composition, in which they can be classified into two categories: the building-time issues and the running-time issues, according to the life-cycle of a Web service composition. This thesis emphasizes the former category of issues and focuses on its most important issues: Web service discovery, automatic Web service composition and verification of Web service composition. The major work and contributions are as follows:First, we propose an efficient two-phase semantic Web service discovery method -TSSD. This method carries out Web service discovery in two phases: discovery based on operation matchmaking and discovery based on operation composition matchmaking. During the first phase, it considers semantic information and interface dependencies within an operation. During the second phase, it takes interface assign relations between operations into consideration to compose operations to fulfill users' requests. A serial of experiments show that TSSD gains better performance on both discovery recall rate and precision than traditional approaches and scales well with the number of services being accessed.Second, we propose an automatic service composition approach based on Generation-Tree. This approach makes use of the divide and rule strategy through three steps to automate composition of Web services. It first builds aComplete-Generation-Tree on-line for each output that a user asks for; then it searches for an optimal valid Generation-Path for each output; after that it composes Generation-Paths to construct a coarse-grain composite service. The characteristics of this method include a smaller search space, low complexity and good efficiency. It can support the users' requirement with not only single target but also with multiple targets. A set of experiments show that this approach has a good performance and can serve users well even the repository has a large number of services.Third, we propose a pi-calculus-based method for the verification of Web service composition. It first utilizes pi-calculus to formalize service behavior as well as the interaction behavior between services as processes. And then it verifies whether two services are compatible with each other through the use of the operational semantics, the automatic deductive inference ability of pi-calculus automatically. Compared to other approaches, this method not only checks the compatibility between two services in a qualitative and a quantificational way, but also can point out the scenarios where two services can interact with each other properly and where they can not. These characteristics are significant in the guidance of service composition execution.Last, we propose a logic framework of service composition-WSCF and implement a prototype of service composition system-JTangFlow-S. WSCF outlines the main functions, components and core processes in a service composition system, and supports business process-driven service composition as well as on-line task oriented service composition. According to WSCF, we design and implement a service composition prototype-JTangFlow-S, in which we realize the service discovery method, the service composition method and the verification method proposed in this thesis.