Published in Volume XXII, Issue 1, 2012, pages 61-104, doi: 10.7561/SACS.2012.1.61

Authors: L. Bocchi, J. Lange, E. Tuosto


Distributed interactions are crucial design aspects to consider in modern applications. They can be suitably designed in terms of choreographies, that are global descriptions of the coordination of several distributed parties. Global assertions define contracts for choreographies by annotating multiparty session types with logical formulae to validate the content of the exchanged messages. The introduction of such constraints is a critical design issue as it may be hard to specify contracts that allow each party to be able to progress without violating the contract. We propose three algorithms to correct inconsistent global assertions. The methods are compared by discussing their applicability and the relationships between the amended global assertions and the original (inconsistent) ones. Also, we specify a methodology that exploits our algorithms to help designers to amend their choreographies. To show how the methodology can be applied we consider a simple scenario.

Full Text (PDF)


[1] R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts. In Software Concepts and Tools, pages 304-313, 2003.

[2] K. R. Apt, N. Francez, and S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226-241, 1988.

[3] L. Bocchi, K. Honda, E. Tuosto, and N. Yoshida. A theory of design-by-contract for distributed multiparty interactions. In Paul Gastin and Francois Laroussinie, editors, CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 162-176. Springer, 2010.

[4] L. Bocchi, J. Lange, and E. Tuosto. Amending contracts for choreographies. In A. Silva, S. Bliudze, R. Bruni, and M. Carbone, editors, ICE, volume 59 of EPTCS, pages 111-129, 2011.

[5] Maria Grazia Buscemi and Ugo Montanari. Cc-pi: A constraint-based language for specifying service level agreements. In Rocco De Nicola, editor, ESOP, volume 4421 of Lecture Notes in Computer Science, pages 18-32. Springer, 2007.

[6] Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centred programming for web services. In Rocco De Nicola, editor, ESOP, volume 4421 of Lecture Notes in Computer Science, pages 2-17. Springer, 2007.

[7] Tzu-Chun Chen, Laura Bocchi, Pierre-Malo Denielou, Kohei Honda, and Nobuko Yoshida. Asynchronous distributed monitoring for multiparty session enforcement. In Roberto Bruni and Vladimiro Sassone, editors, TGC’11, LNCS. Springer, 2011. To appear.

[8] K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, POPL, pages 273-284. ACM, 2008.

[9] Julien Lange and Emilio Tuosto. A modular toolkit for distributed interactions. In Kohei Honda and Alan Mycroft, editors, PLACES, volume 69 of EPTCS, pages 92-110, 2010.

[10] Sjouke Mauw. The formalization of message sequence charts. Computer Networks and ISDN Systems, 28(12):1643-1657, 1996.

[11] B. Meyer. Object-Oriented Software Construction (Chapter 31). Prentice Hall, 1997.

[12] Sebastian Uchitel, Jeff Kramer, and Jeff Magee. Detecting implied scenarios in message sequence chart specifications. In ESEC / SIGSOFT FSE, pages 74-82, 2001.

[13] Nobuko Yoshida, Pierre-Malo Denielou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. In C.-H. Luke Ong, editor, FOSSACS, volume 6014 of Lecture Notes in Computer Science, pages 128-145. Springer, 2010.


  title={Three Algorithms and a Methodology for Amending Contracts for Choreographies},
  author={L. Bocchi and J. Lange and E. Tuosto},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}