Skip to Main content Skip to Navigation
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

https://hal.inria.fr/hal-01090924
Contributor : Zavattaro Gianluigi Connect in order to contact the contributor
Submitted on : Thursday, December 4, 2014 - 1:35:51 PM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM
Long-term archiving on: : Monday, March 9, 2015 - 5:58:16 AM

File

MODstar2014.pdf
Files produced by the author(s)

Identifiers

Collections

`

Citation

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⟩

Share

Metrics

Record views

227

Files downloads

296