The goal of this paper is to demonstrate that process verification has matured to a level where it can be used in practice. 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 correctness of real-life models. 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 20 most frequently used patterns found today (including 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.
['Moe Thandar Wynn', 'H. M. W. Verbeek', 'W. M. P. van der Aalst', 'A.H.M. ter Hofstede', 'David Edmond']
Business process verification - finally a reality!