Abstract
Web services promise the interoperability of various applications running on heterogeneous platforms over the Internet, and are gaining more and more attention. Web service composition refers to the process of combining Web services to provide value-added services, which has received much interest in supporting enterprize application integration. Industry standards for Web Service composition, such as WSBPEL, provide the notation and additional control mechanisms for the execution of business processes in Web service collaborations. However, these standards do not provide support for checking interesting properties related to Web Service and process behavior. In an attempt to fill this gap, we describe a formalization of WSBPEL business processes, that adds communications semantics to the specifications of interacting Web services, and uses a formal logic to model their dynamic behavior, which enables their formal analysis and the inference of relevant properties of the systems being built.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Andrews T, Curbera F, Dholakia H, Goland Y, Klein J, Leymann F, Liu K, Roller D, Smith D, Thatte S, Trickovic I, Weerawarana S (2003) Business process execution language for Web Services, Version 1.1. Standards proposal by BEA Systems, International Business Machines Corporation, and Microsoft Corporation
Arkin A, Askary S, Bloch B, Curbera F (2004) Web services business process execution language version 2.0. Technical report, OASIS
Brogi A, Canal C, Pimentel E, Vallecillo A (2004) Formalizing web service choreographies. Electr Notes Theor Comput Sci 105:73–94
Casati F, Shan M-C (2001) Dynamic and adaptive composition of e-services. Inf Syst 26(3):143–163
Fahland D, Reisig W (2005) ASM-based semantics for BPEL: the negative control flow. In: Beauquier D, Börger E, Slissenko A (eds) Proceedings of 12th international workshop on abstract state machines. Paris, France, pp 131–151
Ferrara A (2004) Web services: a process algebra approach. In: Proceedings of the 2nd international conference on service oriented computing. ACM Press, New York, pp 242–251
Fisteus J, Fernández L, Kloos C (2004) Formal verification of BPEL4WS business collaborations. In: Bauknecht K, Bichler M, Proll B (eds) Proceedings of the 5th international conference on electronic commerce and Web technologies (EC-Web ’04). Lecture Notes in Computer Science, vol 3182, Zaragoza, Spain. Springer, Berlin, pp 79–94
Foster H, Kramer J, Magee J, Uchitel S (2003) Model-based verification of web service compositions. In: 18th IEEE international conference on automated software engineering (ASE)
Fu X (2004) Formal specification and verification of asynchronously communicating Web services. Phd Thesis, University of California, Santa Barbara
Fu X, Bultan T, Su J (2004) Analysis of interacting bpel web services. In: WWW ’04: Proceedings of the 13th international conference on World Wide Web, ACM Press, New York, pp 621–630
Gustavo Alonso HKVM (2004) Fabio Casati. Web services: concepts, architectures and applications. Springer, Berlin
Koshkina M, van Breugel F (2004) Modelling and verifying web service orchestration by means of the concurrency workbench. SIGSOFT Softw Eng Notes 29(5):1–10
Kowalski R, Sergot MJ (1986) A logic-based calculus of events. New Generation Comput 4(1):67–95
Kozlenkov A, Zisman A (2004) Discovering, recording, and handling inconsistencies in software specifications. Int J Comput Inf Sci 5(2):89–108
Magee J, Kramer J (1999) Concurrency: state models & Java programs. Wiley, New York
Mahbub K, Spanoudakis G (2004) A framework for requirents monitoring of service based systems. In: ICSOC ’04: Proceedings of the 2nd international conference on Service oriented computing, ACM Press, New York, pp 84–93
Martens A (2005) Analyzing Web service based business processes. In: Cerioli M (ed) Proceedings of the 8th international conference on fundamental approaches to software engineering (FASE 2005). Lecture Notes in Computer Science, vol 3442. Springer, Berlin, pp 19–33
Nakajima S (2002) Verification of web service flows with model-checking techniques. In: Proceedings of the first international symposium on Cyber Worlds (CW 2002). IEEE Computer Society, Washington, pp 378–385
Narayanan S, McIlraith SA (2002) Simulation, verification and automated composition of web services. In: WWW ’02: Proceedings of the 11th international conference on World Wide Web. ACM Press, , New York, pp 77–88
Ouyang C, Aalst W, Breutel S, Dumas M, Verbeek H (2005) Formal semantics and analysis of control flow in WS-BPEL. BPM Center Report BPM-05-15, BPMcenter.org
Pistore M, Roveri M, Busetta P (2004) Requirements-driven verification of web services. Electr Notes Theor Comput Sci 105:95–108
Pu G, Zhao X, Wang S, Qiu Z (2006) Towards the semantics and verification of bpel4ws. Electr Notes Theor Comput Sci 151(2):33–52
Rouached M, Gaaloul W, van der Aalst WMP, Bhiri S, Godart C (2006) Web service mining and verification of properties: an approach based on event calculus. In: Proceedings 14th international conference on cooperative information Systems (CoopIS 2006)
Rouached M, Godart C (2007) A dynamic query based discovery for Web services composition. http://www.loria.fr/~rouached/CWSDiscovery.pdf
Rouached M, Godart C (2007) Requirements-driven verification of wsbpel processes. In: Proceedings of the IEEE international conference on Web services (ICWS’07), Salt Lake City
Spanoudakis G, Zisman A, Kozlenkov A (2005) A service discovery framework for service centric systems. In: SCC ’05: Proceedings of the 2005 IEEE international conference on services computing. IEEE Computer Society, Washington, DC, pp 251–259
Stahl C (2004) Transformation von BPEL4WS in Petrinetze (In German). Master’s Thesis, Humboldt University, Berlin
Stratulat S (2001) A general framework to build contextual cover set induction provers. J Symb Comput 32(4):403–445
van Breugel F, Koshkina M (2006) Models and verification of bpel. Available at http://www.cse.yorku.ca/franck/research/drafts/tutorial.pdf
Yang Y, Tan Q, Xiao Y (2005) Verifying web services composition based on hierarchical colored petri nets. In: IHIS ’05: Proceedings of the first international workshop on Interoperability of heterogeneous information systems. ACM Press, New York, pp 47–54
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Rouached, M., Fdhila, W. & Godart, C. A semantical framework to engineering WSBPEL processes. Inf Syst E-Bus Manage 7, 223–250 (2009). https://doi.org/10.1007/s10257-008-0081-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10257-008-0081-5