On the verification of business processes by model checking techniques

The correctness of a workflow specification is critical for the automation of business processes. For this reason, errors in the specification should be detected and corrected as early as possible - at specification time. In this paper, we present a verification method for workflow specifications using model checking techniques. We propose an approach for verifying correctness properties of workflow processes using SPIN model checker. First, a formalized workflow specification is translated into a Promela description. Second, the desired property is translated to an LTL formula. Finally, the SPIN model checker is run to check if the correctness properties hold for the model, and, if not, to provide a counterexample.