Skip to main content
SpringerLink
Log in
Book cover

Formal Aspects of Component Software

FACS 2015: Formal Aspects of Component Software pp 161–180Cite as

An Operational Semantics of BPMN Collaboration

  • Conference paper
  • First Online:

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

Abstract

In the last years we are observing a growing interest in formalising the execution semantics of business process modelling languages that, despite their lack of formal characterisation, are widely adopted in industry and academia. In this paper, we focus on the OMG standard BPMN 2.0. Specifically, we provide a direct formalisation of its operational semantics in terms of Labelled Transition Systems (LTS). This approach permits both to avoid possible miss-interpretations due to the usage of the natural language in the specification of the standard, and to overcome issues due to the mapping of BPMN to other formal languages, which are equipped with their own semantics. In addition, it paves the way for the use of consolidated formal reasoning techniques based on LTS (e.g., model checking). Our operational semantics is given for a relevant subset of BPMN elements focusing on the capability to model collaborations among organisations via message exchange. Moreover, one of its distinctive aspects is the suitability to model business processes with arbitrary topology. This allows designers to freely specify their processes according to the reality without the need of defining well-structured models. We illustrate our approach through a simple, yet realistic, running example about commercial transactions.

This research has been partially founded by EU project LearnPAd (GA:619583) and by the Project MIUR PRIN CINA (2010LHT4KM).

This is a preview of subscription content, 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   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

Learn about institutional subscriptions

Notes

  1. 1.

    We use BPMN or BPMN 2.0 interchangeably to refer to version 2.0 of the notation.

  2. 2.

    BPMN is currently supported by 75 tools (see http://www.bpmn.org for a detailed list).

  3. 3.

    http://maude.cs.illinois.edu/.

  4. 4.

    http://www.eclipse.org/bpmn2-modeler/.

References

  1. Lindsay, A., Downs, D., Lunn, K.: Business processes - attempts to find a definition. Inf. Softw. Technol. 45(15), 1015–1019 (2003)

    Article  Google Scholar 

  2. Reichert, M., Weber, B.: Enabling Flexibility in Process-Aware Information Systems: Challenges, Methods, Technologies. Springer, Heidelberg (2012)

    Book  Google Scholar 

  3. OMG: Business Process Model and Notation (BPMN v2.0), Normative document, Jan 2011

    Google Scholar 

  4. Breu, R., Dustdar, S., Eder, J., Huemer, C., Kappel, G., Köpke, J., Langer, P., Mangler, J., Mendling, J., Neumann, G., Rinderle-Ma, S., Schulte, S., Sobernig, S., Weber, B.: Towards living inter-organizational processes. In: CBI, pp. 363–366. IEEE (2013)

    Google Scholar 

  5. Plotkin, G.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)

    MathSciNet  Google Scholar 

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

    Article  Google Scholar 

  7. Weske, M.: Business Process Management. Springer, Heidelberg (2012)

    Book  Google Scholar 

  8. Recker, Jan, Muehlen, M.Z.: How much language is enough? theoretical and practical use of the business process modeling notation. In: Bellahsène, Z., Léonard, M. (eds.) CAiSE 2008. LNCS, vol. 5074, pp. 465–479. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Christiansen, D.R., Carbone, M., Hildebrandt, T.T.: Formal semantics and implementation of BPMN 2.0 inclusive gateways. In: WSFM, pp. 146–160 (2011)

    Google Scholar 

  10. Wilmsmann, G., Völzer, H., Gfeller, B.: Faster or-join enactment for BPMN 2.0. In: Dijkman, R., Hofstetter, J., Koehler, J. (eds.) BPMN 2011. LNBIP, vol. 95, pp. 31–43. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Dumas, M., Grosskopf, A., Hettel, T., Wynn, M.T.: Semantics of standard process models with OR-joins. In: Tari, Z., Meersman, R. (eds.) OTM 2007, Part I. LNCS, vol. 4803, pp. 41–58. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Sinot, F.-R.: Call-by-name and call-by-value as token-passing interaction nets. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 386–400. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Kirchner, F., Sinot, F.: Rule-based operational semantics for an imperative language. Electr. Notes Theor. Comput. Sci. 174(1), 35–47 (2007)

    Article  Google Scholar 

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

    Article  Google Scholar 

  15. El-Saber, N., Boronat, A.: BPMN formalization and verification using maude. In: BM-FA, pp. 1–12. ACM Press (2014)

    Google Scholar 

  16. Thalheim, B., Börger, E.: A method for verifiable and validatable business process modeling. In: Börger, E., Cisternino, A. (eds.) Advances in Software Engineering. LNCS, vol. 5316, pp. 59–115. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Laue, R., Mendling, J.: The impact of structuredness on error probability of process models. In: Kaschek, R., Kop, C., Steinberger, C., Fliedl, G. (eds.) Information Systems and e-Business Technologies. Lecture Notes in Business Information Processing, vol. 5, pp. 585–590. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Kiepuszewski, B., ter Hofstede, A.H.M., Bussler, C.J.: On structured workflow modelling. In: Wangler, B., Bergman, L.D. (eds.) CAiSE 2000. LNCS, vol. 1789, p. 431. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Polyvyanyy, A., Garcuelos, L., Dumas, M.: Structuring acyclic process models. Inf. Syst. 37(6), 518–538 (2012)

    Article  Google Scholar 

  20. Polyvyanyy, A., Garcia-Banuelos, L., Fahland, D., Weske, M.: Maximal structuring of acyclic process models. Comput. J. 57(1), 12–35 (2014)

    Article  Google Scholar 

  21. Huai, W., Liu, X., Sun, H.: Towards trustworthy composite service through business process model verification. In: UIC/ATC, pp. 422–427. IEEE (2010)

    Google Scholar 

  22. Koniewski, R., Dzielinski, A., Amborski, K.: Use of petri nets and business processes management notation in modelling and simulation of multimodal logistics chains. In: ECMS, pp. 99–102 (2006)

    Google Scholar 

  23. Ramadan, M., Elmongui, H.G., Hassan, R.: BPMN formalisation using coloured petri nets. In: SEA (2011)

    Google Scholar 

  24. Awad, A., Decker, G., Lohmann, N.: Diagnosing and repairing data anomalies in process models. In: Rinderle-Ma, S., Sadiq, S., Leymann, F. (eds.) Business Process Management Workshops. LNBIP, vol. 43, pp. 5–16. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  25. Corradini, F., Polini, A., Re, B.: Inter-organizational business process verification in public administration. Bus. Process Manag. J. 21(5), 1040–1065 (2015)

    Article  Google Scholar 

  26. Ye, J., Song, W.: Transformation of BPMN diagrams to YAWL nets. J. Softw. 5(4), 396–404 (2010)

    Article  Google Scholar 

  27. Dijkman, R., Decker, G., García-Bañuelos, L., Dumas, M.: Transforming BPMN diagrams into YAWL nets. In: Dumas, M., Reichert, M., Shan, M.-C. (eds.) BPM 2008. LNCS, vol. 5240, pp. 386–389. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Wong, P.Y., Gibbons, J.: Formalisations and applications of BPMN. Sci. Comput. Program. 76(8), 633–650 (2011)

    Article  MATH  Google Scholar 

  29. Gibbons, J., Wong, P.Y.H.: A process semantics for BPMN. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 355–374. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  30. Arbab, F., Kokash, N., Meng, S.: Towards using reo for compliance-aware business process modeling. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. CCIS, vol. 17, pp. 108–123. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Quaglia, P., Zannone, N., Prandi, D.: Formal analysis of BPMN via a translation into COWS. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 249–263. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  32. Weske, M., Puhlmann, F.: Investigations on soundness regarding lazy activities. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 145–160. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  33. Puhlmann, F.: Soundness verification of business processes specified in the Pi-calculus. In: Meersman, R., Tari, Z. (eds.) OTM 2007, Part I. LNCS, vol. 4803, pp. 6–23. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  34. Corradini, F., Polini, A., Polzonetti, A., Re, B.: Business processes verification for e-government service delivery. Inf. Syst. Manag. 27(4), 293–308 (2010)

    Article  Google Scholar 

  35. Lucanu, D., Şerbănuţă, T.F., Roşu, G.: \(\mathbb{K}\) framework distilled. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 31–53. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  36. Rosu, G., Stefanescu, A.: Matching logic: a new program verification approach. In: ICSE, pp. 868–871. ACM (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Science and Technology, University of Camerino, Camerino, Italy

    Flavio Corradini, Andrea Polini, Barbara Re & Francesco Tiezzi

Authors
  1. Flavio Corradini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrea Polini
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Barbara Re
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Francesco Tiezzi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Barbara Re .

Editor information

Editors and Affiliations

  1. Universidade Federal Fluminense, Niterói, Brazil

    Christiano Braga

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Corradini, F., Polini, A., Re, B., Tiezzi, F. (2016). An Operational Semantics of BPMN Collaboration. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28934-2_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28933-5

  • Online ISBN: 978-3-319-28934-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation