A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies

  • Huu Nghia Nguyen
  • Pascal Poizat
  • Fatiha Zaïdi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7636)


Checking choreography conformance aims at verifying whether a set of distributed peers or local role specifications match a global specification. This activity is central in both top-down and bottom-up development processes for distributed systems. Such systems usually collaborate through information exchange, thus requiring value-passing choreography languages and models. However, most of the conformance checking techniques abstract value-passing or bound the domains for the exchanged data. As an alternative, we propose to rely on symbolic models and an extension of the symbolic bisimulation equivalence. This enables one to take into account value passing while avoiding state space explosion issues. Our framework is fully tool supported.


choreography specification conformance symbolic transition systems symbolic branching bisimulation tools 


  1. 1.
    Poizat, P.: Formal Model-Based Approaches for the Development of Composite Systems. Habilitation thesis, Université Paris Sud (November 2011),
  2. 2.
    Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the Theoretical Foundation of Choreography. In: Proc. of WWW 2007 (2007)Google Scholar
  3. 3.
    Basu, S., Bultan, T.: Choreography Conformance via Synchronizability. In: Proc. of WWW 2011 (2011)Google Scholar
  4. 4.
    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
  5. 5.
    Li, J., Zhu, H., Pu, G.: Conformance Validation between Choreography and Orchestration. In: Proc. of TASE 2007 (2007)Google 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.
    Kazhamiakin, R., Pistore, M.: Choreography Conformance Analysis: Asynchronous Communications and Information Alignment. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 227–241. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Van Glabbeek, R., Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3) (1996)Google Scholar
  9. 9.
    Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138(2), 353–389 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Lin, H.: Symbolic Transition Graph with Assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  11. 11.
    Li, Z., Chen, H.: Computing Strong/Weak Bisimulation Equivalences and Observation Congruence for Value-Passing Processes. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 300–314. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  12. 12.
    Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.: Local and Symbolic Bisimulation Using Tabled Constraint Logic Programming. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 166–180. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Bravetti, M., Zavattaro, G.: Towards a Unifying Theory for Choreography Conformance and Contract Compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Nguyen, H.N., Poizat, P., Zaïdi, F.: A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. Long version, in P. Poizat WebpageGoogle Scholar
  15. 15.
    Decker, G., Kopp, O., Barros, A.P.: An Introduction to Service Choreographies. Information Technology 50(2), 122–127 (2008)Google Scholar
  16. 16.
    Kopp, O., Leymann, F.: Do We Need Internal Behavior in Choreography Models? In: Proc. of ZEUS 2009 (2009)Google Scholar
  17. 17.
    Poizat, P., Salaün, G.: Checking the Realizability of BPMN 2.0 Choreographies. In: Proc of SAC 2012 (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Huu Nghia Nguyen
    • 1
  • Pascal Poizat
    • 1
    • 2
  • Fatiha Zaïdi
    • 1
  1. 1.LRI; Univ. Paris-Sud, CNRSOrsayFrance
  2. 2.Univ. Évry Val d’EssonneEvryFrance

Personalised recommendations