Foundational Aspects of Contract Compliance and Choreography Conformance

In the context of Service Oriented Computing, contracts are de- scriptions of the externally observable behaviour of services. Given a group of collaborating services, their contracts can be used to ver- ify whether their composition is sound, i.e., the services are compli- ant. In our work, we relate the theory of contracts with the notion of choreography conformance, used to check whether an aggregation of services correctly behaves according to a high level specification of their possible conversations. The main result of our work is the definition of an effective procedure that can be used to verify whether a service with a given contract can correctly play a specific role within a choreography. This procedure is achieved via composition of choreography projection and contract refinement. Our work comprises the analysis of different options for the con- tract language adopted, where either outputs and inputs are syn- chronized as in standard process algebra or a destination contract is specified in outputs, and for the notion of compliance adopted, where we consider either a standard notion of compliance which just ensures deadlock and livelock freedom or a stronger one where outputs cannot wait for the availability of a synchronizing input