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.

Foundational Aspects of Contract Compliance and Choreography Conformance

BRAVETTI, MARIO;ZAVATTARO, GIANLUIGI
2008

Abstract

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.
Microsoft Research Technical Report
11
14
M. Bravetti; G. Zavattaro
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/72723
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact