Choreography synthesis as contract agreement

Post date: 24-Apr-2013 15:41:48

Upcoming paper (to be presented at ICE 2013, Florence, June 6 2013)

Choreography synthesis as contract agreement

J. Lange and A. Scalas

Abstract. We propose a formal model for distributed systems, where each participant advertises its requirements and obligations as behavioural contracts, and where multiparty sessions are started when a set of contracts allows to synthesise a choreography. Our framework is based on the CO2 calculus for contract-oriented computing, and borrows concepts and results from the session types literature.

It supports sessions where the number of participants is not determined beforehand, and keeps CO2's ability to rule out which participants are culpable if contracts are not fulfilled at runtime. We show that we have progress and session fidelity, as a result of the honesty of participants - i.e., their ability to always adhere to their contracts.