Summary
International Technical Conference on Circuits/Systems, Computers and Communications
2008
Session Number:F1
Session:
Number:F1-3
A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets
Shingo Yamaguchi, Munenori Yamaguchi, Minoru Tanaka,
pp.-
Publication Date:2008/7/7
Online ISSN:2188-5079
Summary:
In this paper, we propose a tool to verify soundness of acyclic WF-nets using SPIN. We first give a method to describe a given WF-net system in the modeling language of SPIN. Next we give a method to express the conditions of soundness property as Linear Temporal Logic formulas. Finally we show efficiency of our method by comparing it with Woflan on verification time for acyclic asymmetric choice WF-nets.