Contract Compliance and Choreography Conformance in the Presence of Message Queues

摘要

Choreography conformance and contract compliance have been widely studied in the context of synchronous communication. In this paper we approach a more realistic scenario in which the messages containing the invocations are queued in the called service. More precisely, we study the foundational aspects of contract compliance in a language independent way by just taking contracts to be finite labeled transition systems. Then, we relate the proposed theory of contract compliance with choreography specifications a la WS-CDL where activities are interpreted as pairs of send and receive events. An interesting consequence of adopting a language independent representation of contracts is that choreography projection can be defined in structured operational semantics.