Model checking is a formal verification method widely accepted in the web service world because of its capability to reason about service behavior at process level. It has been used as a basic tool in several scenarios such as service selection, service validation, and service composition. The importance of semantics is also widely recognized. Indeed, there are several solutions to the problem of providing semantics to web services, most of them relying on some form of Description Logic. This paper presents an integration of model checking and semantic reasoning technologies in an efficient way. This can be considered the first step toward the use of semantic model checking in problems of selection, validation, and composition. The approach relies on a representation of services at process level that is based on semantically annotated state transition systems (asts) and a representation of specifications based on a semantically annotated version of computation tree logic (anctl). This paper proves that the semantic model checking algorithm is sound and complete and can be accomplished in polynomial time. This approach has been evaluated with several experiments.

Several approaches have been proposed to tackle the selection of distributed processes described as semantic Web services. However, their practical applicability in real composition scenarios is still an open question. Addressing this problem requires on the one hand to deal with services described as stateful business processes and, on the other hand, to consider complex selection requirements concerning both the service interface and its behavior. In fact, in most existing approaches the selection is performed on the basis of the ldquofunctionalrdquo description of a service, i.e. in terms of its inputs, outputs, preconditions and effects. In this paper, we present our approach for the process-level service selection and evaluate it on a real world scenario that entails a high level of complexity: the eBay Web Services,the Amazon E-Commerce Services and the e-payment service offered by PayPal. The approach is based on a representation of services at the process level that is based on BPEL and WSDL specifications and that extends these standard specifications with minimal semantic annotations that permit to perform an efficient and yet useful, semantic reasoning for the process-level selection of Web services.