http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets
Shingo YAMAGUCHI,Munenori YAMAGUCHI,Minoru TANAKA 대한전자공학회 2008 ITC-CSCC :International Technical Conference on Ci Vol.2008 No.7
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.