No.050 Software Contracts for Communication, Monitoring, and Security

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.