Automated Verification of BPMN Workflows Through Promela and LTL Properties

This paper presents an automated tool for verifying Business Process Model and Notation (BPMN) workflows by generating Promela code and Linear Temporal Logic (LTL) properties. The tool integrates multiple phases of model verification, starting from BPMN workflow ingestion and translation into Promela models to the automated generation of LTL properties from state diagrams. We discuss the requirements for BPMN and state diagrams, including specific syntax and structure needed for accurate translation and verification. The methodology employs a visitor pattern to traverse BPMN elements and produce verifiable Promela code, while LTL properties are derived from boolean expressions in state diagrams. Additionally, the paper introduces an error visualization mechanism that enhances the interpretability of counterexamples by annotating BPMN and state diagrams along the error trace. Evaluation results demonstrate the tool's efficacy in handling varying complexities of BPMN workflows, highlighting its scalability and performance in different verification scenarios.