Automatic Composition Of Semantic Web Services

This dissertation is focused on the research of the methodology of automatic composition of Semantic Web Services.The three main parts of this research are:Semantic of Web Services,Composite Web Services,and Automatic Service Composition.All the research of this work is based on the "Semantic" of Web Services."Semantic" is one of the most important parts of the Semantic Web Services architecture.Service is regarded as a special kind of software component.Its "IOPEV",which stand for Input,Output,Precondition, Effect,and IO-Vinculum,are selected as the 5-essentials for the definition of the "semantic" of service.The semantic relations between services are analyzed based on this definition.The "Semantic Match" is formally and strictly defined.A thoroughly discussion is given to the Composite Services,which are the output of Service Composition.Composite Services are basically execution flows of its component services.Two formal representing methods for Composite Services are defined,both based on pi-Calculus. One of the methods is from the viewpoint of Data-Flow Model(DFM)and the other from Centralized-Control Model(CCM).The Semantic-Calculus Algorithm(SCA)is defined to calculus the semantic of the composite service from its components,which is the basis for service verification.A mapping(CCM2BPEL)is defined to generate BPEL script from CCM representation.A transformation(DFM2CCM)from DFM representation to CCM representation is also defined.Taking the "Proof as Programs Principle" as background theory,and the "Deductive Program Synthesis Method" as blueprint reference,an integrated solution for automatic composition of services is proposed. Following a template,the semantic of service is transformed into a First-Order Logic formula.The available services are treated as known theorems and the object service as an un-proven theorem.Import method is defined to lead the semantic information of OWL ontology and background knowledge into the process of proof.An automatic theorem prover is applied to perform the proving from known theorems to un-proven theorem. Finally,by using the Composite-Service Extract Algorithm(CSEA),the implementation of the object service is extracted from the proof.The complete path from requirement to implementation is solved as: "Problem→Proof→DFM→CCM→BPEL".The "proof to program" approach applied in this solution given a completeness and correctness guarantee to the composition result.An example is used to illustrate every important part of the whole solution.A prototype system is implemented to give an elementary verification of the feasibility of the result.