A Model Checking Method of Soundness for Acyclic Workflow Nets Using the SPIN Model Checker

Workflow nets (WF-nets) axe Petri nets for modeling workflows, and are utilized for verification and performance evaluation of workflows. A WF-net should have a property, called soundness, 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 method to verify its soundness in polynomial time. Unfortunately some workflows cannot be represented as free choice WF-nets, so an efficient method is required. In this paper, we propose a method to verify soundness of acyclic WF-nets using the SPIN model checker. In this method, we describe a given WF-net system in the modeling language of SPIN, and express the conditions of soundness property as Linear Temporal Logic formulas. We also give a tool to verify soundness based on our method. Finally we show efficiency of our tool by comparing it with an existing WF-nets analysis tool, Woflan, on verification time.