Abstract
Web services are a very appropriate communication mechanism to perform distributed business processes among several organisations. These processes should be reliable, because a failure in them can cause high economic losses. To increase their reliability at design time, we have developed VERBUS, a framework for the formal verification of business processes. VERBUS can automatically translate business process definitions to specifications verifiable in several available tools. It is based on a modular and extensible architecture: new process definition languages and verification tools can be added easily to the framework. The prototype of VERBUS presented in this work can verify BPEL4WS process specifications, by translating them to Promela. The Promela specifications are verified with the well known model checker Spin. In this paper we describe the general architecture of VERBUS and how BPEL4WS specifications are translated and verified. The explanation is completed by describing what types of properties can be verified and providing an overview of the implementation.
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
Jae-yoon Jung, W.H., Kang, S.H.: Business Process Choreography for B2B Collaboration. IEEE Internet Computing 8, 37–45 (2004)
Aissi, S., Malu, P., Srinivasan, K.: E-business process modeling: the next big step. IEEE Computer 35, 55–62 (2002)
Andrews, T., Curbera, F., Dholakia, H., et al.: Business Process Execution Language for Web Services. Version 1.1 Specification (2003), Available at http://www-106.ibm.com/developerworks/webservices/library/ws-bpel
Arkin, A.: Business Process Modelling Language. Business Process Management Initiative (2002)
ebXML Business Process Team: ebXML Business Process Specification Schema. Version 1.01 (2001), Available at http://www.ebxml.org/specs/ebBPSS.pdf
Aalst, W.M.P.: Woflan: A petri-net-based workflow analyzer. Systems Analysis – Modelling – Simulation 35, 345–357 (1999)
Eshuis, R.: Semantics and Verification of UML Activity Diagrams for Workflow Modelling. PhD thesis, University of Twente (2002)
Narayanan, S., McIlraith, S.: Simulation, Verification and Automated Composition of Web Services. In: Proceedings of the Eleventh International World Wide Web Conference, Budapest, Hungary (2002)
Holzmann, G.J.: The Spin model checker. Addison-Wesley, Reading (2003)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Fisteus, J.A., Marin, A., Delgado, C.: VERBUS: A Formal Model for Business Process Verification. In: Proceedings of the 2004 IRMA International Conference, New Orleans, USA (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fisteus, J.A., Fernández, L.S., Kloos, C.D. (2004). Formal Verification of BPEL4WS Business Collaborations. In: Bauknecht, K., Bichler, M., Pröll, B. (eds) E-Commerce and Web Technologies. EC-Web 2004. Lecture Notes in Computer Science, vol 3182. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30077-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-30077-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22917-9
Online ISBN: 978-3-540-30077-9
eBook Packages: Springer Book Archive