Modelling and verifying contract-oriented systems in Maude

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 contractoriented 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 describe an executable specification in Maude of the semantics of CO2, a calculus for contract-oriented systems [6]. The honesty property [5] characterises those agents which always respect their contracts, in all possible execution contexts. Since there is an infinite number of such contexts, honesty cannot be directly verified by model-checking the state space of an agent (indeed, honesty is an undecidable property in general [5]). The main contribution of this paper is a sound verification technique for honesty. To do that, we safely over-approximate the honesty property by abstracting from the actual contexts a process may be engaged with. Then, we develop a model-checking technique for this abstraction, we describe an implementation in Maude, and we discuss some experiments with it.

Original languageEnglish
Pages (from-to)130-146
Number of pages17
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8663
DOIs
Publication statusPublished - 16 Nov 2014

Fingerprint Dive into the research topics of 'Modelling and verifying contract-oriented systems in Maude'. Together they form a unique fingerprint.

Cite this