BPMN Formalization and Verification using Maude

ABSTRACT

OMG's Business Process Model and Notation (BPMN) standard provides an informal specification of a technology independent modelling language for designing business processes. However, BPMN models may include structural issues that hinder their design. In this paper, we propose a formal characterization and semantics specification of well-formed BPMN processes in rewriting logic using Maude with a focus on data-based decision gateways and data objects semantics. Our formal specification adheres to the BPMN standards, verified with respect to the classical workflow soundness definition, and automatically verified using the verification toolkit that Maude includes.

References

1. W. M. Aalst, A. Hirnschall, and H. M. W. E. Verbeek. An Alternative Way to Analyze Workflow Graphs. In A. Pidduck, M. T. Ozsu, J. Mylopoulos, and C. C. Woo, editors, Advanced Information Systems Engineering, volume 2348 of Lecture Notes in Computer Science, pages 535--552. Springer Berlin Heidelberg, 2002.
2. E. Börger. Approaches to Modeling BPs: a Critical Analysis of BPMN, Workflow Patterns and YAWL. Software & Systems Modeling, 11(3):305--318, 2012.
3. A. Boronat and J. Meseguer. An Algebraic Semantics for MOF. In J. L. Fiadeiro and P. Inverardi, editors, FASE, LNCS, pages 377--391. Springer, 2008.
4. I. M. Chiswell. Context-free Languages. In A Course in Formal Languages, Automata and Groups, Universitext, pages 1--33. Springer London, 2009.
5. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, Berlin, 2007.
6. R. M. Dijkman, M. Dumas, and C. Ouyang. Semantics and Analysis of Business Process Models in BPMN. Information and Software Technology, 50(12):1281--1294, Nov. 2008.
7. R. M. Dijkman and P. V. Gorp. BPMN 2.0 Execution Semantics Formalized as Graph Rewrite Rules. In J. Mendling, M. Weidlich, and M. Weske, editors, Business Process Modeling Notation - Second International Workshop, BPMN 2010, volume 67 of LNBIP, pages 16--30. Springer, 2010.
8. S. Eker, J. Meseguer, and A. Sridharanarayanan. The Maude LTL Model Checker. In WRLA 2002, volume 71 of ENTCS, Amsterdam, 2002. Elsevier.
9. P. V. Gorp and R. M. Dijkman. A visual token-based formalization of BPMN 2.0 based on in-place transformations. Information & Software Technology, 55(2):365--394, 2013.
10. L. H. Grande. Introducción a la notación BPMN y su relación con las estrategias del lenguaje Maude. Master's thesis, Facultad de Informática, 2009.
11. A. Ligeza, K. Kluza, and T. Potempa. AI Aapproach to Formal Analysis of BPMN Models. Towards a Logical Model for BPMN Diagrams. In Computer Science and Information Systems (FedCSIS), 2012 Federated Conference on, pages 931--934, Sept 2012.
12. J. Meseguer. Conditional Rewriting Logic As a Unified Model of Concurrency. Theoretical Computer Science, 96(1):73--155, Apr. 1992.
13. J. Meseguer. Membership Algebra as a Logical Framework for Equational Specification. WADT '97, pages 18--61, London, 1997. Springer-Verlag.
14. M. Muehlen and J. Recker. How Much Language Is Enough? Theoretical and Practical Use of the Business Process Modeling Notation. In Z. Bellahséne and M. Léonard, editors, Advanced Information Systems Engineering, volume 5074 of Lecture Notes in Computer Science, pages 465--479. Springer Berlin Heidelberg, 2008.
15. OMG. BPMN Version 2.0. Technical Report formal/2011-01-03, 2011.
16. F. Puhlmann and M. Weske. Investigations on Soundness Regarding Lazy Activities. In Proceedings of the 4th international conference on Business Process Management, BPM'06, pages 145--160, Berlin, Heidelberg, 2006. Springer-Verlag.
17. W. M. P. van der Aalst. Verification of Workflow Nets. In P. Azéma and G. Balbo, editors, ICATPN, volume 1248 of LNCS, pages 407--426. Springer, 1997.
18. W. M. P. van der Aalst, K. M. van Hee, A. H. M. ter Hofstede, N. Sidorova, H. M. W. Verbeek, M. Voorhoeve, and M. T. Wynn. Soundness of Workflow Nets: Classification, Decidability, and Analysis. Formal Aspe. Comput., 23(3):333--363, 2011.
19. P. Y. Wong and J. Gibbons. A Process Semantics for BPMN. In Proceedings of the 10th International Conference on Formal Methods and Software Engineering, ICFEM '08, pages 355--374, Berlin, Heidelberg, 2008. Springer-Verlag.
20. P. Y. Wong and J. Gibbons. Formalisations and Applications of BPMN. Science of Computer Programming, 76(8):633--650, Aug. 2011.
21. J. Ye and W. Song. Transformation of BPMN Diagrams to YAWL Nets. Journal of Software, 5(4), 2010.

Index Terms

• Information systems

  • Information systems applications