Published in Volume XXII, Issue 1, 2012, pages 5-60, doi: 10.7561/SACS.2012.1.5

Authors: M. Bartoletti, E. Tuosto, R. Zunino

Abstract

We present CO2, a parametric calculus for contract-based computing in distributed systems.
By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms.
The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts.
Coordination among participants happens via multi-party sessions, which are created once agreements are reached.
We present two instances of our calculus, by modelling contracts as processes in a variant of CCS, and as formulae in a logic.
We formally relate the two paradigms, through an encoding from contracts-as-formulae to contracts-as-processes which ensures that the promises deducible in the logical system are exactly those reachable by its encoding as a process.
Finally, we present a coarse-grained taxonomy of possible misbehaviours in contract-oriented systems, and we illustrate them with the help of
a variety of examples.

Full Text (PDF)

References

[1] Alexander Artikis, Marek J. Sergot, and Jeremy V. Pitt. Specifying norm-governed computational societies. ACM Trans. Comput. Log., 10(1), 2009. http://dx.doi.org/10.1145/1459010.1459011

[2] Massimo Bartoletti, Emilio Tuosto, and Roberto Zunino. Contracts in distributed systems. In ICE, volume 59 of EPTCS, pages 130-147, 2011.http://dx.doi.org/10.4204/EPTCS.59.11

[3] Massimo Bartoletti and Roberto Zunino. A logic for contracts. Technical Report DISI-09-034, DISI – Universit a di Trento, 2009.

[4] Massimo Bartoletti and Roberto Zunino. A calculus of contracting processes. In LICS, pages 332-341. IEEE Computer Society, 2010.http://dx.doi.org/10.1109/LICS.2010.25

[5] Massimo Bartoletti and Roberto Zunino. Primitives for contract-based synchronization. In ICE, volume 38 of EPTCS, pages 67-82, 2010.

[6] Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 162-176. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-15375-4_12

[7] Mario Bravetti and Gianluigi Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. In Software Composition, volume 4829 of Lecture Notes in Computer Science, pages 34-50. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-77351-1_4

[8] Maria Grazia Buscemi and Hern an C. Melgratti. Transactional service level agreement. In TGC, volume 4912 of Lecture Notes in Computer Science, pages 124-139. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-78663-4_10

[9] Maria Grazia Buscemi and Ugo Montanari. CC-Pi: A constraint-based language for specifying service level agreements. In ESOP, volume 4421 of Lecture Notes in Computer Science, pages 18-32. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-71316-6_3

[10] Felice Cardone. The geometry and algebra of commitment. In Ludics, dialogue and interaction, pages 147-160. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-19211-1_9

[11] Samuele Carpineti, Giuseppe Castagna, Cosimo Laneve, and Luca Padovani. A formal account of contracts for web services. In WS-FM, volume 4184 of Lecture Notes in Computer Science, pages 148-162. Springer, 2006. http://dx.doi.org/10.1007/11841197_10

[12] Samuele Carpineti and Cosimo Laneve. A basic contract language for web services. In ESOP, volume 3924 of Lecture Notes in Computer Science, pages 197-213. Springer, 2006. http://dx.doi.org/10.1007/11693024_14

[13] Giuseppe Castagna, Nils Gesbert, and Luca Padovani. A theory of contracts for web services. ACM Transactions on Programming Languages and Systems, 31(5), 2009. http://dx.doi.org/10.1145/1538917.1538920

[14] Giuseppe Castagna and Luca Padovani. Contracts for mobile processes. In Proc. CONCUR, volume 5710 of Lecture Notes in Computer Science, pages 211-228. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-04081-8_15

[15] Mario Coppo and Mariangiola Dezani-Ciancaglini. Structured communications with concurrent constraints. In TGC, volume 5474 of Lecture Notes in Computer Science, pages 104-125. Springer, 2008. http://dx.doi.org/10.1007/978-3-642-00945-7_7

[16] Mads Dam. On the Decidability of Process Equivalences for the pi-calculus. Theoretical Computer Science, 183(2):215-228, 1997. http://dx.doi.org/10.1016/S0304-3975(96)00325-8

[17] E. Allen Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 995-1072. North-Holland Pub. Co./MIT Press, 1990.

[18] Gian Luigi Ferrari and Alberto Lluch-Lafuente. A logic for graphs with QoS. Electr. Notes Theor. Comput. Sci., 142:143-160, 2006. http://dx.doi.org/10.1016/j.entcs.2004.10.030

[19] Deepak Garg and Martin Abadi. A modal deconstruction of access control logics. In FoSSaCS, volume 4962 of Lecture Notes in Computer Science, pages 216-230. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-78499-9_16

[20] Thomas Hobbes. Leviathan or The Matter, Forme and Power of a Common Wealth Ecclesiasticall and Civil. 1651. Chapter XIV | Of the first and second natural laws, and of contracts.

[21] Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP, volume 1381, 1998. http://dx.doi.org/10.1007/BFb0053567

[22] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronoussession types. In POPL, pages 273-284. ACM, 2008. http://dx.doi.org/10.1145/1328438.1328472

[23] Ashley T. McNeile. Protocol contracts with application to choreographed multiparty collaborations. Service Oriented Computing and Applications, 4(2):109-136, 2010. http://dx.doi.org/10.1007/s11761-010-0060-9

[24] Robin Milner. Communication and concurrency. Prentice-Hall, Inc., 1989.

[25] Cristian Prisacariu and Gerardo Schneider. A formal language for electronic contracts. In FMOODS, volume 4468 of Lecture Notes in Computer Science, pages 174-189. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-72952-5_11

[26] Cristian Prisacariu and Gerardo Schneider. A dynamic deontic logic for complex contracts. The Journal of Logic and Algebraic Programming (JLAP), 81(4):458-490, 2012. http://dx.doi.org/10.1016/j.jlap.2012.03.003

[27] Vijay Saraswat, Prakash Panangaden, and Martin Rinard. Semantic foundations of concurrent constraint programming. In POPL, pages 333-352, 1991. http://dx.doi.org/10.1145/99583.99627

[28] Anne Troelstra and Dirk van Dalen. Constructivism in Mathematics, vol. 1. North-Holland, 1988

Bibtex

@article{sacscuza:bartoletti2013ccic,
  title={Contract-Oriented Computing in CO2},
  author={M. Bartoletti and E. Tuosto and R. Zunino},
  journal={Scientific Annals of Computer Science},
  volume={22},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2013},
  pages={5--60},
  doi={10.7561/SACS.2012.1.5},
  publisher={``A.I. Cuza'' University Press}
}