オブジェクト指向ペトリネットに基づくビジネスプロセスの時間制約に関するモデル検証

摘要

業務プロセス管理において、時間制約の概念は重要な要素の一つである．著者らは，オブジェクト指向ペトリネットというモデルにより業務プロセスを記述し，そのモデルに時間表現を導入し拡張することに試みている．ここでは，時間表現を導入したオブジェクト指向ペトリネットを時間オートマトンに変換し，UPPAALというモデル検査ツールを利用して，業務プロセスにおける時間制約をモデル検査手法を用いて検証する試みについて報告する．