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.

Verifiable abstractions for contract-oriented systems

BARTOLETTI, MASSIMO
;
MURGIA, MAURIZIO;SCALAS, ALCESTE;
2017

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.
Contracts; Process calculi; Model checking
File in questo prodotto:
File Dimensione Formato  
JLAMP46-final.pdf

Solo gestori archivio

Descrizione: Articolo principale
Tipologia: versione pre-print
Dimensione 726.32 kB
Formato Adobe PDF
726.32 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/187054
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact