Abstract
A service choreography is a model of interactions in which a set of services engage to achieve a goal, seen from the perspective of an ideal observer that records all messages exchanged between these services. Choreographies have been put forward as a starting point for building service-oriented systems since they provide a global picture of the system’s behavior. In previous work we presented a language for service choreography modeling targeting the early phases of the development lifecycle. This paper provides an execution semantics for this language in terms of a mapping to π-calculus. This formal semantics provides a basis for analyzing choreographies. The paper reports on experiences using the semantics to detect unreachable interactions.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Repeated Interaction
- Service Interaction
- Stop Condition
- Business Process Execution Language
- Execution Semantic
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.
References
Andrews, T., Curbera, F., Dholakia, H., Goland, Y., Klein, J., Leymann, F., Liu, K., Roller, D., Smith, D., Thatte, S., Trickovic, I., Weerawarana, S.: Business Process Execution Language for Web Services, version 1.1 (May 2003), http://www-106.ibm.com/developerworks/webservices/library/ws-bpel
Arkin, A., et al.: Web Service Choreography Interface (WSCI) 1.0 (2002), www.w3.org/TR/wsci/
Brogi, A., Canal, C., Pimentel, E., Vallecillo, A.: Formalizing Web Service Choreographies. In: Proceedings of 1st International Workshop on Web Services and Formal Methods, Pisa, Italy, February 2004. Elsevier, Amsterdam (2004)
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)
Clark, J., Casanave, C., Kanaskie, K., Harvey, B., Smith, N., Yunker, J., Riemer, K. (eds.): ebXML Business Process Specification Schema Version 1.01, UN/CEFACT and OASIS Specification (May 2001), http://www.ebxml.org/specs/ebBPSS.pdf
Hull, R., Su, J.: Tools for composite web services: a short overview. SIGMOD Record 34(2), 86–95 (2005)
Kavantzas, N., Burdett, D., Ritzinger, G., Lafon, Y.: Web Services Choreography Description Language Version 1.0, W3C Candidate Recommendation (November 2005), http://www.w3.org/TR/ws-cdl-10
Decker, G., Puhlmann, F., Weske, M.: Formalizing Service Interactions. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 414–419. Springer, Heidelberg (2006)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100, 1–40 (1992)
Puhlmann, F., Weske, M.: Using the π-Calculus for Formalizing Workflow Patterns. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 153–168. Springer, Heidelberg (2005)
Sangiorgi, D.: A theory of bisimulation for the π-calculus. Acta Informatica 16(33), 69–97 (1996)
Victor, B., Moller, F., Dam, M., Eriksson, L.H.: The Mobility Workbench, Uppsala University (2006), http://www.it.uu.se/research/group/mobility/mwb
Yang, H., Zhao, X., Qiu, Z., Pu, G., Wang, S.: A Formal Model for Web Service Choreography Description Language (WS-CDL), Preprint, School of Mathematical Sciences, Peking University (January 2006), www.math.pku.edu.cn:8000/var/preprint/7021.pdf
Zaha, J.M., Barros, A., Dumas, M., ter Hofstede, A.: Lets Dance: A Language for Service Behavior Modeling. Preprint # 4468, Faculty of IT, Queensland University of Technology (February 2006), http://eprints.qut.edu.au/archive/00004468
Zaha, J.M., Dumas, M., ter Hofstede, A., Barros, A., Decker, G.: Service Interaction Modeling: Bridging Global and Local Views. In: Proceedings of the 10th International EDOC Conference, Hong Kong (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Decker, G., Zaha, J.M., Dumas, M. (2006). Execution Semantics for Service Choreographies. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds) Web Services and Formal Methods. WS-FM 2006. Lecture Notes in Computer Science, vol 4184. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11841197_11
Download citation
DOI: https://doi.org/10.1007/11841197_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-38862-3
Online ISBN: 978-3-540-38865-4
eBook Packages: Computer ScienceComputer Science (R0)