O-013
時間制約を考慮したビジネスプロセスの表現と検証

◎梶村賢吾・新川芳行（龍谷大）

ネットワーク技術やweb技術の進歩により、従来、起業内で閉じていたビジネスプロセスは、企業間の相互作用を含む複雑なものとなり、この相互作用において時間制約が重要な問題となっている。本研究は、ソフトウェア開発における標準的モデル記述言語UMLのタイミング図が持つ高い時間制約記述能力と、時間オートマトンと時相論理に基づくモデル検査ツールUPPAALとの厳密な時間制約検証能力に注目し、これらを統合して、ビジネスプロセスにも適用可能なモデル化および検証手法を提案する。