Abstract
In this paper we propose an approach to derive the formal semantics of WS-BPEL processes compositionally using Reo and constraint automata. We map each WS-BPEL process into a Reo circuit and then construct the corresponding constraint automaton which shows the behavior of the process. The constraint automaton can be used for analyzing the process behavior. Our work covers the core part of the WS-BPEL language including basic and structured activities, correlation sets, variables, and links.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Jordan, D., Evdemon, J.: Web services business process execution language version 2.0. Technical report, OASIS (2006)
Fahland, D.: Complete abstract operational semantics for the web service business process execution language. Technical Report 190, Humboldt University, Berlin (2005)
Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri Nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 220–235. Springer, Heidelberg (2005)
Ferrara, A.: Web services: a process algebra approach. In: Proceedings of 2nd International Conference on Service Oriented Computing, pp. 242–251. ACM Press, New York (2004)
Farahbod, R., Glasser, U., Vajihollahi, M.: Specification and validation of the business process execution language for web services. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 78–94. Springer, Heidelberg (2004)
Diakov, N., Arbab, F.: Compositional construction of web services using Reo. In: WSMAI, pp. 49–58 (2004)
Lemniotes, T., Papadopoulos, G.A., Arbab, F.: Coordinating web services using channel based communication. In: 28th Annual International Computer Software and Applications Conference (COMPSAC 2004), pp. 486–491 (2004)
Meng, S., Arbab, F.: Web services choreography and orchestration in Reo and constraint automata. In: Proceedings of 22nd Annual ACM Symposium on Applied Computing(SAC 2007) (2007)
Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), 329–366 (2004)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Science of Computer Programming 61(2), 75–113 (2006)
Arbab, F., Rutten, J.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 35–56. Springer, Heidelberg (2003)
Mahdikhani, F.: BPEL to Reo tool (2007), http://ece.ut.ac.ir/msirjani/B2ReoTool/B2R.jar
Klüppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. In: FOCLASA 2006 (2006)
Pourvatan, B., Rouhy, N.: An alternative algorithm for constraint automata product. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 409–419. Springer, Heidelberg (2007)
Clarke, D.: A basic logic for reasoning about connector reconfiguration. Fundamenta Informaticae (accepted, 2007)
Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: 13th Int. Conf. World Wide Web (WWW 2004), pp. 621–630. ACM Press, New York (2004)
Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2003)
Borger, E., Stark, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Fahland, D., Reisig, W.: ASM-based semantics for BPEL: The negative control flow. In: Proceedings of 12th International Workshop on Abstract State Machines, Paris, pp. 78–94. Springer, Heidelberg (2005)
Schmidt, K., Stahl, C.: A Petri Net semantic for BPEL4WS - validation and application. In: Proceedings of 11th Workshop on Algorithms and Tools for Petri Nets (2004)
Ouyang, C., van der Aalst, W., Breutel, S., Dumas, M., ter Hofstede, A., Verbeek, H.: Formal semantics and analysis of control flow in WS-BPEL. Technical Report BPM-05-15, BPM Center (2005)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts i and ii. Information and Computation 100(1), 1–77 (1992)
Koshkina, M.: Verification of business processes for web services. Master thesis, York University (2003)
Brogi, A., Popescu, R.: From BPEL processes to YAWL workflows. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 107–122. Springer, Heidelberg (2006)
Diakov, N., Arbab, F.: Software adaptation in integrated tool frameworks for composite services. In: Proceedings of The Third International Workshop on Coordination and Adaptation of Software Entities(WCAT 2006), Nantes, France, pp. 9–14 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tasharofi, S., Vakilian, M., Zilouchian Moghaddam, R., Sirjani, M. (2008). Modeling Web Service Interactions Using the Coordination Language Reo. In: Dumas, M., Heckel, R. (eds) Web Services and Formal Methods. WS-FM 2007. Lecture Notes in Computer Science, vol 4937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79230-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-79230-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79229-1
Online ISBN: 978-3-540-79230-7
eBook Packages: Computer ScienceComputer Science (R0)