Verification of contract-oriented systems

In this thesis 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 respect them. A key issue is that the honesty property, which characterises those agents which respect their contracts in all possible execution contexts, is undecidable in general. We develop a sound verification technique for honesty, targeted at agents modelled in a value-passing version of the calculus CO2. To do that, we safely over-approximate the honesty property by abstracting from the actual values and from the contexts a process may be engaged with. We develop a model-checking technique for this abstraction, we describe its implementation in Maude, and we discuss some experiments with it. We then introduce timed session types, an extension of binary session types, formalising timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one, and if so, to construct the most precise session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results.