A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems

TL;DR

This article proposes a formalization of the execution semantics of BPMN that, compared to existing approaches, covers more B PMN elements while also facilitating property checking, and is based on a higher-order transformation from BPMn models to graph transformation systems.

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 article, we propose a formalization of the execution semantics of BPMN that, compared to existing approaches, covers more BPMN elements while also facilitating property checking. Our approach is based on a higher-order transformation from BPMN models to graph transformation systems. To show the capabilities of our approach, we implemented it as an open-source web-based tool.

Figures (29)

• Figure 1: Overview of the approach
• Figure 2: Simplified excerpt of the BPMN metamodel objectmanagementgroupBusinessProcessModel2013
• Figure 3: Overview of the supported BPMN elements (structure adapted from houhouFirstOrderLogicVerification2022)
• Figure 4: BPMN execution metamodel
• Figure 5: Example start graph in abstract (left) and concrete syntax (right)