Abstract
Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings. A common problem is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the user's goals. In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules. Suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined.
Building on our experience in the MAS area, in this paper we make a first step towards the formal verification of web services conformance to choreographies in Abductive Logic Programming.We adapt the SCIFF framework for the new settings, and propose a heir of SCIFF, the framework AlLoWS (Abductive Logic Web-service Specification). AlLoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, AlLoWS has a declarative and an operational semantics. We show examples of how AlLoWS deals correctly with interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, AlLoWS deals seamlessly with other cases involving constraints and deadlines.