The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Les réseaux de workflow (WF-nets) sont des réseaux de Petri qui représentent des workflows. Solidité est un critère d'exactitude logique défini pour les réseaux WF. Il est connu que la vérification de la solidité est difficile à résoudre. Dans cet article, nous proposons une méthode pour vérifier la solidité à l'aide d'un outil de vérification de modèle de logique temporelle linéaire (LTL), SPIN. Nous donnons une condition LTL nécessaire et suffisante pour vérifier la solidité des réseaux WF sans livelock. Les réseaux WF acycliques n'ont pas de livelock, mais les réseaux WF cycliques peuvent avoir un livelock. Nous donnons également une condition nécessaire et suffisante pour vérifier le livelock. Pendant ce temps, nous montrons qu'aucun outil de vérification de modèle LTL ne peut vérifier la solidité des réseaux WF avec livelock. Nous donnons les conditions nécessaires pour en vérifier la solidité. Ces conditions nous permettent d'utiliser SPIN même si un WF-net donné dispose d'un livelock. Nous développons également un outil de vérification de la solidité basé sur notre méthode. Nous montrons l'efficacité de notre méthode en comparant notre outil avec les outils de vérification de solidité existants sur le temps de vérification pour 200 réseaux ACWF cycliques.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copier
Munenori YAMAGUCHI, Shingo YAMAGUCHI, Minoru TANAKA, "A Model Checking Method of Soundness for Workflow Nets" in IEICE TRANSACTIONS on Fundamentals,
vol. E92-A, no. 11, pp. 2723-2731, November 2009, doi: 10.1587/transfun.E92.A.2723.
Abstract: Workflow nets (WF-nets) are Petri nets which represent workflows. Soundness is a criterion of logical correctness defined for WF-nets. It is known that soundness verification is intractable. In this paper, we propose a method to verify soundness using a Linear Temporal Logic (LTL) model checking tool, SPIN. We give an LTL necessary and sufficient condition to verify soundness for WF-nets without livelock. Acyclic WF-nets have no livelock, but cyclic WF-nets may have livelock. We also give a necessary and sufficient condition to verify livelock. Meanwhile, we show that any LTL model checking tool cannot verify soundness for WF-nets with livelock. We give necessary conditions to verify soundness for them. Those conditions enable us to use SPIN even if a given WF-net has livelock. We also develop a tool to verify soundness based on our method. We show effectiveness of our method by comparing our tool with existing soundness verification tools on verification time for 200 cyclic ACWF-nets.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E92.A.2723/_p
Copier
@ARTICLE{e92-a_11_2723,
author={Munenori YAMAGUCHI, Shingo YAMAGUCHI, Minoru TANAKA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={A Model Checking Method of Soundness for Workflow Nets},
year={2009},
volume={E92-A},
number={11},
pages={2723-2731},
abstract={Workflow nets (WF-nets) are Petri nets which represent workflows. Soundness is a criterion of logical correctness defined for WF-nets. It is known that soundness verification is intractable. In this paper, we propose a method to verify soundness using a Linear Temporal Logic (LTL) model checking tool, SPIN. We give an LTL necessary and sufficient condition to verify soundness for WF-nets without livelock. Acyclic WF-nets have no livelock, but cyclic WF-nets may have livelock. We also give a necessary and sufficient condition to verify livelock. Meanwhile, we show that any LTL model checking tool cannot verify soundness for WF-nets with livelock. We give necessary conditions to verify soundness for them. Those conditions enable us to use SPIN even if a given WF-net has livelock. We also develop a tool to verify soundness based on our method. We show effectiveness of our method by comparing our tool with existing soundness verification tools on verification time for 200 cyclic ACWF-nets.},
keywords={},
doi={10.1587/transfun.E92.A.2723},
ISSN={1745-1337},
month={November},}
Copier
TY - JOUR
TI - A Model Checking Method of Soundness for Workflow Nets
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2723
EP - 2731
AU - Munenori YAMAGUCHI
AU - Shingo YAMAGUCHI
AU - Minoru TANAKA
PY - 2009
DO - 10.1587/transfun.E92.A.2723
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E92-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 2009
AB - Workflow nets (WF-nets) are Petri nets which represent workflows. Soundness is a criterion of logical correctness defined for WF-nets. It is known that soundness verification is intractable. In this paper, we propose a method to verify soundness using a Linear Temporal Logic (LTL) model checking tool, SPIN. We give an LTL necessary and sufficient condition to verify soundness for WF-nets without livelock. Acyclic WF-nets have no livelock, but cyclic WF-nets may have livelock. We also give a necessary and sufficient condition to verify livelock. Meanwhile, we show that any LTL model checking tool cannot verify soundness for WF-nets with livelock. We give necessary conditions to verify soundness for them. Those conditions enable us to use SPIN even if a given WF-net has livelock. We also develop a tool to verify soundness based on our method. We show effectiveness of our method by comparing our tool with existing soundness verification tools on verification time for 200 cyclic ACWF-nets.
ER -