A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets

Workflow nets (WF-nets) are Petri nets for modeling workflows, and are utilized to verification and performance evaluation of workflows. A WF-net should have a property, called soundeness, which guarantees a logical correctness of the modeled workflow. If a given WF-net is free choice then its soundness can be verified in polynomial time. Otherwise there is no polynomial time method to verify soundness for general WF-nets. Unfortunately, some workflows cannot be represented as free choice WF-nets. For example, the WF-net representing an inter-organizational workflow may become asymmetric choice. Thus an efficient method is required. In this paper, we propose a tool to verify soundness using the SPIN model checker. We also show efficiency of our tool by comparing it with an existing WF-nets analysis tool, Woflan, on verification time for asymmetric choice WF-nets.