Abstract
We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.
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.
References
Curbera, F., Goland, Y., Klein, J., Leymann, F., Roller, D., Thatte, S., Weerawarana, S.: Business Process Execution Language forWeb Services, Version 1.1. Technical report, BEA Systems, International Business Machines Corporation, Microsoft Corporation (2003)
Leymann, F.: WSFL- Web Services Flow Language. IBM Software Group, Whitepaper (2001), http://ibm.com/webservices/pdf/WSFL.pdf
Thatte, S.: XLANG–Web Services for Business Process Design. Microsoft Corporation, Initial Public Draft. (2001), http://www.gotdotnet.com/team/xmlwsspecs/xlang-c
Fisteus, J.A., Fernández, L.S., Kloos, C.D.: Formal Verification of BPEL4WS Business Collaborations. In: Bauknecht, K., Bichler, M., Pröll, B. (eds.) EC-Web 2004. LNCS, vol. 3182, pp. 76–85. Springer, Heidelberg (2004)
Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: WWW 2004: Proceedings of the 13th international conference on World Wide Web, pp. 621–630. ACM Press, New York (2004)
Ferrara, A.: Web services: a process algebra approach. In: ICSOC, pp. 242–251. ACM, New York (2004)
Fahland, D., Reisig, W.: ASM-based semantics for BPEL: The negative Control Flow. In D. Beauquier, E.B., Slissenko, A., eds.: Proc. 12th International Workshop on Abstract State Machines, Paris, March 2005. Lecture Notes in Computer Science, Springer-Verlag (to appear, 2005)
Farahbod, R., Glässer, 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)
van der Aalst, W.M.P.: The Application of Petri Nets to Workflow Management. Journal of Circuits, Systems and Computers 8, 21–66 (1998)
Martens, A.: Verteilte Gesch∙aftsprozesse –Modellierung und Verifikation mit Hilfe von Web Services. Dissertation, WiKu-Verlag Stuttgart (2004)
Schmidt, K.: Controlability of Business Processes. Technical Report 180, Humboldt-Universität zu Berlin (2004)
Schmidt, K.: LoLA – A Low Level Analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 465. Springer, Heidelberg (2000)
Ratzer, A.V., Wells, L., Lassen, H.M., Laursen, M., Qvortrup, J.F., Stissing, M.S., Westergaard, M., Christensen, S., Jensen, K.: CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 450–462. Springer, Heidelberg (2003)
Starke, P.H., Roch, S.: Ina et al. In: Mortensen, K.H. (ed.) Tool Demonstrations 21st International Conference on Application and Theory of Petri Nets. Department of Computer Science, pp. 51–56. University of Aarhus (2000)
Leymann, F., Roller, D.: Production Workflow –Concepts and Techniques. Prentice-Hall, Englewood Cliffs (1999)
Stahl, C.: Transformation von BPEL4WS in Petrinetze. Diplomarbeit, Humboldt- Universität zu Berlin (2004)
Stahl, C.: A Petri Net Semantics for BPEL. Technical report, Humboldt- Universität zu Berlin (to appear, June 2005)
Cabrera, G., Copeland, J., Cox, B., Freund, T., Klein, J., Storey, T., Thatte, S.: Web Services Transaction. Vorschlag zur Standardisierung, Version 1.0 (2002), http://ibm.com/developerworks/webservices/library/ws-transpec/
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Schmidt, K., Stahl, C.: A Petri net semantic for BPEL4WS - validation and application. In: Kindler, E. (ed.) Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN–2004), Universität Paderborn, pp. 1–6 (2004)
Hinz, S.: Implementation einer Petrinetz-Semantik für BPEL4WS. Diplomarbeit, Humboldt-Universität zu Berlin (2005)
Billington, J., et al.: The Petri Net Markup Language: Concepts, Technology, and Tools (2003)
Schmidt, K.: How to calculate symmetries of petri nets. Acta Informatica, 545–590 (2000)
Schmidt, K.: Stubborn set for standard properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46–65. Springer, Heidelberg (1999)
Schmidt, K.: Automated Generation of a Progress Measure for the Sweep-Line Method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 192–204. Springer, Heidelberg (2004)
Heidinger, T.: Statische Analyse von BPEL4WS-Prozessmodellen. Studienarbeit, Humboldt-Universität zu Berlin (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hinz, S., Schmidt, K., Stahl, C. (2005). Transforming BPEL to Petri Nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds) Business Process Management. BPM 2005. Lecture Notes in Computer Science, vol 3649. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11538394_15
Download citation
DOI: https://doi.org/10.1007/11538394_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28238-9
Online ISBN: 978-3-540-31929-0
eBook Packages: Computer ScienceComputer Science (R0)