Skip to main content

A Formal Model for Business Process Configuration Verification Supporting OR-Join Semantics

  • Conference paper
  • First Online:
Book cover On the Move to Meaningful Internet Systems. OTM 2018 Conferences (OTM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11229))

  • 1615 Accesses

Abstract

In today’s industries, similar process models are typically reused in different application contexts. These models result in a number of process model variants sharing several commonalities and exhibiting some variations. Configurable process models came to represent and group these variants in a generic manner. These processes are configured according to a specific context through configurable elements. Considering the large number of possible variants as well as the potentially complex configurable process, the configuration may be a tedious task and errors may lead to serious behavioral issues. Since achieving configuration in a correct manner has become of paramount importance, the analysts undoubtedly need assistance and guidance in configuring process variants. In this work, we propose a formal behavioral model based on the Symbolic Observation Graph (SOG) allowing to find the set of deadlock-free configuration choices while avoiding the well-known state-space explosion problem and considering loops and OR-join semantics. These choices are used to support business analysts in deriving deadlock-free variants.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Notes

  1. 1.

    BPMN 2.0 specification http://www.omg.org/spec/BPMN/2.0/.

  2. 2.

    Note that our approach does not rely on specific Petri nets properties but can be applied to any formal model as soon as states and transition relations are well defined.

  3. 3.

    http://www-lipn.univ-paris13.fr/~klai/SignavioExtensionSOG.

  4. 4.

    For more details see http://www-inf.it-sudparis.eu/SIMBAD/tools/SOGImplementation.

  5. 5.

    http://www-inf.it-sudparis.eu/SIMBAD/tools/SOGEvaluation.

References

  1. van der Aalst, W.M.P., Dreiling, A., Gottschalk, F., Rosemann, M., Jansen-Vullers, M.H.: Configurable process models as a basis for reference modeling. In: Bussler, C.J., Haller, A. (eds.) BPM 2005. LNCS, vol. 3812, pp. 512–518. Springer, Heidelberg (2006). https://doi.org/10.1007/11678564_47

    Chapter  Google Scholar 

  2. Aalst, W.V.D., et al.: Preserving correctness during business process model configuration. Form. Asp. Comput. 22(3–4), 459–482 (2008)

    MATH  Google Scholar 

  3. Aalst, W.V.D., et al.: Soundness of workflow nets: classification, decidability, and analysis. Formal Asp. Comput. 23(3), 333–363 (2011)

    Article  MathSciNet  Google Scholar 

  4. Aalst, W.V.D., Lohmann, N., Rosa, M.L.: Ensuring correctness during process configuration via partner synthesis. Inf. Syst. 37(6), 574–592 (2012)

    Article  Google Scholar 

  5. Assy, N.: Automated support of the variability in configurable process models. Ph.D. thesis, University of Paris-Saclay, France (2015)

    Google Scholar 

  6. Assy, N., Gaaloul, W.: Extracting configuration guidance models from business process repositories. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 198–206. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23063-4_14

    Chapter  Google Scholar 

  7. Boubaker, S., Mammar, A., Graiet, M., Gaaloul, W.: A formal guidance approach for correct process configuration. In: Sheng, Q.Z., Stroulia, E., Tata, S., Bhiri, S. (eds.) ICSOC 2016. LNCS, vol. 9936, pp. 483–498. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46295-0_30

    Chapter  Google Scholar 

  8. Boubaker, S., Klai, K., Schmitz, K., Graiet, M., Gaaloul, W.: Deadlock-freeness verification of business process configuration using SOG. In: Maximilien, M., Vallecillo, A., Wang, J., Oriol, M. (eds.) ICSOC 2017. LNCS, vol. 10601, pp. 96–112. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-69035-3_7

    Chapter  Google Scholar 

  9. Dijkman, R., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281–1294 (2008)

    Article  Google Scholar 

  10. Gottschalk, F., Aalst, W.V.D., Jansen-Vullers, M., Rosa, M.L.: Configurable workflow models. Int. J. Coop. Inf. Syst. 17, 177–221 (2008)

    Article  Google Scholar 

  11. Haddad, S., Ilié, J.-M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 196–210. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30476-0_19

    Chapter  MATH  Google Scholar 

  12. Hallerbach, A., Bauer, T., Reichert, M.: Guaranteeing soundness of configurable process variants in Provop. In: IEEE Conference on Commerce and Enterprise Computing, CEC, pp. 98–105 (2009)

    Google Scholar 

  13. Hallerbach, A., Bauer, T., Reichert, M.: Capturing variability in business process models: the Provop approach. J. Softw. Maint. 22(6–7), 519–546 (2010)

    Google Scholar 

  14. Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 294–309. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03848-8_20

    Chapter  Google Scholar 

  15. Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl. Eng. 70(5), 467–482 (2011)

    Article  Google Scholar 

  16. La Rosa, M., et al.: Questionnaire-based variability modeling for system configuration. Softw. Syst. Model. 8(2), 251–274 (2008)

    Article  Google Scholar 

  17. Razavian, M., Khosravi, R.: Modeling variability in business process models using UML. In: Fifth International Conference on Information Technology: New Generations. ITNG 2008, pp. 82–87, April 2008

    Google Scholar 

  18. Rosemann, M., Aalst, W.V.D.: A configurable reference modelling language. Inf. Syst. 32(1), 1–23 (2007)

    Article  Google Scholar 

  19. Verbeek, H., Basten, T., Aalst, W.V.D.: Diagnosing workflow processes using Woflan. Comput. J. 44(4), 246–279 (2001)

    Article  Google Scholar 

  20. Weske, M.: Business Process Management: Concepts, Languages, Architectures. Springer, Heidelberg (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Souha Boubaker .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Boubaker, S., Klai, K., Kortas, H., Gaaloul, W. (2018). A Formal Model for Business Process Configuration Verification Supporting OR-Join Semantics. In: Panetto, H., Debruyne, C., Proper, H., Ardagna, C., Roman, D., Meersman, R. (eds) On the Move to Meaningful Internet Systems. OTM 2018 Conferences. OTM 2018. Lecture Notes in Computer Science(), vol 11229. Springer, Cham. https://doi.org/10.1007/978-3-030-02610-3_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02610-3_35

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02609-7

  • Online ISBN: 978-3-030-02610-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics