Formalizing and Analyzing BPMN Models Using Higher-Order Graph Transformation Systems

This article proposes a formalization of the execution semantics of the Business Process Modeling Notation (BPMN) using a higher-order transformation from BPMN models to graph transformation systems. This approach covers a wide range of BPMN elements and facilitates the checking of behavioral properties to uncover control-flow errors in BPMN models.