CINECA IRIS Institutional Research Information System
IRIS è l'Anagrafe della ricerca dell'Università degli Studi di Trento, e ha lo scopo di raccogliere, documentare, conservare e diffondere, anche ad accesso aperto, la produzione scientifica degli autori afferenti all'Università degli Studi di Trento.
EnglishWe 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; Zunino, Roberto. - In: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING. - ISSN 2352-2216. - 86:1(2017), pp. 159-207. [10.1016/j.jlamp.2015.10.005]
| Titolo: | Verifiable abstractions for contract-oriented systems | |
| Autori: | Bartoletti, Massimo; Murgia, Maurizio; Scalas, Alceste; Zunino, Roberto | |
| Autori Unitn: | ||
| Titolo del periodico: | THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING | |
| Anno di pubblicazione: | 2017 | |
| Numero e parte del fascicolo: | 1 | |
| Codice identificativo Scopus: | 2-s2.0-85010874826 | |
| Codice identificativo WOS: | WOS:000390497700008 | |
| Digital Object Identifier (DOI): | http://dx.doi.org/10.1016/j.jlamp.2015.10.005 | |
| Handle: | http://hdl.handle.net/11572/171597 | |
| Citazione: | Verifiable abstractions for contract-oriented systems / Bartoletti, Massimo; Murgia, Maurizio; Scalas, Alceste; Zunino, Roberto. - In: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING. - ISSN 2352-2216. - 86:1(2017), pp. 159-207. [10.1016/j.jlamp.2015.10.005] | |
| Appare nelle tipologie: | 03.1 Articolo su rivista (Journal article) |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| VerifiableAbstractionsForContractOrientedSystems-JLAMP2017.pdf | Versione editoriale (Publisher’s layout) | Tutti i diritti riservati (All rights reserved) | Administrator |
http://hdl.handle.net/11572/171597
Copyright © 2022