A Framework for Verifying BPMN with Hoare Logic

The Business Process Model and Notation (BPMN) has become a widely accepted standard for business process modeling. However, much of the formal verification research on BPMN is based on earlier versions and often overlooks unstructured and loop elements. This paper presents a novel approach to BPMN verification using Hoare logic. In this paper, we enhance the expressiveness and precision of BPMN by explicitly incorporating conditions into decision gateways and loop tasks. Based on this enhancement, we provide formal semantics and dynamic state explanations for BPMN diagrams. A framework is designed to partition BPMN diagrams and verify properties with our proof system based on Hoare logic, offering an intuitive, state-space explosion-free method. A logistics case study demonstrates the framework's applicability and effectiveness.