Realizability of Choreographies for Services Interacting Asynchronously

  • Gregor Gössler
  • Gwen Salaün
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7253)


Choreography specification languages describe from a global point of view interactions among a set of services in a system to be designed. Given a choreography specification, the goal is to obtain a distributed implementation of the choreography as a system of communicating peers. These peers can be given as input (e.g., obtained using discovery techniques) or automatically generated by projection from the choreography. Checking whether some set of peers implements a choreography specification is called realizability. This check is in general undecidable if asynchronous communication is considered, that is, services interact through message buffers. In this paper, we consider conversation protocols as a choreography specification language, and leverage a recent decidability result to check automatically the realizability of these specifications by a set of peers under an asynchronous communication model with a priori unbounded buffers.


Label Transition System Asynchronous Communication Outgoing Transition Message Sequence Chart Internal Choice 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 305–318. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. IEEE Transactions on Software Engineering 29(7), 623–633 (2003)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Etessami, K., Yannakakis, M.: Realizability and Verification of MSC Graphs. Theoretical Computer Science 331(1), 97–114 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Basu, S., Bultan, T.: Choreography Conformance via Synchronizability. In: Proc. WWW 2011. ACM Press (2011)Google Scholar
  5. 5.
    Bultan, T., Fu, X.: Specification of Realizable Service Conversations using Collaboration Diagrams. Service Oriented Computing and Applications 2(1), 27–39 (2008)CrossRefGoogle Scholar
  6. 6.
    Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Choreography and Orchestration Conformance for System Design. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 63–81. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    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
  8. 8.
    Cortadella, J., Kondratyev, A., Lavagno, L., Passerone, C., Watanabe, Y.: Quasi-Static Scheduling of Independent Tasks for Reactive Systems. IEEE Trans. on CAD of Integrated Circuits and Systems 24(10), 1492–1514 (2005)CrossRefGoogle Scholar
  9. 9.
    Darondeau, P., Genest, B., Thiagarajan, P.S., Yang, S.: Quasi-Static Scheduling of Communicating Tasks. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 310–324. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Deniélou, P.-M., Yoshida, N.: Buffered Communication Analysis in Distributed Multiparty Sessions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 343–357. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    Fu, X., Bultan, T., Su, J.: Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services. Theor. Comput. Sci. 328(1-2), 19–37 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Fu, X., Bultan, T., Su, J.: Synchronizability of Conversations among Web Services. IEEE Transactions on Software Engineering 31(12), 1042–1055 (2005)CrossRefGoogle Scholar
  13. 13.
    Genest, B., Kuske, D., Muscholl, A.: A kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput. 204(6), 920–956 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1984)Google Scholar
  15. 15.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison Wesley (1979)Google Scholar
  16. 16.
    Jéron, T., Jard, C.: Testing for Unboundedness of FIFO Channels. Theor. Comput. Sci. 113(1), 93–117 (1993)zbMATHCrossRefGoogle Scholar
  17. 17.
    Kazhamiakin, R., Pistore, M.: Analysis of Realizability Conditions for Web Service Choreographies. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 61–76. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Leue, S., Mayr, R., Wei, W.: A Scalable Incomplete Test for Message Buffer Overflow in Promela Models. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 216–233. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Leue, S., Mayr, R., Wei, W.: A Scalable Incomplete Test for the Boundedness of UML RT Models. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 327–341. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Li, J., Zhu, H., Pu, G.: Conformance Validation between Choreography and Orchestration. In: Proc. TASE 2007, pp. 473–482. IEEE Computer Society (2007)Google Scholar
  21. 21.
    Lohmann, N., Wolf, K.: Realizability Is Controllability. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 110–127. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  22. 22.
    Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the Theoretical Foundation of Choreography. In: Proc. WWW 2007, pp. 973–982. ACM Press (2007)Google Scholar
  23. 23.
    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
  24. 24.
    Su, J., Bultan, T., Fu, X., Zhao, X.: Towards a Theory of Web Service Choreographies. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 1–16. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  25. 25.
    Tivoli, M., Fradet, P., Girault, A., Gössler, G.: Adaptor Synthesis for Real-Time Components. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 185–200. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  26. 26.
    Uchitel, S., Kramer, J., Magee, J.: Incremental Elaboration of Scenario-based Specifications and Behavior Models using Implied Scenarios. ACM Transactions on Software Engineering and Methodology 1(13), 37–85 (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Gregor Gössler
    • 1
  • Gwen Salaün
    • 2
  1. 1.INRIA Grenoble – Rhône-AlpesFrance
  2. 2.Grenoble INP, INRIAFrance

Personalised recommendations