Research On Modeling And Verification Of QoS-Oriented Web Services Composition

SOC(Service-Oriented Computing) and SOA(Service-Oriented Architecture) is leading the forward trend of distributed computing and software development. Web Services Composition(WSC) is the recommended technology for implementing SOC&SOA and a novel way to build Web application by composing existing Web services. Quality of Service (QoS) of WSC is a key factor to affect its successful application since Web services composing WSC are autonomous and owned by different organizations, and distributed in the open and dynamic internet circumstance. In the phase of modeling or design, it is useful to ensure dependence of WSC by modeling, analyzing and verifying its model from functional and QoS view.Currently, functional model and QoS model of WSC are separately created for analysis and verification at different phase, which causes more development cost and longer development period. The main cause is that current modeling and verification methods and tools do not strongly support WSC. Hence, it is worthful to improve current modeling and verification methods and tools for WSC. Some questions rise for doing that. First, QoS of WSC includes many properties, and evaluations of those properties very differ among application fields and organizations. Thus, it is impossible to model and verify all properties in a unique model. How do we extract necessary properties to be modeled from varieties of properties? How do we evaluate the necessary properties in consistent way regardless of fields and organizations? Second, UML Sequence Diagram (SD) is a modeling language for modeling interactive behaviors among components of system in graphical way. It is popular in that it features intuitive modeling way and easily used by end users, analyzers and designers. SD is suitable for modeling WSC since WSC also features interacting among Web services components that comprises WSC. However, SD does not strongly support modeling QoS of WSC. How do we improve SD to support modeling QoS of WSC? Third, Process Algebras (PAs) is a set of formal and verification-oriented modeling languages that are good at modeling and verifying concurrent and composite systems. They are widely used to formally modeling and verifying WSC. However, PAs does not strongly support modeling and analyzing QoS of WSC. How do we improve PAs to support modeling and analyzing QoS of WSC? Finally, it is difficult for SD to support directly formal analysis and verification of system since SD has graphical syntax and natural language semantics. Comparatively, it is difficult for end users, analyzers and designers to understand and use PAs since they are based on strict mathematics theory and formal symbols. Hence, it makes sense to figure out a solution to compromise for both to take advantages of them. This thesis does systemic researches on above problems and achieves some contributions as below.(1) We propose an abstract QoS model that includes only three abstract properties to cover all concrete QoS properties, i.e., time, cost and probability, from views of practice and conciseness. We also propose approaches for handling and evaluating the abstract properties in unique way, which support evaluating QoS of Web services in consistent and unambiguous way in abstract model level, and selecting Web service with optimal QoS.(2) We propose a specific sequence diagram called SDQ(Sequence Diagram for QoS) by extending traditional UML SD with QoS modeling capability, and present modeling approach based on SDQ. SDQ includes two parts, i.e., bSDQ(basic SDQ) and hSDQ(high level SDQ). The bSDQ is a specific SD extended with time and cost modeling capabilities to model local scenarios, while the hSDQ is a direct graph extended with probability modeling capability to model global scenarios by composing bSDQs. Then we present an approach to model WSC by mapping activities of BPEL4WS to SDQ.(3) We propose a specific process algebra called PAQ(Process Algebra for QoS), and then present approaches to analyze and verify functionality and QoS in unique way based on PAQ. We propose PAQ to improve a existing process algebras with capability of analyzing and verifying QoS by mapping time, cost and probability to the process algebra. Also we present syntax and semantics of PAQ and prove in theory level that PAQ extends the existing process algebra with capability of modeling QoS. After that, we represent approaches to formally analyze and verify functionality and QoS of WSC in unique way using PAQ.(4) We present an approach to translate SDQ to PAQ. The approach is a semantics-based translation. We formalize the semantics of SDQ using PAQ, and then figure out an algorithm of translating SDQ models to PAQ models. The approach integrates the advantage of graphical modeling capability of SDQ and the advantage of formal analysis and verification of PAQ.(5) And a tool,called UMV4WSC,is designed according to the above proposed approaches. After that, we present a full case study that includes: modeling Web service composition using SDQ, translating SDQ models to PAQ models, and verifying PAQ models. The case study indicates the effectiveness of the above proposed approaches.