A Study On Formally Modeling And Verifying The Composition Of Web Services

Recently, Service-Oriented Archtecutre (SOA in short) has drawn a lot of attention. It is a kind of new distributed application architecture and component technology. SOA which can help IT organizations meet more challenging requirement of market is promoted in the industry as the next evolutionary step in software architecture. Web services are the most promising technique to realze SOA. Web services are software applications which can be used through a network (intranet or Internet) via the exchange of messages based on XML standards. Due to the limit of the function that a single web service can provide, web services usually need to be composed into larger ones to meet the users' requirement. Composition approaches for web services can be generally divided into three groups:the workflow based methods, the ontology based methods and the formal methods.This paper aims to study the formal method of modeling and analyzing the compositon of web services. The main contribution of this paper is introduced as following:1. The Development of Web Service Composition Model FMWSCWeb service compositon model FMWSC (Formal Model for Web Service Composition) comprised two parts:Service Description Model and Service Interaction Model. Service Description Model is based on WSDL (Web Services Description Language) and used for describing the stactic information of web service composition; Service Interaction Model is used for describing the dynamic information of web services.2. The Development of the Formal Verification Method for Determing the Properties and Correctness of the Service Interaction ProcessThe formal verification method for the Service Interaction Model focuses on verifying the properties of the basic interaction processes. The properties of the complete service interaction process are determined by the properties of the basic interaction process and the way these basic processes are composed. A distingusing merit of our method is the scale of the model checking can be reduced, and therefore the efficiency of model checking can be improved. The semantics of IMWSC is studied. This semantics comprised three parts:semantic domain, semantic range, and the valuation functions. Based on the semantics of MWSC, the formal verification method of IMWSC is given. A kind of modal logic,μ-calculus is introduced as the formal reasoning logic to verify the properties of IMWSC Instances.3. Investigating the Application of the FMWSC Model on a Case StudyThe application of the FMWSC Model is further investigated in a Vehicle Repair Management System (VRMS). First step is describing the the stactic information of the components that compose the VRMS system. The second step is describing the interactive process of these components by using the Service Interaction Model. Then the prime properties of the system and the behavior consistency are verified. Finally, after introducing the web service composition execution language CCML (Cooperative Computation Modeling Language) and the correspondence relation between FMWSC and CCML, (part of) the CCML code of VRMS system was given.