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. A demonstration of our tool is available at https://youtu.be/MxXbNUl6IjE.

翻译：业务流程建模标注（BPMN）是定义组织内部及跨组织工作流的广泛使用的标准标注。然而，BPMN执行语义的非正式描述导致了对BPMN元素的不同解读以及检查行为属性的困难。在本文中，我们提出了一种BPMN执行语义的形式化方法，与现有方法相比，该方法覆盖了更多BPMN元素，同时便于属性检查。我们的方法基于从BPMN模型到图转换系统的高阶转换。为展示我们方法的能力，我们将其实现为基于Web的开源工具。该工具的演示可在https://youtu.be/MxXbNUl6IjE获取。