Formal Verification of Business Constraints in Workflow-Based Applications

Workflows coordinate a series of computing tasks to create a sophisticated workflow logic. Ensuring the correctness of a workflow specification is essential for automating business processes. Errors in the specification should be identified and resolved as early as possible, during the design phase. In this paper, we propose a verification approach for workflow specifications utilizing model checking techniques. We introduce a method for verifying the correctness properties of workflow processes by utilizing our database-embedded Alternating-time Temporal Logic (ATL) model checker. First, the workflow specification is translated into a concurrent game structure (CGS). Next, the desired property is expressed as an ATL formula. Finally, the ATL model checker is executed to verify whether the correctness properties hold for the model. To support users in the formalization of business constraints, the proposed solution implements an assistant based on generative AI. The experimental results show that employing the chain-of-thought prompting method significantly enhances the reasoning process performance when using the GPT-4o model.