Skip to main content
SpringerLink
Log in

Formalization and Analysis of BPMN Using Graph Transformation Systems

  • Conference paper
  • First Online:
Graph Transformation (ICGT 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13961))

Included in the following conference series:

  • 294 Accesses

Abstract

The Business Process Modeling Notation (BPMN) is a widely used standard notation for defining intra- and inter-organizational workflows. However, the informal description of the BPMN execution semantics leads to different interpretations of BPMN elements and difficulties in checking behavioral properties. In this paper, we propose a formalization of the execution semantics of BPMN that, compared to existing approaches, covers more BPMN elements while facilitating property checking. Our approach is based on a higher-order transformation from BPMN models to graph transformation systems. As proof of concept, we have implemented our approach in an open-source web-based tool.

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

Access this chapter

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

References

  1. Camunda services GmbH: BPMN 2.0 implementation reference. https://docs.camunda.org/manual/7.16/reference/bpmn20/, March 2023

  2. Camunda services GmbH: Bpmn-js token simulation. https://github.com/bpmn-io/bpmn-js-token-simulation, March 2023

  3. Camunda services GmbH: Bpmnlint. https://github.com/bpmn-io/bpmnlint, March 2023

  4. Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: A formal approach for the analysis of BPMN collaboration models. J. Syst. Softw. 180, 111007 (2021). https://doi.org/10.1016/j.jss.2021.111007

    Article  Google Scholar 

  5. Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: Formalising and animating multiple instances in BPMN collaborations. Inf. Syst. 103, 101459 (2022). https://doi.org/10.1016/j.is.2019.101459

    Article  Google Scholar 

  6. Corradini, F., Muzi, C., Re, B., Tiezzi, F.: A classification of BPMN collaborations based on safeness and soundness notions. Electron. Proc. Theor. Comput. Sci. 276, 37–52 (2018). https://doi.org/10.4204/EPTCS.276.5

    Article  MathSciNet  MATH  Google Scholar 

  7. Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281–1294 (2008). https://doi.org/10.1016/j.infsof.2008.02.006

    Article  Google Scholar 

  8. Durán, F., Salaün, G.: Verifying timed BPMN processes using Maude. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. Lecture Notes in Computer Science, vol. 10319, pp. 219–236. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59746-1_12

    Chapter  Google Scholar 

  9. Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic approaches to graph transformation – part ii: single pushout approach and comparison with double pushout approach, pp. 247–312. World Scientific, February 1997. https://doi.org/10.1142/9789812384720_0004

  10. El-Saber, N.A.S.: CMMI-CM compliance checking of formal BPMN models using Maude. Ph.D. thesis, University of Leicester, January 2015

    Google Scholar 

  11. Freund, J., Rücker, B.: Real-Life BPMN: using BPMN and DMN to analyze, Improve, and automate processes in your company. Berlin, 4th edn, Camunda (2019)

    Google Scholar 

  12. Heckel, R., Taentzer, G.: Graph transformation for software engineers: with applications to model-based development and domain-specific language engineering. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-43916-3

  13. Hofstede, A., Aalst, W.: Workflow patterns: on the expressive power of (petri-net-based) workflow languages. In: Proceedings of Fourth Workshop on the Practical Use of Coloured Petri Nets and CPN Tools (CPN 2002), vol. 560, August 2002

    Google Scholar 

  14. Houhou, S., Baarir, S., Poizat, P., Quéinnec, P., Kahloul, L.: A first-order logic verification framework for communication-parametric and time-aware BPMN collaborations. Inf. Syst. 104, 101765 (2022). https://doi.org/10.1016/j.is.2021.101765

    Article  Google Scholar 

  15. Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 299–305. Springer, Heidelberg (2006). https://doi.org/10.1007/11691617_19

    Chapter  Google Scholar 

  16. Kräuter, T.: Artifacts - ICGT. https://github.com/timKraeuter/ICGT-2023, October 2023

  17. Meyers, B., Deshayes, R., Lucio, L., Syriani, E., Vangheluwe, H., Wimmer, M.: ProMoBox: a framework for generating domain-specific property languages. In: Combemale, B., Pearce, D.J., Barais, O., Vinju, J.J. (eds.) SLE 2014. LNCS, vol. 8706, pp. 1–20. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11245-9_1

    Chapter  Google Scholar 

  18. Object management group: business process model and notation (BPMN), Version 2.0.2. https://www.omg.org/spec/BPMN/, December 2013

  19. Peter, D.: Hyperfine (2022)

    Google Scholar 

  20. Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25959-6_40

    Chapter  Google Scholar 

  21. Rensink, A.: Nested quantification in graph transformation rules. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 1–13. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_1

    Chapter  MATH  Google Scholar 

  22. Rensink, A.: How much are your geraniums? Taking graph conditions beyond first order. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 191–213. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_10

    Chapter  Google Scholar 

  23. Tisi, M., Jouault, F., Fraternali, P., Ceri, S., Bézivin, J.: On the use of higher-order model transformations. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 18–33. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02674-4_3

    Chapter  Google Scholar 

  24. Van Gorp, P., Dijkman, R.: A visual token-based formalization of BPMN 2.0 based on in-place transformations. Inf. Softw. Technol. 55(2), 365–394 (2013). https://doi.org/10.1016/j.infsof.2012.08.014

Download references

Author information

Authors and Affiliations

  1. Western Norway University of Applied Sciences, Bergen, Norway

    Tim Kräuter, Adrian Rutle, Harald König & Yngve Lamo

  2. University of Applied Sciences, FHDW, Hanover, Germany

    Harald König

Authors
  1. Tim Kräuter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adrian Rutle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Harald König
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yngve Lamo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tim Kräuter .

Editor information

Editors and Affiliations

  1. King's College London, London, UK

    Maribel Fernández

  2. Singapore Management University, Singapore, Singapore

    Christopher M. Poskitt

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kräuter, T., Rutle, A., König, H., Lamo, Y. (2023). Formalization and Analysis of BPMN Using Graph Transformation Systems. In: Fernández, M., Poskitt, C.M. (eds) Graph Transformation. ICGT 2023. Lecture Notes in Computer Science, vol 13961. Springer, Cham. https://doi.org/10.1007/978-3-031-36709-0_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-36709-0_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-36708-3

  • Online ISBN: 978-3-031-36709-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation