Semantic Web Service Composition Using Formal Verification Techniques

Web service is a software system designed to support interoperable machine-to-machine interaction over a network. The web service composition problem aims to find an optimal composition of web services to satisfy a given request by using their syntactic and/or semantic features when no single service satisfies it. In particular, the semantics of services helps a composition engine identify more correct, complete and optimal candidates as a solution. In this paper, we study the web service composition problem considering semantic aspects, i.e., exploiting the semantic relationship between parameters of web services. Given a set of web service descriptions, their semantic information and a requirement web service, we find the optimal composition that contains the shortest path of semantically well connected web services which satisfies the requirement. Our techniques are based on semantic matchmaking and two formal verification techniques such as boolean satisfiability solving and symbolic model checking. In a preliminary experiment, our proposal efficiently identify optimal compositions of web services.