Foundational aspects of contract compliance and choreography conformance

Mario Bravetti

ABSTRACT: 
A choreography is the description of the behaviour of a group of
interacting participants. Two main approaches are considered in the
context of service oriented computing for the description of
choreographies, the WS-CDL approach (expressing the global view of
participant interactions) and the BPEL4Chor approach (describing the
sequence of invoke and receive operations executed by each
participant). Given a choreography, expressed in one of the two
approaches, we consider the problem of independently retrieving
services that, once combined, correctly implement the
choreography. The theory that we propose to address this problem
assumes that each available service publishes its externally
observable message passing behaviour in a so-called service
contract. In order to check whether a service correctly implements a
given participant in a choreography, we first extract from the
choreography description the contract representing that participant,
then we check whether the contract of the considered service refines
it.