Incremental Construction of Realizable Choreographies

  • Sarah Benyagoub
  • Meriem Ouederni
  • Yamine Aït-AmeurEmail author
  • Atif Mashkoor
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)


This paper proposes a correct-by-construction method to build realizable choreographies described using conversation protocols (\( CP \)s). We define a new language consisting of an operators set for incremental construction of CPs. We suggest an asynchronous model described with the Event-B method and its refinement strategy, ensuring the scalability of our approach.


Realisability Conversation protocols Correct-by-construction method proof and refinement Event-B 


  1. 1.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253–284 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefzbMATHGoogle Scholar
  3. 3.
    Athalye, A.: CoqIOA: A formalization of IO automata in the Coq proof assistant, vol. 1019, pp. 1–53 (1995)Google Scholar
  4. 4.
    Babin, G., Ait-Ameur, Y., Pantel, M.: Correct instantiation of a system reconfiguration pattern: a proof and refinement-based approach. In: Proceedings of HASE 2016, pp. 31–38. IEEE Computer Society (2016)Google Scholar
  5. 5.
    Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Proceedings of POPL 2012, pp. 191–202. ACM (2012)Google Scholar
  6. 6.
    Benyagoub, S., Ouederni, M., Ait-Ameur, Y.: Towards correct evolution of conversation protocols. In: Proceedings of VECOS 2016. CEUR Workshop Proceedings, vol. 1689, pp. 193–201. (2016)Google Scholar
  7. 7.
    Benyagoub, S., Ouederni, M., Singh, N.K., Ait-Ameur, Y.: Correct-by-construction evolution of realisable conversation protocols. In: Bellatreche, L., Pastor, Ó., Almendros Jiménez, J.M., Aït-Ameur, Y. (eds.) MEDI 2016. LNCS, vol. 9893, pp. 260–273. Springer, Cham (2016). CrossRefGoogle Scholar
  8. 8.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Bultan, T.: Modeling interactions of web software. In: Proceedings of IEEE WWV 2006, pp. 45–52 (2006)Google Scholar
  10. 10.
    Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  11. 11.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). CrossRefGoogle Scholar
  12. 12.
    Decker, G., Weske, M.: Local enforceability in interaction petri nets. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 305–319. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  13. 13.
    Farah, Z., Ait-Ameur, Y., Ouederni, M., Tari, K.: A correct-by-construction model for asynchronously communicating systems. Int. J. STTT 19, 1–21 (2016)Google Scholar
  14. 14.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison Wesley, Boston (1979)zbMATHGoogle Scholar
  15. 15.
    Bendisposto, J., Clark, J., Dobrikov, I., Karner, P., Krings, S., Ladenberger, L., Leuschel, M., Plagge, D.: Prob 2.0 tutorial. In: Proceedings of of 4th Rodin User and Developer Workshop, TUCS (2013)Google Scholar
  16. 16.
    Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)zbMATHGoogle Scholar
  17. 17.
    Müller, O., Nipkow, T.: Combining model checking and deduction for I/O- automata. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 1–16. Springer, Heidelberg (1995). CrossRefGoogle Scholar
  18. 18.
    OMG: Business Process Model and Notation (BPMN) - Version 2.0 (2011)Google Scholar
  19. 19.
    Project RODIN: Rigorous open development environment for complex systems (2004).
  20. 20.
    Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the theoretical foundation of choreography. In: Proceedings of WWW 2007. ACM Press (2007)Google Scholar
  21. 21.
    Salaün, G., Bultan, T.: Realizability of choreographies using process algebra encodings. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 167–182. Springer, Heidelberg (2009). CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Sarah Benyagoub
    • 1
    • 2
  • Meriem Ouederni
    • 2
  • Yamine Aït-Ameur
    • 2
    Email author
  • Atif Mashkoor
    • 3
  1. 1.University of MostaganemMostaganemAlgeria
  2. 2.INP-ENSEEIHT/IRITUniversité de ToulouseToulouseFrance
  3. 3.SCCH GmbH and Johannes Kepler UniversityLinzAustria

Personalised recommendations