The authors discuss the interplay between the notions of contract compliance, contract refinement, and choreography conformance in the context of service oriented computing, by considering both synchronous and asynchronous communication. Service contracts are specified in a language independent way by means of finite labeled transition systems. In this way, the theory is general and foundational as the authors abstract away from the syntax of contracts and simply assume that a contract language has an operational semantics defined in terms of a labeled transition system. The chapter makes a comparative analysis of synchronous and asynchronous communication. Concerning the latter, a realistic scenario is considered in which services are endowed with queues used to store the received messages. In the simpler context of synchronous communication, the authors are able to resort to the theory of fair testing to provide decidability results.
TopIntroduction
In the context of Service Oriented Computing (SOC) the problem of the specification of service composition is addressed using two main approaches: service orchestration and service choreography. According to the first approach, the activities of the composed services are coordinated by a specific component, called the orchestrator, that is responsible for invoking the composed services and collect their responses. Several languages have been proposed for programming orchestrators such as WS-BPEL (OASIS, 2007). As far as choreography languages are concerned, the two main representatives are WS-CDL (W3C, 2005) and BPEL4Chor (Decker, Kopp, Leymann & Weske, 2007). Differently from orchestration languages, choreography languages admit the direct interaction among the combined services without the mediation of the orchestrator. In WS-CDL, the basic activity is the interaction between a sender and a receiver, while according to the BPEL4Chor approach a choreography is obtained as the parallel composition of processes that independently execute send and receive activities.
Given an orchestrator (resp. a choreography), one of the main challenges for the SOC community is the definition of appropriate mechanisms for the (semi)automatic retrieval of services that, once combined with the orchestrator (resp. once reciprocally combined), are guaranteed to implement a correct service composition. The currently investigated approach for solving this problem is to associate to each available service a behavioral description that describes the externally observable message-passing behavior of the service itself. In the literature, this description is known with the name of behavioral signature (Rajamani & Rehof, 2002), contract (Fournet, Hoare, Rajamani & Rehof, 2004), or in the specific SOC area, service contract (Carpineti, Castagna, Laneve & Padovani, 2006) (Bravetti & Zavattaro, 2007b) (Laneve & Padovani, 2007) (Castagna, Padovani & Gesbert, 2008). Assuming that services expose their contract, the above problem can be rephrased as follows: given an orchestrator (resp. a choreography) and a set of service contracts, check whether the services exposing the given contracts can be safely combined with the orchestrator (resp. safely reciprocally combined). The proposed theories of contracts solve this problem by formalizing the following notions: contract compliance (if a set of contracts is compliant then the corresponding services can be safely combined), contract refinement (if a service exposes a refinement of the contract of another service then the former is a safe substitute for the latter), and choreography conformance (if the contract of a service is conformant with a given role of a choreography then the service can be used to implement that role in any implementation of the choreography).
In this chapter we summarize the main results reported in Bravetti & Zavattaro (2007a) and Bravetti & Zavattaro (2009) about two theories for contract compliance, contract refinement, and choreography conformance. In Bravetti & Zavattaro (2007a) synchronous communication is considered, while in Bravetti & Zavattaro (2009) asynchronous communication is modeled by considering a more realistic scenario in which contracts are endowed with queues used to store the received messages. The main novelty of this chapter is the uniform presentation of the two theories. In fact, in Bravetti & Zavattaro (2007a) contracts are represented as terms of a specific process algebra thus the obtained results apply only to this specific language. On the contrary, in Bravetti & Zavattaro (2009) contracts are specified in a language independent way by means of finite labeled transition systems. In this chapter we adopt the second approach for both the theories thus obtaining more general and foundational results that can be applied to any contract language which has an operational semantics defined in terms of a labeled transition system.
The uniform presentation of the synchronus and asynchronous cases also allows us to better appreciate the impact of the addition of queues to the developed theories.