Establishing Conformance between Contracts and Choreographies

In a business-to-business collaborative setting, a choreography and a business contract (service agreement) are two specifications that describe permissible interactions between partners from different view points, emphasising different aspects. A choreography specification is a description, from a global perspective, of all permissible message exchange sequences between the partners. A business contract on the other hand specifies what operations the business partners have the rights, obligations or prohibitions to execute, it also stipulates when the operations are to be executed and in which order. It is naturally important to make sure that message exchanges as encoded in a given choreography conform to (are in accordance with) the contract between the partners. In other words, make sure that any message interaction permitted in the choreography will not cause a breach of the contract. The paper develops the concept of conformance between a contract and a choreography assuming that they can be modelled by Finite Automata. This approach opens the way for automatically establishing conformance by using model checking techniques.