形式手法を用いたビジネスプロセスモデリングとその検証技術に関する研究

摘要

正しいビジネスプロセスを設計することは企業経営における重要な関心事である。ビジネスプロセスは特定の目標を達成するために組織されたタスク群のことであり、タスクがどのような順で実行されるか（ワークフロー）や、タスクの実行者あるいは実行に要する資源は何か（リソース）などを定めたものである。従って、ビジネスプロセスの正しさとは、デッドロックがないこと、正しく終了することなどのワークフローに関するもの、すなわちビジネスドメインに依存しない一般的な性質や、企業の在庫管理が正しいか、あるいはタスクの実行者の権限定義に矛盾がないかなど、ビジネスドメイン固有の性質などがある。資源に関する刺約、並行性、適時性などを考慮のうえでこれらのビジネスプロセスの正しさを保証することは自明ではない。この問題における有望なアプローチとして形式手法が注目されている。形式手法とは、対象を形式的に（数学的な言語で厳密に）モデル化し、数学的理論に基づいた手法で分析·検証する手法の総称である。形式手法は元来コンピュータに関連したシステムの検証のために開発されたものであるが、いくつかのブレイクスルーを経て、ビジネスプロセスを含む様々な現実的なシステムの検証に適用されるに至っている。