Abstract
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.
This work is supported by the PIMI project (ANR-2010-VERS-0014-03) of the French National Agency for Research.
Chapter PDF
Similar content being viewed by others
Keywords
References
Poizat, P.: Formal Model-Based Approaches for the Development of Composite Systems. Habilitation thesis, Université Paris Sud (November 2011), http://www.lri.fr/~poizat/documents/hdr.pdf
Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the Theoretical Foundation of Choreography. In: Proc. of WWW 2007 (2007)
Basu, S., Bultan, T.: Choreography Conformance via Synchronizability. In: Proc. of WWW 2011 (2011)
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)
Li, J., Zhu, H., Pu, G.: Conformance Validation between Choreography and Orchestration. In: Proc. of TASE 2007 (2007)
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)
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)
Van Glabbeek, R., Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3) (1996)
Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138(2), 353–389 (1995)
Lin, H.: Symbolic Transition Graph with Assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)
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)
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)
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)
Nguyen, H.N., Poizat, P., Zaïdi, F.: A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. Long version, in P. Poizat Webpage
Decker, G., Kopp, O., Barros, A.P.: An Introduction to Service Choreographies. Information Technology 50(2), 122–127 (2008)
Kopp, O., Leymann, F.: Do We Need Internal Behavior in Choreography Models? In: Proc. of ZEUS 2009 (2009)
Poizat, P., Salaün, G.: Checking the Realizability of BPMN 2.0 Choreographies. In: Proc of SAC 2012 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, H.N., Poizat, P., Zaïdi, F. (2012). A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds) Service-Oriented Computing. ICSOC 2012. Lecture Notes in Computer Science, vol 7636. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34321-6_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-34321-6_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34320-9
Online ISBN: 978-3-642-34321-6
eBook Packages: Computer ScienceComputer Science (R0)