Authors: Niels Lohmann, Eric Verbeek, Chun Ouyang, Christian Stahl
Addresses: Institut fur Informatik, Universitat Rostock, 18051 Rostock, Germany. ' Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The Netherlands. ' Faculty of Science and Information Technology, Queensland University of Technology, GPO Box 2434, Brisbane QLD 4001, Australia. ' Institut fur Informatik, Humboldt-Universitat zu Berlin, Unter den Linden 6, 10099 Berlin, Germany; Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, The Netherlands
Abstract: We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.
Keywords: business process modelling; business process execution language; Petri nets; semantics; formal methods; verification; BPEL; web services; WS-BPEL.
International Journal of Business Process Integration and Management, 2009 Vol.4 No.1, pp.60 - 73
Published online: 12 Jul 2009 *Full-text access for editors Access for subscribers Purchase this article Comment on this article