Abduction for specifying and verifying web service choreographies

Global choreographies have been recently proposed as a way for specifying the overall behaviour of a system composed of heterogeneous web services. In this work, we propose an abductive framework based on computational logic to specify both choreographies and web service interface behaviours. One of the main motivations for using computational logic is that its operational counterpart provides a proof-theoretic support able to verify, from different viewpoints, the conformance of services designed in a cooperative and incremental manner. We show how it is possible to specify both the choreography and the web service interface behaviours (restricted to the conversation aspects) using a uniform formalism based on abductive logic programs. Then, we provide a definition of conformance, and show how, by using an abductive proof procedure, it is possible to automatically verify the conformance of a given web service w.r.t. a certain choreography.