Stepwise Development of Formal Models for Web Services Compositions: Modelling and Property Verification

  • Idir Ait-Sadoune
  • Yamine Ait-Ameur
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8220)


The ability to compose existing services to provide more complex features is one of the main benefits of Service Oriented Architecture (SOA). This services composition process, especially Web services, is generally defined by a choreography or an orchestration of atomic services. These compositions are seen as a state transition system describing the communication protocol between the participating services. The services description languages, expressing these compositions, suffer from the lack of formal semantics and the ambiguities in the definition of their constructors in the standards defining these languages. The tools associated with these languages do not offer the possibility to formally verify and validate the behaviour and the properties of the obtained composed service.

Our work focuses on the formal modelling and verification of the web services composition described by the BPEL standard using the Event-B method. The proposed approach formalizes the static and the dynamic parts of BPEL, and uses the refinement to structure a BPEL development. The theorem-proving technique is set-up to verify the properties. A one-to-one link is guaranteed between BPEL elements and their Event-B formalization. This correspondence provides assistance for developers to improve the quality of the obtained BPEL process. This approach is implemented in the BPEL2B tool.


Formal modelling Verification Refinement and proof Event-B Composition operators Services composition 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    van der Aalst, W.M.P., Mooij, A.J., Stahl, C., Wolf, K.: Service Interaction: Patterns, Formalization, and Analysis. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 42–88. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)CrossRefzbMATHGoogle Scholar
  3. 3.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)Google Scholar
  4. 4.
    Abrial, J.R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundamenta Informaticae 77, 1–28 (2007)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Ait-Ameur, Y., Baron, M., Kamel, N., Mota, J.M.: Encoding a process algebra using the Event B method. International Journal on Software Tools for Technology Transfer (STTT) 11(3), 239–253 (2009)CrossRefGoogle Scholar
  6. 6.
    Ait-Sadoune, I., Ait-Ameur, Y.: Animating Event B Models by Formal Data Models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 37–55. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Ait-Sadoune, I., Ait-Ameur, Y.: From BPEL to Event-B. In: International Workshop on Integration of Model-based Methods and Tools at IFM Conference (2009)Google Scholar
  8. 8.
    Ait-Sadoune, I., Ait-Ameur, Y.: A Proof Based Approach for Modelling and Verifying Web Services Compositions. In: 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 1–10. IEEE Computer Society, Potsdam (2009)CrossRefGoogle Scholar
  9. 9.
    Aït Sadoune, I., Aït Ameur, Y.: A proof based approach for formal verification of transactional BPEL web services. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 405–406. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  10. 10.
    Ait-Sadoune, I., Ait-Ameur, Y.: Stepwise Design of BPEL Web Services Compositions, An Event B Refinement Based Approach. In: Lee, R., Ormandjieva, O., Abran, A., Constantinides, C. (eds.) SERA 2010. SCI, vol. 296, pp. 51–68. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    ter Beek, M.H., Bucchiarone, A., Gnesi, S.: Formal methods for service composition. Annals of Mathematics, Computing and Teleinformatics 1(5), 1–10 (2007)Google Scholar
  12. 12.
    Börger, E., Thalheim, B.: Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 24–38. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  13. 13.
    Brodt, R.: BPEL Designer Project (April 2012),
  14. 14.
    Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1977)Google Scholar
  15. 15.
    Fahland, D., Reisig, W.: ASM-based semantics for BPEL: The negative Control Flow. In: 12th International Workshop on Abstract State Machines, pp. 131–151 (2005)Google Scholar
  16. 16.
    Farahbod, R., Glässer, U., Vajihollahi, M.: An Abstract Machine Architecture for Web Service Based Business Process Management. In: Bussler, C.J., Haller, A. (eds.) BPM 2005 Workshops. LNCS, vol. 3812, pp. 144–157. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Foster, H.: A Rigorous Approach to Engineering Web Service Compositions. Ph.D. thesis, University of London (2006)Google Scholar
  18. 18.
    Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based Verification of Web Service Compositions. In: 18th IEEE International Conference on Automated Software Engineering (ASE 2003), pp. 152–163 (2003)Google Scholar
  19. 19.
    Foster, H., Uchitel, S., Magee, J., Kramer, J.: LTSA-WS: A Tool for Model-Based Verification of Web Service Compositions and Choreography. In: 28th International Conference on Software Engineering, pp. 771–774 (2006)Google Scholar
  20. 20.
    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
  21. 21.
    Hoare, C.A.R.: An axiomatic basis for computer programming. ACM 12, 576–580 (1969)CrossRefzbMATHGoogle Scholar
  22. 22.
    Lohmann, N.: A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 77–91. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Marconi, A.: Automated Process-level Composition of Web Services: from Requirements Specification to Process Run. Ph.D. thesis, University of Trento, Italy (2008)Google Scholar
  24. 24.
    Marconi, A., Pistore, M.: Synthesis and Composition of Web Services. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 89–157. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  25. 25.
    Nakajima, S.: Lightweight formal analysis of Web service flows. Progress in Informatics, 57–76 (2005)Google Scholar
  26. 26.
    Nakajima, S.: Model-Checking Behavioral Specification of BPEL Applications. Electronic Notes in Theoretical Computer Science 151, 89–105 (2006)CrossRefGoogle Scholar
  27. 27.
    OASIS: Web Services Business Process Execution Language Version 2.0 (April 2007),
  28. 28.
    OMG: Business Process Model and Notation (BPMN) Version 2.0 (June 2010),
  29. 29.
    Rodin: User Manual of the RODIN Platform (October 2007),
  30. 30.
    Salaün, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: IEEE International Conference on Web Services (ICWS 2004), pp. 43–51 (2004)Google Scholar
  31. 31.
    Salaün, G., Ferrara, A., Chirichiello, A.: Negotiation Among Web Services Using LOTOS/CADP. In: Zhang, L.-J., Jeckle, M. (eds.) ECOWS 2004. LNCS, vol. 3250, pp. 198–212. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  32. 32.
    Verbeek, H., van der Aalst, W.M.P: Analyzing BPEL processes using Petri nets. In: 2nd International Workshop on Applications of Petri Nets to Coordination, Workflow and Business Process Management (2005)Google Scholar
  33. 33.
    W3C: OWL-S: Semantic Markup for Web Services (November 2004),
  34. 34.
    W3C: Web Service Definition Language (WSDL 1.1) (February 2004),
  35. 35.
    W3C: Web Services Choreography Description Language Version 1.0 (November 2005),
  36. 36.
    WMC-WS: Process Definition Interface - XML Process Definition Language (October 2008),

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Idir Ait-Sadoune
    • 1
  • Yamine Ait-Ameur
    • 2
  1. 1.E3S - SupelecGif-Sur-YvetteFrance
  2. 2.IRIT - ENSEEIHTToulouseFrance

Personalised recommendations