A Generic Approach for the Verification of Static and Dynamic Behavioral Properties of SCDL/WS-BPEL Service-Component Architectures

  • Taoufik Sakka RouisEmail author
  • Mohamed Tahar Bhiri
  • Mourad Kmimech
  • Layth Sliman
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 931)


Web systems verification is a crucial activity throughout the systems development life cycle, especially in the phase of service-component architectural design. Indeed, this activity allows the detection and consequently the correction of errors early in Web systems development life cycle. In this paper, we discuss the behavioral verification problem on the SCDL/WS-BPEL service-component architectures. To do so, the Wright formal ADL and the Ada concurrent language were used as a target models. To achieve this, a set of systematic translation rules are proposed. This allows the verification of the standard behavioral properties using the Wr2fdr tool. In addition, using an Ada dynamic analysis tool, we could detect the potential behavioral properties such as the deadlock of an Ada concurrent program.


Verification Concurrent program Model-Checker Static behavioral properties Dynamic behavioral properties Service-Component architecture 


  1. 1.
    Barros, O.: Business process patterns and frameworks: reusing knowledge in process innovation. Bus. Process Manag. J. 13(1), 47–69 (2007)CrossRefGoogle Scholar
  2. 2.
    Bhiri, M.T., Fourati, F., Kmimech, M., Graiet, M.: Transformation exogène de Wright vers Ada. Technique et Science Informatiques 31(7), 839–868 (2012)CrossRefGoogle Scholar
  3. 3.
    Chama, I.E., Belala, N., Saïdouni, D.E.: Formalizing timed BPEL by D-LOTOS. IJERTCS J. 5(2), 1–21 (2014)Google Scholar
  4. 4.
    Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based verification of web service compositions. In: Proceedings of 18th IEEE International Conference on Automated Software Engineering, Montreal, Canada, pp. 152–163. IEEE, October 2003Google Scholar
  5. 5.
    Foster, H., Uchitel, S. Magee, J., Kramer, J., Magee, J.: Compatibility verification for web service choreography. In: Proceedings of the IEEE International Conference on Web Services, San Diego, CA, USA, pp. 738–741. IEEE, June 2004Google Scholar
  6. 6.
    Maâlej, A.J., Lahami, M., Krichen, M., Jmaïel, M.: Distributed and resource-aware load testing of WS-BPEL compositions. In: ICEIS (2), pp. 29–38 (2018)Google Scholar
  7. 7.
    Haddad, I., Kmimech, M., Sakka Rouis, T., Bhiri, M.T.: Towards a practical approach to check service component architecture. In: 11th International Conference on Semantics, Knowledge and Grid, pp. 65–72. IEEE (2015)Google Scholar
  8. 8.
    Hamel, L.M., Graiet, G.M., Kmimech, M.: Formal modeling for verifying SCA composion. In: RCIS Conference, pp. 193–204 (2015)Google Scholar
  9. 9.
  10. 10.
    Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and GNATprove - A competition report from builders of an industrial-strength verifying compiler. Int. J. Softw. Tools Technol. Transf. 17(6), 695–707 (2015)CrossRefGoogle Scholar
  11. 11.
    Maalej, Maroua, Taft, Tucker, Moy, Yannick: Safe dynamic memory management in ada and SPARK. In: Casimiro, António, Ferreira, Pedro M. (eds.) Ada-Europe 2018. LNCS, vol. 10873, pp. 37–52. Springer, Cham (2018). Scholar
  12. 12.
    Mateo, J.A., Ruiz, V.V., Macià, H., Díaz, G.: A coloured petri net approach to model and analyse stateful workflows based on WS-BPEL and WSRF. In: SEFM Workshops, pp. 389–404 (2014)Google Scholar
  13. 13.
    Naumovich, G., Avrunin, G.S., Clarke, L.A., Osterweil, L.J., Applying static analysis to software architectures’. In: ACM SIGSOFT 1997, Software Engineering Notes, vol. 22(6), pp. 77–93 (1997)CrossRefGoogle Scholar
  14. 14.
    OASIS. Service Component Architecture Assembly Model Specification Version 1.1. Oasis, July 2017.
  15. 15.
    Sakka Rouis, T., Bhiri, M.T., Kmimech, M., Moussa, F.: Wr2Fdr Tool Maintenance for models Checking. In: SoMeT Conference, pp. 425–440 (2017)Google Scholar
  16. 16.
    Strobl, S., Zoffi, M., Bernhart, M., Grechenig, T.: A tiered approach towards an incremental BPEL to BPMN 2.0 Migration. In: ICSME Conference, pp. 563–567 (2016)Google Scholar
  17. 17.
    Yang, Y., Tan, Q., Xiao, Y., Liu, F., Yu, J.: Transform BPEL workflow into hierarchical CP-nets to make tool support for verification. In: APWeb Conference, pp. 275–284 (2006)Google Scholar
  18. 18.
    Yeung, W.L.: Mapping WS-CDL and BPEL into CSP for behavioural specification and verification of web services. In: ECOWS, IEEE Computer, pp. 297–305 (2006)Google Scholar

Copyright information

© Springer Nature Singapore Pte Ltd. 2019

Authors and Affiliations

  • Taoufik Sakka Rouis
    • 1
    Email author
  • Mohamed Tahar Bhiri
    • 2
  • Mourad Kmimech
    • 3
  • Layth Sliman
    • 4
  1. 1.LIPAH Laboratory, FSTUniversity of Tunis El ManarTunisTunisia
  2. 2.MIRACL Laboratory, ISIMSUniversity of SfaxSfaxTunisia
  3. 3.UR-OASIS Laboratory, ENITUniversity of Tunis El ManarTunisTunisia
  4. 4.Efrei - École d’Ingénieur Généraliste en InformatiqueVillejuifFrance

Personalised recommendations