Evolution-Driven Testing And Verification For Web Composite Service

SOA(Service-Oriented Architecture) is the milestone in distributed computing and the development of software technologies. As the basis of SOA, Web service is a kind of networking component with autonomy, openness, self-description and realization-independency. Its interoperation and loose coupling makes it more convenient to do software development and distributed application on Internet. Web service composition makes uses of existing services to provide more and value-added services, which can be done by composing them according to the implementation logic users ask for. And BPEL(Business Process Execution Language) is the most popular language to describe the Web composite service.BPEL composite service must evolve a lot to meet various requirements, such as bugs fixing, requirements adding, performance improving, environment changing, and so on. How to make sure the correctness of every version in the lifetime of BPEL composite service, especially the correctness of data flow, is an important problem. Testing and verification is two effective methods to provide quality assurance. Since BPEL is based on XML language, it needs to be formally modeled to support automatic and efficient testing and verification.Based on the feature of evolution, the dissertation systematically investigates the modeling, testing and verification of BPEL composite service from the perspective of data flow. The main contributions of this dissertation are listed as follows:(1) It provides a classification for change types during evolution of BPEL composite service and proposes a formal model called XCFG(eXtended Control Flow Graph). Variable sets are defined to describe the variables used in the BPEL process. PartnerLink sets are defined to describe the partner services interacting with the process. Flow graph is defined to describe the process behavior, where nodes describe the activities, control edges describe the execution order and link edges describe links. Each element in XCFG has its field to record corresponding information in BPEL composite service. The model can not only capture the control flow of BPEL composite service, but also the data flow among exchanges, which provides necessary information for data flow based testing and verification.(2) It proposes a XCFG based test case selection method for regression testing with all-uses testing policy. The method consist of four steps, including data flow analysis, affected du-pair identification, testing path computation and test case selection. First it improves the traditional computation method for reaching definition and proposes the XCFG based data flow analysis method which can get the du-pairs of BPEL process. Then it recognizes the du-pairs affected by process change, binding change and interface change, which needs to be tested in the regression testing, and computes the data flow paths which cover the affected du-pairs. Finally it analyzes and compares the path conditions between the paths of baseline version and evolved version to select test cases. Experiment study shows the proposed method is effective and can detect three change types.(3) It proposes verification algorithms to verify consistency of def-use, deadlock-free, reachability and non-conflict for single versions of BPEL composite services. The verifications for the four data flow related properties are based on XCFG, and experiment study shows the effectiveness and efficiency of the proposed verification algorithms. It also proposes ICV(InCremental Verification) to incrementally verify the non-conflict property of evolved version. ICV computes the concurrency sets for both the baseline and evolved version, and recognizes the activities which are affected by process change and be related to non-conflict Then it concentrates on these affected activities to perform the verification. Experimental study shows ICV is effective and more efficiency than the verification method for single versions.(4) A prototype tool called XCFG4BPEL is designed and implemented to support our approaches. XCFG4BPEL can be used to construct XCFG models of BPEL composite services, compute testing paths for data flow testing of single versions, select test cases for data flow based regression testing, verify data flow related properties of single versions, including consistencyof def-use, deadlock-free, reachability and non-conflict, and verify the non-conflict property of evolved version with ICV.