一句话：提出基于高阶变换将 BPMN 模型映射为图变换系统，以形式化执行语义并支持行为性质检查。
BPMN 是广泛使用的业务流程建模标准，但其执行语义以非形式化方式描述，导致元素解释不一致，也难以为行为性质提供可靠检查。本文提出一种 BPMN 执行语义的形式化方法，核心是使用高阶变换将 BPMN 模型转换为图变换系统。与已有方法相比，该方法覆盖更多 BPMN 元素，同时便于开展性质检查。作者还将其实现为开源 Web 工具，以展示方法的能力。
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.
@article{paperbot2718,
title = {A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems},
author = {Tim Kräuter and Adrian Rutle and Harald König and Yngve Lamo},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:4)2024}
}