Business process verification – finally a reality!

Purpose - The goal of this paper is to demonstrate that process verification has matured to a level where it can be used in practise. Earlier techniques assumed simplified process models without the more advanced constructs available in today's modelling languages (e.g., cancellation and OR-joins). This paper reports on new verification techniques that can be used to assess the cor- rectness of real-life models. Design/Methodology/approach - The proposed approach relies on using formal methods (i.e., mapping a business model to a reset net which is an extension of Petri nets, and performing state space analysis) to determine the correctness of business processes with cancellation and OR- joins. The paper also demonstrates how reduction rules can be used to improve the efficiency. We present these techniques in the context of the workflow language YAWL that provides direct support for cancellation and OR-joins. But the results also apply to other languages with these features (e.g., BPMN, EPCs, UML activity diagrams, etc.). We have developed an editor that provides diagnostic information based on the techniques presented in this paper. Findings - We propose four properties for business processes with cancellation and OR-joins, namely, soundness, weak soundness, irreducible cancellation regions, and immutable OR-joins and develop new techniques to verify these properties. Reduction rules have been used as a means of improving the efficiency of the algorithm. We demonstrate the feasibility of our verification approach using a realistic and complex business process, the visa application process for general skilled migration to Australia, modelled as a YAWL workflow with cancellation regions and OR- joins. Originality/value - Business processes sometimes require complex execution interdependencies to properly complete a process. For instance, it is possible that certain activities need to be can- celled mid-way though the process. Some parallel activities may require complex "wait and see" style synchronisation depending on a given context. These types of business processes can be found in various domains, such as application integration, B2B commerce, web service com- position and workflow systems. Even though cancellation and sophisticated join structures are present in many business processes, existing verification techniques are unable to deal with such processes. Hence, this paper plays an important role in making process verification a reality.