Skip to main content

Checking Business Process Evolution

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2016)

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

Included in the following conference series:

Abstract

Business processes support the modeling and the implementation of software as workflows of local and inter-process activities. Taking over structuring and composition, evolution has become a central concern in software development. We advocate it should be taken into account as soon as the modeling of business processes, which can thereafter be made executable using process engines or model-to-code transformations. We show here that business process evolution needs formal analysis in order to compare different versions of processes, identify precisely the differences between them, and ensure the desired consistency. To reach this objective, we first present a model transformation from the BPMN standard notation to the LNT process algebra. We then propose a set of relations for comparing business processes at the formal model level. With reference to related work, we propose a richer set of comparison primitives supporting renaming, refinement, property- and context-awareness. Thanks to an implementation of our approach that can be used through a Web application, we put the checking of evolution within the reach of business process designers.

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.

    The \(\dashrightarrow \) symbol is overloaded since a refinement rule is an evolution at the task level.

References

  1. VBPMN Framework. https://pascalpoizat.github.io/vbpmn/

  2. Arnold, A.: Finite Transition Systems - Semantics of Communicating Systems. Prentice Hall International Series in Computer Science. Prentice Hall, Hertfordshire (1994)

    MATH  Google Scholar 

  3. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  4. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Lang, F., McKinty, C., Powazny, V., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator, Version 6.1. INRIA/VASY (2014)

    Google Scholar 

  5. Christiansen, D.R., Carbone, M., Hildebrandt, T.: Formal semantics and implementation of BPMN 2.0 inclusive gateways. In: Bravetti, M., Bultan, T. (eds.) WS-FM 2010. LNCS, vol. 6551, pp. 146–160. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19589-1_10

    Chapter  Google Scholar 

  6. Corradini, F., Polini, A., Re, B., Tiezzi, F.: An operational semantics of BPMN collaboration. In: Braga, C., Ölveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 161–180. Springer, Cham (2016). doi:10.1007/978-3-319-28934-2_9

    Chapter  Google Scholar 

  7. Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 128–142. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16561-0_18

    Chapter  Google Scholar 

  8. de Medeiros, A.K.A., van der Aalst, W.M.P., Weijters, A.J.M.M.: Quantifying process equivalence based on observed behavior. Data Knowl. Eng. 64(1), 55–74 (2008)

    Article  Google Scholar 

  9. Decker, G., Weske, M.: Interaction-centric modeling of process choreographies. Inf. Syst. 36(2), 292–312 (2011)

    Article  Google Scholar 

  10. 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 

  11. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE 1999, pp. 411–420. ACM (1999)

    Google Scholar 

  12. Garavel, H., Lang, F.: SVL: A scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001. IIFIP, vol. 69, pp. 377–392. Springer, Boston, MA (2002). doi:10.1007/0-306-47003-9_24

    Chapter  Google Scholar 

  13. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A toolbox for the construction and analysis of distributed processes. STTT 2(15), 89–107 (2013)

    Article  MATH  Google Scholar 

  14. Güdemann, M., Poizat, P., Salaün, G., Dumont, A.: VerChor: A framework for verifying choreographies. In: Cortellessa, V., Varró, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 226–230. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37057-1_16

    Chapter  Google Scholar 

  15. ISO. LOTOS – A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Technical Report 8807, ISO (1989)

    Google Scholar 

  16. ISO/IEC. International Standard 19510, Information technology - Business Process Model and Notation (2013)

    Google Scholar 

  17. Kluza, K., Kaczor, K.: Overview of BPMN model equivalences. Towards normalization of BPMN diagrams. In: Proceedings of KESE 2012, pp. 38–45 (2012)

    Google Scholar 

  18. Kossak, F., Illibauer, C., Geist, V., Kubovy, J., Natschläger, C., Ziebermayr, T., Kopetzky, T., Freudenthaler, B., Schewe, K.-D.: A Rigorous Semantics for BPMN 2.0 Process Diagrams. Springer, Heidelberg (2014)

    Book  Google Scholar 

  19. Lam, V.: Foundation for equivalences of BPMN models. Theoret. Appl. Inform. 24(1), 33–66 (2012)

    Article  MathSciNet  Google Scholar 

  20. Larman, C.: Applying UML and Patterns an Introduction to Object-Oriented Analysis and Design and Iterative Development. Prentice Hall, Upper Saddle River (2005)

    Google Scholar 

  21. Martens, A.: Analyzing web service based business processes. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 19–33. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31984-9_3

    Chapter  Google Scholar 

  22. Mateescu, R., Salaün, G., Ye, L.: Quantifying the parallelism in BPMN processes using model checking. In: Proceedings of CBSE 2014, pp. 159–168 (2014)

    Google Scholar 

  23. Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68237-0_12

    Chapter  Google Scholar 

  24. OMG. Business Process Model and Notation (BPMN) - Version 2.0., January 2011

    Google Scholar 

  25. Poizat, P., Salaün, G.: Checking the realizability of BPMN 2.0 choreographies. In: Proceedings of SAC 2012, pp. 1927–1934 (2012)

    Google Scholar 

  26. Raedts, I., Petkovic, M., Usenko, Y.S., van der Werf, J.M., Groote, J.F., Somers, L.: Transformation of BPMN models for behaviour analysis. In: Proceedings of MSVVEIS 2007, pp. 126–137 (2007)

    Google Scholar 

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

    Book  MATH  Google Scholar 

  28. van der Aalst, W.M.P., Ter Hofstede, A.H.M.: YAWL: Yet another workflow language. Inf. Syst. 30, 245–275 (2003)

    Article  Google Scholar 

  29. van Dongen, B., Dijkman, R., Mendling, J.: Measuring similarity between business process models. In: Bellahsène, Z., Léonard, M. (eds.) CAiSE 2008. LNCS, vol. 5074, pp. 450–464. Springer, Heidelberg (2008). doi:10.1007/978-3-540-69534-9_34

    Chapter  Google Scholar 

  30. van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  31. Weidlich, M., Dijkman, R.M., Weske, M.: Behaviour equivalence and compatibility of business process models with complex correspondences. Comput. J. 55(11), 1398–1418 (2012)

    Article  Google Scholar 

  32. Wong, P.Y.H., Gibbons, J.: A relative timed semantics for BPMN. Electr. Notes Theor. Comput. Sci. 229(2), 59–75 (2009)

    Article  MATH  Google Scholar 

  33. Wong, P.Y.H., Gibbons, J.: A process semantics for BPMN. In: Proceedings of ICFEM 2008, pp. 355–374 (2008)

    Google Scholar 

  34. Wong, P.Y.H., Gibbons, J.: Verifying business process compatibility. In: Proceedings of QSIC 2008, pp. 126–131 (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Pascal Poizat .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Poizat, P., Salaün, G., Krishna, A. (2017). Checking Business Process Evolution. In: Kouchnarenko, O., Khosravi, R. (eds) Formal Aspects of Component Software. FACS 2016. Lecture Notes in Computer Science(), vol 10231. Springer, Cham. https://doi.org/10.1007/978-3-319-57666-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57666-4_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57665-7

  • Online ISBN: 978-3-319-57666-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics