時間,資源の制約をもつビジネスプロセスの形式検証

綿引 健二  石川 冬樹  平石 邦彦  

誌名
電子情報通信学会論文誌 D   Vol.J96-D   No.8   pp.1878-1891
発行日: 2013/08/01
Online ISSN: 1881-0225
Print ISSN: 1880-4535
論文種別: 論文
専門分野: ソフトウェアシステム
キーワード: 
ビジネスプロセス,  BPMN,  モデル検査,  時間オートマトン,  

本文: PDF(1MB)
>>論文を購入


あらまし: 
ITシステムの開発においてビジネスプロセスのモデル化は非常に重要であり,その設計段階においてプロセスの正しさや妥当性を十分に検証しておく必要がある.特に,時間や資源に関する性質はボトルネック問題のようなビジネスプロセスの典型的な問題に関連しているため,注意深く分析する必要がある.本論文では,時間及び資源に関する制約をもつビジネスプロセスの性質を,モデル検査技法を用いて形式的に検証する手法を提案する.まず,ビジネスプロセスの標準記法BPMNに対して時間及び資源に関する制約を付加できるように拡張を加える.更に,拡張したBPMNで記述されたビジネスプロセスを,モデル検査ツールで検証可能な時間オートマトンに変換する方法を示す.本手法によって,プロセスの構造的な問題だけでなく,時間と資源に関連した問題を初期の設計段階において排除し,ビジネスプロセスの設計品質の保証に役立てることができる.