Verifiable abstractions for contract-oriented systems

Massimo Bartoletti*, Maurizio Murgia, Alceste Scalas, Roberto Zunino

*Corresponding author for this work

Research output: Contribution to journalArticle

Abstract

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. The main contribution of this paper is 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. Then, we develop a model-checking technique for this abstraction, we describe its implementation in Maude, and we discuss some experiments with it.

Original languageEnglish
Pages (from-to)159-207
Number of pages49
JournalJournal of Logical and Algebraic Methods in Programming
Volume86
Issue number1
Early online date2 Nov 2015
DOIs
Publication statusPublished - 1 Jan 2017

Keywords

  • Contract-oriented computing
  • Rewriting logic
  • Session types
  • Verification

Fingerprint Dive into the research topics of 'Verifiable abstractions for contract-oriented systems'. Together they form a unique fingerprint.

Cite this