Abstract
We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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
Alves, A., et al.: Web Services Business Process Execution Language Version 2.0. Technical report, OASIS (2007)
Andrews, T., et al.: Business Process Execution Language for Web Services, Version 1.1. Technical report, BEA, IBM, Microsoft (2003)
Breugel, F., Koshkina, M.: Models and verification of BPEL (2006), http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf
Aalst, W.M.P., Hee, K.M.v.: Workflow Management: Models, Methods, and Systems. MIT Press, Cambridge (2002)
Reisig, W.: Petri Nets. Springer, Heidelberg (1985)
Aalst, W.M.P.: The application of Petri nets to workflow management. Journal of Circuits, Systems and Computers 8(1), 21–66 (1998)
Martens, A.: Analyzing Web service based business processes. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 19–33. Springer, Heidelberg (2005)
Schmidt, K.: Controllability of open workflow nets. In: Desel, J., Frank, U. (eds.) Enterprise Modelling and Information Systems Architectures, Proceedings of the Workshop in Klagenfurt, October 24-25, 2005. Lecture Notes in Informatics (LNI), vol. 75, pp. 236–249. GI (2005)
Girault, C., Valk, R. (eds.): Petri Nets for System Engineering – A Guide to Modeling Verification and Applications. Springer, Heidelberg (2002)
Stahl, C.: A Petri net semantics for BPEL. Techn. Report 188, Humboldt-Universität zu Berlin (2005)
Lohmann, N.: A feature-complete Petri net semantics for WS-BPEL 2.0 and its compiler BPEL2oWFN. Techn. Report 212, Humboldt-Universität zu Berlin, Berlin, Germany (2007)
Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting BPEL processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 17–32. Springer, Heidelberg (2006)
Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting WS-BPEL processes using flexible model generation. Data Knowl. Eng. 64(1), 38–54 (2008)
Reisig, W.: Petri nets and algebraic specifications. Theor. Comput. Sci. 80(1), 1–34 (1991)
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)
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)
Moser, S., Martens, A., Görlach, K., Amme, W., Godlinski, A.: Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis. In: IEEE International Conference on Services Computing (SCC 2007), pp. 98–105. IEEE Computer Society Press, Los Alamitos (2007)
Lohmann, N., Massuthe, P., Wolf, K.: Operating guidelines for finite-state services. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 321–341. Springer, Heidelberg (2007)
Lohmann, N., Kopp, O., Leymann, F., Reisig, W.: Analyzing BPEL4Chor: Verification and participant synthesis. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 46–60. Springer, Heidelberg (2007)
Ouyang, C., Verbeek, E., Aalst, W.M.P.: v.d., Breutel, S., Dumas, M., Hofstede, A.H.M.t.: WofBPEL: A tool for automated analysis of BPEL processes. In: Benatallah, B., Casati, F., Traverso, P. (eds.) ICSOC 2005. LNCS, vol. 3826, pp. 484–489. Springer, Heidelberg (2005)
Ouyang, C., Aalst, W.M.P., Breutel, S., Hofstede, A.H.M.t.: Formal semantics and analysis of control flow in WS-BPEL. Sci. Comput. Program 67(2-3), 162–198 (2007)
Lohmann, N., Verbeek, H., Ouyang, C., Stahl, C., Aalst, W.M.P.v.d.: Comparing and evaluating Petri net semantics for BPEL. Computer Science Report 07/23, Eindhoven University of Technology, Eindhoven, The Netherlands (2007)
Wilkes, L.: The Web services protocol stack. Technical report, CBDI Web Services Roadmap (2005), http://roadmap.cbdiforum.com/reports/protocols
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lohmann, N. (2008). A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. 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_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-79230-7_6
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)