Abstract
The definition of choreography specification languages for Service Oriented Systems poses important challenges. Mainstream approaches tend to focus on procedural aspects, leading to over-constrained and over-specified models. Because of such a drawback, declarative languages are gaining popularity as a better way to model service choreographies. A similar issue was met in the Multi-Agent Systems domain, where declarative approaches based on social semantics have been used to capture the nature of agent interaction without over-constraining their behaviour.
In this work, we present an integrated framework capable to cover the entire cycle of specification and verification of choreographies, by mixing approaches coming from the Service Oriented Computing and Multi-Agent Systems research domains. SCIFF is the underlying logic programming framework for modelling and verifying interaction in open systems. The use of SCIFF brings us two main advantages: (1) it allows us to capture within a single framework different aspects of a choreography, ranging from constraints on the flow of messages to effects and commitments resulting from their exchange; (2) it provides an operational model that can be exploited to perform a variety of verification tasks.