TY - JOUR
T1 - Modelling and verifying contract-oriented systems in Maude
AU - Bartoletti, Massimo
AU - Murgia, Maurizio
AU - Scalas, Alceste
AU - Zunino, Roberto
PY - 2014/11/16
Y1 - 2014/11/16
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84911983359&partnerID=8YFLogxK
UR - https://link.springer.com/chapter/10.1007%2F978-3-319-12904-4_7
U2 - 10.1007/978-3-319-12904-4_7
DO - 10.1007/978-3-319-12904-4_7
M3 - Article
AN - SCOPUS:84911983359
VL - 8663
SP - 130
EP - 146
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
SN - 0302-9743
ER -