Choreography synthesis as contract agreement

Julien Lange, Alceste Scalas

Research output: Contribution to journalConference article

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 type literature. It supports sessions where the number of participants is not determined beforehand, and keeps CO2’s ability to rule out participants that are culpable if contracts are not fulfilled at runtime. We show that we have progress and session fidelity in CO2, as a result of the honesty of participants — i.e., their ability to always adhere to their contracts.

Original languageEnglish
Pages (from-to)52-67
Number of pages16
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume131
DOIs
Publication statusPublished - 15 Oct 2013
Event6th Interaction and Concurrency Experience, ICE 2013 - Florence, Italy
Duration: 6 Jun 2013 → …

Cite this

Lange, J., & Scalas, A. (2013). Choreography synthesis as contract agreement. Electronic Proceedings in Theoretical Computer Science, EPTCS, 131, 52-67. https://doi.org/10.4204/EPTCS.131.6
Lange, Julien ; Scalas, Alceste. / Choreography synthesis as contract agreement. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. 2013 ; Vol. 131. pp. 52-67.
@article{8e857ac853aa4192b1523ed3f69f85da,
title = "Choreography synthesis as contract agreement",
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 type literature. It supports sessions where the number of participants is not determined beforehand, and keeps CO2’s ability to rule out participants that are culpable if contracts are not fulfilled at runtime. We show that we have progress and session fidelity in CO2, as a result of the honesty of participants — i.e., their ability to always adhere to their contracts.",
author = "Julien Lange and Alceste Scalas",
year = "2013",
month = "10",
day = "15",
doi = "10.4204/EPTCS.131.6",
language = "English",
volume = "131",
pages = "52--67",

}

Lange, J & Scalas, A 2013, 'Choreography synthesis as contract agreement', Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 131, pp. 52-67. https://doi.org/10.4204/EPTCS.131.6

Choreography synthesis as contract agreement. / Lange, Julien; Scalas, Alceste.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 131, 15.10.2013, p. 52-67.

Research output: Contribution to journalConference article

TY - JOUR

T1 - Choreography synthesis as contract agreement

AU - Lange, Julien

AU - Scalas, Alceste

PY - 2013/10/15

Y1 - 2013/10/15

N2 - 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 type literature. It supports sessions where the number of participants is not determined beforehand, and keeps CO2’s ability to rule out participants that are culpable if contracts are not fulfilled at runtime. We show that we have progress and session fidelity in CO2, as a result of the honesty of participants — i.e., their ability to always adhere to their contracts.

AB - 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 type literature. It supports sessions where the number of participants is not determined beforehand, and keeps CO2’s ability to rule out participants that are culpable if contracts are not fulfilled at runtime. We show that we have progress and session fidelity in CO2, as a result of the honesty of participants — i.e., their ability to always adhere to their contracts.

UR - http://www.scopus.com/inward/record.url?scp=85069739472&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.131.6

DO - 10.4204/EPTCS.131.6

M3 - Conference article

AN - SCOPUS:85069739472

VL - 131

SP - 52

EP - 67

ER -

Lange J, Scalas A. Choreography synthesis as contract agreement. Electronic Proceedings in Theoretical Computer Science, EPTCS. 2013 Oct 15;131:52-67. https://doi.org/10.4204/EPTCS.131.6