Shonan meeting on Software Contracts

Post date: 09-Jun-2014 08:09:09

Upcoming Seminars

A calculus of contracting systems

A theory of agreements and protection

May 29-30

Shonan meeting on Software Contracts

for Communication, Monotoring, and Security

Massimo Bartoletti

Dip. Matematica e Informatica - University of Cagliari

Abstract of the first talk.

We address the problem of modelling and verifying contract-oriented systems, wherein distributed agents may advertise and stipulate contracts, but — differently from most other approaches to distributed agents — are not assumed to always behave “honestly”.

We model such systems in CO2, a basic calculus for contract-oriented computing. CO2 features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among participants happens via multi-party sessions, which are created once agreements are reached. The possibility of not keeping promises gives rise to a rich variety of possible misbehaviours, which we illustrate with the help some examples. We discuss some verification techniques to ensure “honesty”, namely that a participant always respects her contracts, in all possible execution contexts.

The honesty property is quite strong, because it requires that a participant is capable of fulfilling her obligations also when the context plays against her. We discuss some work in progress about weaker notions of honesty (which however still guarantee safe interactions among agents), and their relation with different cases of inter-session dependencies. Our final goal is a theory for blame shifting, allowing to determine when a (not-strictly-honest) agent can blame other (dishonest) agents for her contractual violations.

Abstract of the second talk.

We present a theory of contracts, interpreted as multi-player concurrent games among competitive participants. The two key notions of our model are that of agreement and protection. The agreement property is a game-theoretic generalization of the notion of compliance typically studied in session behaviours: a participant agrees on a contract if she has a strategy to reach her goals (or make another participant chargeable for a violation), whatever the moves of her adversaries. The protection property is relevant when contract brokers are untrusted: a participant is protected by a contract when she has a strategy to defend herself in all possible contexts, even in those where she has not reached an agreement.

We show that, in a relevant class of contracts, agreements and protection mutually exclude each other. We then propose a novel formalism for modelling contractual obligations (event structures with circular causality), which allows us to construct contracts which guarantee both agreements and protection. Finally, we establish a correspondence between game-theoretic contracts and Propositional Contract Logic, by showing that winning strategies in game-theoretic contracts are related to proofs in the logic.