CO2 model checker

We address the problem of modelling and verifying contract-oriented systems, wherein distributed agents may advertise and stipulate contracts, but - differently to most other approaches to distributed agents - are not assumed to always behave "honestly".

We describe an executable specification in Maude of the semantics of CO₂, a calculus for contract-oriented systems. The honesty property 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).

The main contribution 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.

Publications and downloads

Some of the publications below are accompanied by a CO₂ implementation in Maude. In order to use the latter, simply extract the .tar.gz file: the resulting directory contains a README with instructions for running the examples and tests.

• M. Bartoletti, M. Murgia, A. Scalas, R. Zunino. Verifiable abstractions for contract-oriented systems. Submitted paper, 2014.
  • implementation: co2-abstract-maude.tar.gz (last update: Sep 22, 2014)
• M. Bartoletti, M. Murgia, A. Scalas, R. Zunino. Modelling and verifying contract-oriented systems in Maude (long version). In Proc. WRLA, 2014 (to appear).
  • implementation: co2-model-checking.tar.gz (last update: Dec 31, 2013)
• M. Bartoletti, A. Scalas, E. Tuosto, R. Zunino. Honesty by typing.In Proc. FORTE/FMOODS, 2013.
• M. Bartoletti, E. Tuosto, R. Zunino. Contract-oriented Computing in CO2. In Scientific Annals of Computer Science, 22(1), 2012.
• M. Bartoletti, E. Tuosto, R. Zunino. On the realizability of contracts in dishonest systems. In Proc. COORDINATION, 2012.
• M. Bartoletti and R. Zunino. A calculus of contracting processes. In Proc. IEEE Logics in Computer Science (LICS), 2010.

Acknowledgements

This research has been partially supported by the following projects:

• Autonomous Region of Sardinia grant L.R.7/2007 CRP-17285 TRICS
• Autonomous Region of Sardinia P.I.A. 2010 Social Glue
• MIUR PRIN 2010-11 project Security Horizons
• EU COST Action IC1201 "Behavioural Types for Reliable Large-Scale Software Systems"(BETTY).