Formal Modeling and Analysis of Business Process Timed Constraints | SpringerLink
Skip to main content
Springer Nature Link
Log in

Formal Modeling and Analysis of Business Process Timed Constraints

  • Conference paper
Formalisms for Reuse and Systems Integration (FMI 2014)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 346))

Included in the following conference series:

  • 423 Accesses

Abstract

In this paper, we are interested in formalization, analysis and checking of the BPEL language timed constraints at the semantic level. We propose translating rules from BPEL language to a distributed low-level real-time model (C-DATA). This model is based on true-concurrency semantics and supports at the same time timing constraints, actions durations and communicating aspects. This transformation approach gives a formal semantics to the BPEL language extended with explicit activities durations and allows the formalization and the analysis of both qualitative and quantitative requirements. The resulting C-DATA structures are then analyzed by model checking value-based temporal logic properties (TCTL) using UPPAAL.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Arkin, A., Askary, S., Fordin, S., Jekeli, W.: Web Service Choreography Interface (WSCI) 1.0 (2002), http://ifr.sap.com/wsci/specification/wsci-spec-10.htm

  2. Arkin, A.: Business Process Modeling Language, BPML (2002), http://www.bpmi.org/bpml-spec.esp

  3. Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y.: Web services choreography description language version 1.0 (December 2004), http://www.w3.org/TR/ws-cdl-10/

  4. Jordan, D., et al.: Web Services Business Process Execution Language (WSBPEL), OASIS Standard (2007), http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html

  5. Thatte, S.: microsoft corporation (2001), http://www.gotdotnet.com/tearn/xml_wsspecs/xlang-c/

  6. Leymann, F.: IBM Software Group (May 2001), http://www.ibm.com/software/solutions/webservices/pdf/WSFL.pdf

  7. Chen, J.J., Yang, Y.: Adaptive Selection of Necessary and Sufficient Checkpoints for Dynamic Verification of Temporal Constraints in Grid Workflow Systems. ACM Transactions on Autonomous and Adaptive Systems 2(2), 1–25 (2007)

    Article  Google Scholar 

  8. Chen, J.J., Yang, Y.: Temporal Dependency based Checkpoint Selection for Dynamic Verification of Fixed-Time Constraints in Grid Workflow Systems. In: Proceedings of 30th International Conference on Software Engineering, pp. 141–150 (2008)

    Google Scholar 

  9. 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 9th IEEE International Conference on Quality Software (QSIC 2009), Washington, DC, USA, pp. 92–97 (2009)

    Google Scholar 

  10. Fares, E., Bodeveix, J.P., Filali, M.: Verification of Timed BPEL 2.0 Models. Enterprise, Business-Process and Information Systems Modeling 81, 261–275 (2011)

    Article  Google Scholar 

  11. Pu, G., Zhao, X., Wang, S., Qiu, Z.: Towards the semantics and verification of BPEL4WS. In: International Workshop on Web Languages and Formal Methods (WLFM 2005), pp. 401–418 (2005)

    Google Scholar 

  12. Mateescu, R., Rampacek, S.: Formal Modeling and Discrete-Time Analysis of BPEL Web Services. International Journal of Simulation and Process Modeling (2008)

    Google Scholar 

  13. Maarouk, T.M., Saïdouni, D.E., Khergag, M.: DD-LOTOS: A distributed real time language. In: Proceedings 2nd Annual International Conference on Advances in Distributed and Parallel Computing (ADPC 2011) Special Track: Real Time Embedded Systems (RTES 2011), Singapore, pp. 45–50 (2011)

    Google Scholar 

  14. Saïdouni, D.E.: Sémantique de Maximalité: Application au Raffinement d’Actions en LOTOS. LAAS-CNRS, 7 av. du Colonel Roche, 31077 Toulouse. PhD thesis, France (1996)

    Google Scholar 

  15. Belala, N., Saïdouni, D.E.: ACTIONS DURATION IN TIMED MODELS. In: Proceeding of International Arab Conference on Information Technology (ACIT 2006), Yarmouk University, Irbid (2006)

    Google Scholar 

  16. Chama, I.E., Belala, N., Saidouni, D.E.: Formalization and analysis of Timed BPEL. In: Proceedings of The 2nd IEEE International Workshop on Formal Methods Integration (IEEE FMi 2014) in Conjunction with The 15th IEEE International Conference on Information Reuse and Integration (IEEE IRI 2014), San Francisco, California, USA, pp. 978–971 (August 2014)

    Google Scholar 

  17. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. IJSTTT 1, 134–152 (1997)

    MATH  Google Scholar 

  18. Guellati, S., Kitouni, I., Matmat, R., Saidouni, D.-E.: Timed Automata with Action Durations – From Theory to Implementation. In: Dregvaite, G., Damasevicius, R. (eds.) ICIST 2014. Communications in Computer and Information Science, vol. 465, pp. 94–109. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  19. Breugel, F.V., Koshkina, M.: Models and verification of BPEL (2006), http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf

  20. Lohmann, N.: A feature-complete Petri net semantics for WS-BPEL 2.0. In: Hee, K.V., 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 

  21. 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)

    Chapter  Google Scholar 

  22. Holanda, H., Merseguer, J., Cordeiro, G., Serra, A.: Performance Evaluation of Web Services Orchestrated with WS-BPEL4People. International Journal of Computer Networks & Communications (IJCNC) 2(6), 117–134 (2010)

    Article  Google Scholar 

  23. Li, X., Madnick, S., Zhu, H., Fan, Y.: Improving Data Quality for Web Services Composition. In: Proceedings of the 7th International Workshop on Quality in Databases, QDB 2009 (2009)

    Google Scholar 

  24. Thivolle, D.: Langages modernes pour la modélisation et la vérification des systèmes asynchrones. PhD thesis, Grenoble University (laboratory of computing), Grenoble (2011)

    Google Scholar 

  25. Turner, K.J.: Representing and analysing composed web services using CRESS. J. Netw. Comput. Appl. 30(2), 541–562 (2007)

    Article  Google Scholar 

  26. Ait-Sadoune, I., Ait-Ameur, Y.: A proof based approach for modelling and verifying web services compositions. In: Proceedings of the 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2009), Germany, pp. 1–10 (June 2009)

    Google Scholar 

  27. Ait-Sadoune, I., Ait-Ameur, Y.: From BPEL to Event B. In: Laboratory of Applied Computer Science (LISI), National Engineering School for Mechanics and Aerotechnics (ENSMA), and University of Poitiers. France (2009)

    Google Scholar 

  28. Chirichiello, A., Salaün, G.: Encoding abstract descriptions into executable web services: Towards a formal development. In: Proc. of the 3rd IEEE/WIC/ACM Intl. Conf. on Web Intelligence (WI 2005), pp. 457–463 (2005)

    Google Scholar 

  29. Ferrara, A.: Web services: a process algebra approach. In: Proceedings of the 2nd Interna tional Conference on Service Oriented Computing (ICSOC 2004), New York City, NY, USA, pp. 242–251 (2004)

    Google Scholar 

  30. Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems 14, 25–59 (1987)

    Article  Google Scholar 

  31. Fernandez, J.C., et al.: CADP - A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)

    Google Scholar 

  32. 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, Washington, DC, USA, pp. 497–504 (2006)

    Google Scholar 

  33. JBOSS JBPM BPEL (2009), https://github.com/aadamowski/jbpm-bpel/tree/master/examples/trip

  34. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 140(1), 2–34 (1993)

    Article  MathSciNet  Google Scholar 

  35. Chama, I.E., Belala, N., Saidouni, D.E.: FMEBP: A Formal Modeling Environment of Business Process. In: Dregvaite, G., Damasevicius, R. (eds.) ICIST 2014. Communications in Computer and Information Science, vol. 465, pp. 211–223. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MISC Laboratory, University of Abdelhamid Mehri, Constantine 2, Algeria

    Imed Eddine Chama, Nabil Belala & Djamel Eddine Saidouni

Authors
  1. Imed Eddine Chama
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nabil Belala
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Djamel Eddine Saidouni
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Imed Eddine Chama .

Editor information

Editors and Affiliations

  1. Ecole Nationale Supérieure d'Informatique, Alger, Algeria

    Thouraya Bouabana-Tebibel

  2. SPAWAR Systems Center Pacific, San Diego, California, USA

    Stuart H. Rubin

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Chama, I.E., Belala, N., Saidouni, D.E. (2015). Formal Modeling and Analysis of Business Process Timed Constraints. In: Bouabana-Tebibel, T., Rubin, S. (eds) Formalisms for Reuse and Systems Integration. FMI 2014. Advances in Intelligent Systems and Computing, vol 346. Springer, Cham. https://doi.org/10.1007/978-3-319-16577-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-16577-6_7

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-16576-9

  • Online ISBN: 978-3-319-16577-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation