@inproceedings{6f550e75d0df4ee59f82389a7e1788c6,
title = "BDafny: A Formal Execution and Verification Framework of BPMN 2.0 in Dafny",
abstract = "Business Process Model and Notation (BPMN) has been widely adopted as the international standard for business process modeling in enterprise applications. However, existing BPMN models lack rigorous semantic definitions, leading to significant challenges in correctness verification, including deadlock detection and data conflict analysis. Divergent implementations across execution engines further exacerbate such ambiguities. To address these gaps, this paper proposes BDafny: a formal execution and verification framework for BPMN 2.0. Based on Dafny, the verification-aware language, BDafny provides: (1) Executable formalization of BPMN 2.0 semantics for Hoare-logic based behavioral reasoning. (2) Automated and proven detection of practical modeling errors. (3) Multi-target code generation for portable process deployment. By bridging formal methods with industrial standards, BDafny contributes a mechanically verified foundation for BPMN semantics, supporting correct-by-construction automation of business processes.",
keywords = "BPMN (Business Process Model and Notation), Dafny, Formal Semantics, Verification",
author = "Ziqing Su and Sini Chen and Ran Li and Huibiao Zhu and Jiapeng Wang",
note = "Publisher Copyright: {\textcopyright} 2025 IEEE.; 32nd Asia-Pacific Software Engineering Conference, APSEC 2025 ; Conference date: 02-12-2025 Through 05-12-2025",
year = "2025",
doi = "10.1109/APSEC66846.2025.00026",
language = "英语",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "161--172",
editor = "Tao Zhang and Xiapu Luo and Jacky Keung and Eunjong Choi",
booktitle = "Proceedings - 2025 32nd Asia-Pacific Software Engineering Conference, APSEC 2025",
address = "美国",
}