Web services are increasingly becoming a major part of our daily lives. Many web services composition languages have been developed to describe the way a group of distributed web services interact with each other. In this matter, BPEL is one of the highly used composition languages. In this work, we are interested in verifying BPEL processes. Several works have addressed this issue before, but to our knowledge, a formalism that captures both the behavioral and the timing aspects of all the constructs of BPEL 2.0 does not exist. In this paper, we introduce a verification framework for timed BPEL models. We show how the relative and the absolute time of BPEL can be treated. We also give examples of temporal and timed properties that are supported in our framework. The verification is based on a transformation of all the BPEL constructs to the process algebra language, FIACRE.


Web services BPEL formal methods verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ait-Sadoune, I., Ait-Ameur, Y.: A proof based approach for modelling and verifying web services compositions. In: Proceedings of the 2009 14th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2009, pp. 1–10. IEEE Computer Society, Washington, DC, USA (2009)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality (1996)Google Scholar
  3. 3.
    Alves, A., Arkin, A., Askary, S., Bloch, B., Curbera, F., Goland, Y., Kartha, N., Sterling, König, D., Mehta, V., Thatte, S., van der Rijn, D., Yendluri, P., Yiu, A.: Web Services Business Process Execution Language Version 2.0. OASIS (May 2006)Google Scholar
  4. 4.
    Berglund, A., Boag, S., Chamberlin, D., Fernández, M.F., Kay, M., Robie, J., Siméon, J.: XML Path Language (XPath) 2.0 (W3C Recommendation) (January 2007)Google Scholar
  5. 5.
    Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research 42 (2004)Google Scholar
  6. 6.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM, New York (1999)Google Scholar
  7. 7.
    Farail, P., Gaufillet, P., Peres, F., Bodeveix, J.-P., Filali, M., Berthomieu, B., Rodrigo, S., Vernadat, F., Garavel, H., Lang, F.: FIACRE: an intermediate language for model verification in the TOPCASED environment. In: European Congress on Embedded Real-Time Software (ERTS) (2008)Google Scholar
  8. 8.
    Ferrara, A.: Web services: a process algebra approach. In: ICSOC 2004: Proceedings of the 2nd International Conference on Service Oriented Computing, pp. 242–251. ACM Press, New York (2004)Google Scholar
  9. 9.
    Henzinger, T.A., Manna, Z., Pnueli, A.: Timed Transition Systems. In: REX Workshop, pp. 226–251 (1991)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)Google Scholar
  12. 12.
    Kazhamiakin, R., Pandya, P., Pistore, M.: Representation, verification, and computation of timed properties in Web Service Compositions. In: Proceedings of the IEEE International Conference on Web Services, pp. 497–504. IEEE Computer Society, Washington, DC, USA (2006)Google Scholar
  13. 13.
    Lanz, A., Weber, B., Reichert, M.: Workflow time patterns for process-aware information systems. In: Aalst, W., Mylopoulos, J., Sadeh, N.M., Shaw, M.J., Szyperski, C., Bider, I., Halpin, T., Krogstie, J., Nurcan, S., Proper, E., Schmidt, R., Ukor, R. (eds.) A Concurrent Pascal Compiler for Minicomputers. LNBIP, vol. 50, pp. 94–107. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Lohmann, N.: A feature-complete Petri net semantics for WS-BPEL 2.0. In: van Hee, K., Reisig, W., Wolf, K. (eds.) Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS 2007), pp. 21–35. University of Podlasie (2007)Google Scholar
  15. 15.
    Mateescu, R., Rampacek, S.: Formal Modeling and Discrete-Time Analysis of BPEL Web Services. International Journal of Simulation and Process Modeling (2008)Google Scholar
  16. 16.
    Milner, R.: A Calculus of Communicating Systems. Springer-Verlag New York, Inc., Secaucus (1982)Google Scholar
  17. 17.
    Moreau, J.J., Chinnici, R., Ryman, A., Weerawarana, S.: Web Services Description Language (WSDL) version 2.0 part 1: Core language. Candidate recommendation, W3C (March 2006)Google Scholar
  18. 18.
    Nakajima, S.: Model-Checking Behavioral Specification of BPEL Applications. Electron. Notes Theor. Comput. Sci. 151, 89–105 (2006)CrossRefGoogle Scholar
  19. 19.
    Pu, G., Zhao, X., Wang, S., Qiu, Z.: Towards the semantics and verification of BPEL4WS. Electron. Notes Theor. Comput. Sci. 151, 33–52 (2006)CrossRefGoogle Scholar
  20. 20.
    Qian, Y., Xu, Y., Wang, Z., Pu, G., Zhu, H., Cai, C.: Tool Support for BPEL Verification in ActiveBPEL Engine. In: 18th Australian Software Engineering Conference ASWEC 2007, pp. 90–100 (April 2007)Google Scholar
  21. 21.
    Salaun, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: IEEE International Conference on Web Services, p. 43 (2004)Google Scholar
  22. 22.
    Song, W., Ma, X., Ye, C., Dou, W., Lü, J.: Timed modeling and verification of BPEL processes using time petri nets. In: Proceedings of the 2009 Ninth International Conference on Quality Software, QSIC 2009, pp. 92–97. IEEE Computer Society, Washington, DC, USA (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Elie Fares
    • 1
  • Jean-Paul Bodeveix
    • 1
  • Mamoun Filali
    • 1
  1. 1.IRIT, Université de ToulouseFrance

Personalised recommendations