Contracts in distributed systems
Massimo Bartoletti (Dipartimento di Matematica e Informatica,, Universita' degli Studi di Cagliari, Italy), Emilio Tuosto (Department of, Computer Science, University of Leicester, UK), Roberto Zunino, (DISI-Universita' degli Studi di Trento, COSBI, Italy)
TL;DR
This paper introduces a flexible calculus for contract-based computing in distributed systems, unifying different contract paradigms and enabling coordination through multi-party sessions.
Contribution
It presents a parametric calculus that generalizes contracts-as-processes and contracts-as-formulae, with primitives for advertising, agreement, and fulfillment queries.
Findings
Two instances modeled as CCS processes and logical formulae
Primitives demonstrated through examples
Framework supports various contract paradigms
Abstract
We present a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among principals happens via multi-party sessions, which are created once agreements are reached. We present two instances of our calculus, by modelling contracts as (i) processes in a variant of CCS, and (ii) as formulae in a logic. With the help of a few examples, we discuss the primitives of our calculus, as well as some possible variants.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge