モデル検査ツールSPINによるワークフローネットの健全性の判定について

摘要

ワークフロー(WF)ネットはワークフローをモデル化するためのペトリネットであり,ワークフローの解析や性能評価に活用されている.WFネットが満たすべき性質として,健全性(soundness)がある.健全性はワークフローの論理的な正しさを保証する基準である.組織をまたがるワークフローは非対称選択WFネットとしてモデル化される場合がある.非対称選択WFネットに対しては健全性を多項式時間で判定する方法は知られておらず,効率の良い方法が求められている.本稿ではWFネットの健全性をモデル検査ツールSPINを用いて判定する方法を提案する.さらに非対称選択WFネットに対する健全性の判定時間を評価尺度として,既存のWFネット解析ツールWoflanと比較することによって,提案方法の有効性を示す.