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.
Type de document :
Communication dans un congrès
Proceedings First Workshop on Logics and Model-checking for Self*-Systems, Sep 2014, Bertinoro (FC), Italy. pp.12 - 31, 2014, 〈10.4204/EPTCS.168.2〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01090924
Contributeur : Zavattaro Gianluigi <>
Soumis le : jeudi 4 décembre 2014 - 13:35:51
Dernière modification le : samedi 27 janvier 2018 - 01:31:03
Document(s) archivé(s) le : lundi 9 mars 2015 - 05:58:16

Fichier

MODstar2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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, 2014, 〈10.4204/EPTCS.168.2〉. 〈hal-01090924〉

Partager

Métriques

Consultations de la notice

144

Téléchargements de fichiers

62