FORMAL ANALYSIS OF WEB SERVICE COMPOSITION

Abstract:

Web service technologies have emerged as a de-facto standard for integrating disparate applications and systems using open, XML-based standards. In addition to building Web service interfaces to existing applications, a number of standards (e.g. WS-BPEL) have been proposed to compose these Web services together to form a more meaningful business processes. In this thesis, we focus on the verification and analysis of the composition of
Web services.

We present a fully automated technique for the synthesis of the local time requirement to help the service composition conform to the time requirement. The approach is implementation independent, therefore can be applied at the design stage of service composition. Based on the synthesis requirements, we propose a new approach to select a set of component services to compose a composite service such that it could satisfy the non-functional requirements, and we also extend the work to find a set of features that do not have inconsistency or conflict, yet optimize multiple objectives (e.g., minimizing cost and maximizing number of features), for service-based product lines. To guarantee the requirements of the service composition at the design time, we propose a method to verify the service composition against combined functional and non-functional requirements. We capture the semantics of Web service composition using labelled transition systems (LTSs) and verify the Web service composition directly without building intermediate or abstract models before applying verification approaches. We have also developed a tool to implement our proposed approach. To help the service composition conform to requirements during runtime, we propose an automated approach based on a genetic algorithm to calculate the recovery plan. Our approach has been evaluated on real-world case studies, and has shown promising results.