Choreographies and Behavioural Contracts on the Way to Dynamic Updates

TL;DR

This paper surveys theories of behavioural contracts and choreographies in multiparty interactions, focusing on correctness, substitutability, and dynamic updates under various communication assumptions, with new testing-based characterizations.

Contribution

It introduces a new compliance testing approach for behavioural contracts and explores their relation to choreographies, including extensions for runtime updates and self-adaptation.

Findings

Maximal preorders preserve contract compliance and global traces.

Compliance testing relates to controllability and differs from classical testing preorders.

Extensions enable runtime modifications of choreographies and contracts.

Abstract

We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular 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 communication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly relations between behavioural contracts and choreographic descriptions are considered, 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 matter 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 system 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.