Skip to Main content Skip to Navigation
New interface
Conference papers

Choreographies and Behavioural Contracts on the Way to Dynamic Updates

Mario Bravetti 1, 2 Gianluigi Zavattaro 1, 2 
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We survey our work on choreographies and behavioural contracts in multiparty interactions. In par-ticular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous address or name based com-munication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly relations between behavioural contracts and choreographic descriptions are consid-ered, where a contract for each communicating party is, e.g., derived by projection. The considered relations are induced as the maximal preoders which preserve contract compliance and global traces: we show maximality to hold (permitting services to be discovered/substituted independently for each party) when contract refinement preorders with all the above asymmetric communication means are considered and, instead, not to hold if the standard symmetric CCS/pi-calculus communication is considered (or when directly relating choreographies to behavioral contracts via a preorder, no mat-ter the communication mean). The obtained maximal preorders are then characterized in terms of a new form of testing, called compliance testing, where not only tests must succeed but also the sys-tem under test (thus relating to controllability theory), and compared with classical preorders such as may/must testing, trace inclusion, etc. Finally, recent work about adaptable choreographies and behavioural contracts is presented, where the theory above is extended to update mechanisms allowing choreographies/contracts to be modified at run-time by internal (self-adaptation) or external intervention.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Zavattaro Gianluigi Connect in order to contact the contributor
Submitted on : Thursday, December 4, 2014 - 1:35:51 PM
Last modification on : Wednesday, February 2, 2022 - 3:56:18 PM
Long-term archiving on: : Monday, March 9, 2015 - 5:58:16 AM


Files produced by the author(s)




Mario Bravetti, Gianluigi Zavattaro. Choreographies and Behavioural Contracts on the Way to Dynamic Updates. Proceedings First Workshop on Logics and Model-checking for Self*-Systems, Sep 2014, Bertinoro (FC), Italy. pp.12 - 31, ⟨10.4204/EPTCS.168.2⟩. ⟨hal-01090924⟩



Record views


Files downloads