(57)【要約】  複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成することを目的とする。目標が定義されるミッション図と、各種手続きが定義されるアクティビティ図と、実行主体が有する権限が定義されるファカルティ図とを図形入力により受け付け、かかるミッション図、アクティビティ図およびファカルティ図に基づいて、各種定義ファイルを生成し、生成した定義ファイルに基づいて、挙動モデルを示す挙動モデルファイル（１６２）を生成する。
2009144826.tif 000002
【特許請求の範囲】
【請求項１】
作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成プログラムであって、
前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手順と、
前記受付手順によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手順と、
前記定義ファイル生成手順によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手順と
をコンピュータに実行させることを特徴とする検査用ファイル生成プログラム。
【請求項２】
前記受付手順は、前記各種定義情報として、該各種定義情報が図形および文字列により表された図である定義図を受け付け、
前記定義ファイル生成手順は、前記受付手順によって受け付けられた定義図に基づいて、定義ファイルを生成することを特徴とする請求項１に記載の検査用ファイル生成プログラム。
【請求項３】
前記受付手順は、前記定義図として、前記最終目標、前記サブ目標および前記制約条件が定義された定義図であるミッション図と、前記各種手続き、前記実行順序および前記実行主体が定義された定義図であるアクティビティ図と、前記実行主体が有する権限が定義された定義図であるファカルティ図とを受け付けることを特徴とする請求項２に記載の検査用ファイル生成プログラム。
【請求項４】
前記受付手順は、ＵＭＬ（Unified  Modeling  Language）の記法に則って記述された定義図を受け付けることを特徴とする請求項２または３に記載の検査用ファイル生成プログラム。
【請求項５】
前記挙動モデル生成手順によって生成された挙動モデルに基づいて、前記作業プロセスの整合性が満たされているか否かを検査する検査手順をさらにコンピュータに実行させることを特徴とする請求項１〜３のいずれか一つに記載の検査用ファイル生成プログラム。
【請求項６】
前記検査手順は、前記各種手続きが実行される際に前記サブ目標が達成されるか否か、前記各種手続きが実行される際に前記制約条件が遵守されるか否か、前記各種手続きが前記権限を有する主体によって実行されるか否か、前記最終目標が達成されるか否かを検査することを特徴とする請求項５に記載の検査用ファイル生成プログラム。
【請求項７】
前記検査手順によって前記作業プロセスが整合性を満たさないと判定された場合に、整合性を満たさない原因となっている手続きを識別できるように所定の表示部に表示させる表示制御手順をさらにコンピュータに実行させることを特徴とする請求項５に記載の検査用ファイル生成プログラム。
【請求項８】
作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成装置であって、
前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手段と、
前記受付手段によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手段と、
前記定義ファイル生成手段によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手段と
を備えたことを特徴とする検査用ファイル生成装置。
【請求項９】
前記受付手段は、前記各種定義情報として、該各種定義情報が図形および文字列により表された図である定義図を受け付け、
前記定義ファイル生成手段は、前記受付手段によって受け付けられた定義図に基づいて、定義ファイルを生成することを特徴とする請求項８に記載の検査用ファイル生成装置。
【請求項１０】
前記受付手段は、前記定義図として、前記最終目標、前記サブ目標および前記制約条件が定義された定義図であるミッション図と、前記各種手続き、前記実行順序および前記実行主体が定義された定義図であるアクティビティ図と、前記実行主体が有する権限が定義された定義図であるファカルティ図とを受け付けることを特徴とする請求項９に記載の検査用ファイル生成装置。
【請求項１１】
前記受付手段は、ＵＭＬ（Unified  Modeling  Language）の記法に則って記述された定義図を受け付けることを特徴とする請求項９または１０に記載の検査用ファイル生成装置。
【請求項１２】
前記挙動モデル生成手段によって生成された挙動モデルに基づいて、前記作業プロセスの整合性が満たされているか否かを検査する検査手段をさらに備えたことを特徴とする請求項８〜１０のいずれか一つに記載の検査用ファイル生成装置。
【請求項１３】
前記検査手段は、前記各種手続きが実行される際に前記サブ目標が達成されるか否か、前記各種手続きが実行される際に前記制約条件が遵守されるか否か、前記各種手続きが前記権限を有する主体によって実行されるか否か、前記最終目標が達成されるか否かを検査することを特徴とする請求項１２に記載の検査用ファイル生成装置。
【請求項１４】
前記検査手段によって前記作業プロセスが整合性を満たさないと判定された場合に、整合性を満たさない原因となっている手続きを識別できるように所定の表示部に表示させる表示制御手段をさらに備えたことを特徴とする請求項１２に記載の検査用ファイル生成装置。
【請求項１５】
作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成装置における検査用ファイル生成方法であって、
前記検査用ファイル生成装置が、
前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付工程と、
前記受付工程によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成工程と、
前記定義ファイル生成工程によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成工程と
を含んだことを特徴とする検査用ファイル生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法に関する。
【背景技術】
【０００２】
従来、システム管理者等が情報システムに対して作業（以下、「作業プロセス」という）を行う場合、自然言語によって記述された運用マニュアルを用いることが一般的である。例えば、サーバにパッチを適用する作業プロセスは、かかる作業の手順や規則が記述された運用マニュアルを用いて行われる。【０００３】
ところで、近年、情報システムは大規模化、複雑化しているため、作業プロセスに求められる手順や規則も複雑化している。このことは、人手で作業プロセスの妥当性を検討することを困難にさせており、障害が発生する原因になっている。また、大規模化、複雑化している情報システムにおいては、少数の人間が断片的な知識を有している場合が多い。知識が細分化されていることは、情報システムの挙動の把握を困難にするため、障害が多発する原因になっている。情報システムは、生活インフラを支えるシステムとして重要性が非常に高まっており、情報システム運用管理上の信頼性を向上させることが強く望まれている。【０００４】
そこで、近年では、作業プロセスの妥当性を機械的に検査する技術が提案されている。例えば、ＵＭＬ（Unified  Modeling  Language）図を用いて作業プロセスを記述して、かかるＵＭＬ図が所定の制約や規則等を満たしているか否かを検査する技術が提案されている。【０００５】
【特許文献１】特開２００５−２７５７４９号公報
【非特許文献１】佐々木亨  岡野浩三  楠本真二、「制約指向に基づいたＵＭＬモデルの不整合検出・解消手法の提案」、電子情報通信学会論文誌Ｄ、Ｖｏｌ．Ｊ９０−Ｄ  Ｎｏ．４  ｐｐ．１００５−１０１３、２００７年
【発明の開示】
【発明が解決しようとする課題】
【０００６】
しかしながら、上記従来技術には、単一のＵＭＬ図についてしか整合性検査を行うことができず、複数のＵＭＬ図で記述された作業プロセスについては、ＵＭＬ図間で満たされるべき制約や規則等を網羅的に検査することができないという問題があった。大規模化、複雑化している情報システムでは、作業プロセスを複数の図を用いて記述することが多く、複数のＵＭＬ図で記述された作業プロセスについても網羅的に検査することができる技術の実現が望まれていた。【０００７】
なお、網羅的に整合性検査を行うために、コンピュータが解析しやすい方式（例えば、プログラミング言語）で作業プロセスを記述することも考えられるが、システム管理者等に膨大な手間がかかる。また、コンピュータが解析しやすい方式で記述された作業プロセスは、一般に、人間にとって把握しにくく、かえって障害を招くおそれがある。【０００８】
開示の技術は、上述した従来技術による問題点を解消するためになされたものであり、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成する検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法を提供することを目的とする。
【課題を解決するための手段】
【０００９】
上述した課題を解決し、目的を達成するために、本願に開示する検査用ファイル生成プログラムは、作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成プログラムであって、前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手順と、前記受付手順によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手順と、前記定義ファイル生成手順によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手順とをコンピュータに実行させることを要件とする。【００１０】
なお、本願に開示する検査用ファイル生成プログラムの構成要素、表現または構成要素の任意の組合せを、方法、装置、システム、コンピュータプログラム、記録媒体、データ構造などに適用したものも、他の態様として有効である。
【発明の効果】
【００１１】
本願に開示した検査用ファイル生成プログラムによれば、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成することができるという効果を奏する。
【図面の簡単な説明】
【００１２】
【図１】図１は、本実施例に係る検査用ファイル生成装置の構成を示す図である。
【図２】図２は、ミッション図の一例を示す図である。
【図３】図３は、アクティビティ図の一例を示す図である。
【図４】図４は、ファカルティ図の一例を示す図である。
【図５】図５は、図３に示したアクティビティ図から生成されるアクティビティ定義ファイルの一例を示す図である。
【図６】図６は、制約条件ファイルの一例を示す図である。
【図７】図７は、挙動モデルファイルの一例を示す図である。
【図８】図８は、挙動モデルファイルに組み込む初期状態の一例を示す図である。
【図９−１】図９−１は、整合性検査結果画面の一例を示す図である。
【図９−２】図９−２は、整合性検査結果画面の一例を示す図である。
【図９−３】図９−３は、整合性検査結果画面の一例を示す図である。
【図１０】図１０は、検査用ファイル生成装置による整合性検査処理手順を示すフローチャートである。
【図１１】図１１は、挙動モデル生成部による挙動モデル生成処理手順を示すフローチャートである。
【図１２】図１２は、挙動モデル生成部による初期状態組込処理手順を示すフローチャートである。
【図１３】図１３は、制約条件ファイル生成部による制約条件ファイル生成処理手順を示すフローチャートである。
【図１４】図１４は、作業プロセス検査プログラムを実行するコンピュータを示す機能ブロック図である。
【符号の説明】
【００１３】
１００  検査用ファイル生成装置
１１０  入力部
１２０  表示部
１３０  定義ファイル出力制御部
１３１  受付部
１３２  定義ファイル生成部
１３３  表示制御部
１４０  定義ファイル格納部
１４１  共通定義ファイル
１４２  ミッション定義ファイル
１４３  アクティビティ定義ファイル
１４４  ファカルティ定義ファイル
１５０  検査制御部
１５１  制約条件ファイル生成部
１５２  挙動モデル生成部
１５３  検査部
１５４  反例生成部
１６０  検査結果ファイル格納部
１６１  制約条件ファイル
１６２  挙動モデルファイル
１６３  判定結果ファイル
１６４  反例ファイル
１０００  コンピュータ
１０１０  ＣＰＵ
１０２０  入力装置
１０３０  モニタ
１０４０  媒体読取り装置
１０５０  ネットワークインターフェース装置
１０６０  ＲＡＭ
１０６１  作業プロセス検査プロセス
１０７０  ハードディスク装置
１０７１  作業プロセス検査プログラム
１０７２  定義ファイル
１０７３  検査用データ
１０８０  バス
【発明を実施するための最良の形態】
【００１４】
以下に、本願に開示する検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法の実施例を図面に基づいて詳細に説明する。なお、この実施例により本願に開示する検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法が限定されるものではない。
【実施例】
【００１５】
まず、本実施例に係る検査用ファイル生成装置の概要について説明する。本実施例に係る検査用ファイル生成装置は、作業プロセスにおいて最終的に達成される目標と、作業プロセス内で行われる各種手続きと、各種手続きを実行する実行主体が有する権限に関する情報を受け付ける。具体的には、目標、手続き、実行主体が有する権限に関する情報は、利用者によってＵＭＬの記法を用いて入力される。そして、検査用ファイル生成装置は、入力された目標、手続き、実行主体が有する権限に関する情報に基づいて各種定義ファイルを生成する。続いて、検査用ファイル生成装置は、生成した定義ファイルに基づいて、作業プロセスを実行する際の挙動モデルが示す挙動モデルファイルを生成し、かかる挙動モデルファイルを用いて作業プロセスの整合性を検査する。これにより、本実施例に係る検査用ファイル生成装置では、利用者にとって可読性の高い作業プロセス図を用いて、作業プロセスの妥当性を網羅的に検査することが可能になる。【００１６】
なお、本明細書では、目標が記述された図を「ミッション図」と呼び、手続きが記述された図を「アクティビティ図」と呼び、実行主体が有する権限が記述された図を「ファカルティ図」と呼ぶこととする。【００１７】
このような検査用ファイル生成装置について、図１を用いて具体的に説明する。図１は、本実施例に係る検査用ファイル生成装置の構成を示す図である。図１に示すように、検査用ファイル生成装置１００は、入力部１１０と、表示部１２０と、定義ファイル出力制御部１３０と、定義ファイル格納部１４０と、検査制御部１５０と、検査結果ファイル格納部１６０とを有する。【００１８】
入力部１１０は、各種情報や操作指示を入力するための入力デバイスであり、例えば、キーボードやマウスである。表示部１２０は、各種情報を表示する表示デバイスであり、例えば、モニタである。【００１９】
なお、本実施例に係る検査用ファイル生成装置１００を用いる利用者は、表示部１２０に表示される所定のＵＭＬエディタを用いて、ミッション図、アクティビティ図およびファカルティ図を入力できるものとする。ＵＭＬエディタを実現するためのアプリケーションの例としては、「Ｅｃｌｉｐｓｅ」と、ＥｃｌｉｐｓｅのＵＭＬプラグインである「ＳｙｓｔｅｍＤｉｒｅｃｔｏｒ  Ａｐｐｌｉｃａｔｉｏｎ  Ｍｏｄｅｌｅｒ  ＵＭＬ  Ｅｄｉｔｏｒ」との組合せなどがある。【００２０】
ここで、図２〜図４を用いて、ミッション図、アクティビティ図およびファカルティ図の記述例について説明する。ここでは、作業プロセスとして、サービス用サーバを増設する例を示す。具体的には、かかる作業プロセスは、サーバの利用者がいないことを確認し、システム管理者の承認を得た後に、サービスを停止し、サービス用サーバを増設し、最後にサービスを再起動するという手続きを順に行うものとする。【００２１】
図２は、ミッション図の一例を示す図である。図２に示した例のように、ミッション図は、作業プロセスにおいて達成される目標が、ＵＭＬのクラス図によって記述される図である。具体的には、ミッション図は、作業プロセスにおいて最終的に達成される目標（以下、「最終目標」という）と、最終目標を達成するために必要な目標（以下、「サブ目標」という）が記述される。【００２２】
また、ミッション図は、各サブ目標が達成すべき条件（以下、「ゴール条件」という）と、各サブ目標が実行されている間、常に満たしていなければならない条件（以下、「制約条件」という）とが時相論理式によって記述される。具体的には、ゴール条件は、「Ｇｏａｌ」という文字列が記述されている矩形内に記述され、制約条件は、「Ｃｏｎｓｔｒａｉｎｔ」という文字列が記述されている矩形内に記述される。【００２３】
図２に例示したミッション図では、最終目標として、「Ｐ００１：サーバ増設」が記述されている。また、最終目標を達成するために必要なサブ目標として、「Ｐ００１−０１：利用者の確認」と、「Ｐ００１−０２：承認を得る」と、「Ｐ００１−０３：サーバを増設する」とが記述されている。また、サブ目標「Ｐ００１−０１：利用者の確認」のサブ目標として、「Ｐ００１−０１−０１：管理サーバにログイン」と、「Ｐ００１−０１−０２：利用者を確認」とが記述されている。【００２４】
また、図２に例示したミッション図では、サブ目標「Ｐ００１−０１−０１：管理サーバにログイン」の制約条件として、［Ｌｏｇｉｎ  ｓｅｒｖｅｒ］→ＡＦ［Ｌｏｇｏｕｔ  ｓｅｒｖｅｒ］が記述されている。かかる制約条件は、サーバにログインした後は、必ずサーバからログアウトしなければならないことを示している。【００２５】
また、サブ目標「Ｐ００１−０１−０２：利用者を確認」のゴール条件として、［Ｕｓｅｒ  ｃｈｅｃｋｅｄ］が記述されている。かかるゴール条件は、サブ目標「Ｐ００１−０１−０２：利用者を確認」が目標を達成するためには、サーバを利用するユーザが存在するか否かを確認する必要があることを示している。【００２６】
また、サブ目標「Ｐ００１−０３：サーバを増設する」のゴール条件として、［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｅｄ］が記述されている。かかるゴール条件は、サブ目標「Ｐ００１−０３：サーバを増設する」が目標を達成するためには、新しいサーバを増設する必要があることを示している。また、サブ目標「Ｐ００１−０３：サーバを増設する」の制約条件として、［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｅｄ］→［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｉｔｉｏｎ  ｇｒａｎｔｅｄ］が記述されている。かかる制約条件は、サーバを増設する際には、システム管理者の承認が得られていなければならないことを示している。【００２７】
図３は、アクティビティ図の一例を示す図である。図３に示した例のように、アクティビティ図は、ミッション図に記述される最終目標を達成するための手続きが、ＵＭＬのアクティビティ図によって記述される図である。具体的には、アクティビティ図は、各手続きの実行主体がアクティビティパーティションによって分離され、かかる主体によって実行される各手続きが有向リンクの結合によって記述される。【００２８】
また、アクティビティ図は、各手続きの事前条件または事後条件が、ノート（コメント）によって記述される。具体的には、事前条件は「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」という文字列が記述されているノート内に記述され、事後条件は「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」という文字列が記述されているノート内に記述される。【００２９】
図３に例示したアクティビティ図では、アクティビティパーティションとして、「作業者［Ｏｐｅｒａｔｏｒ］」と、「管理職［Ｍａｎａｇｅｒ］」とが記述されている。そして、実行主体「作業者」によって実行される手続きとして、手続きＡ１〜Ａ３およびＡ５〜Ａ８が記述されており、実行主体「管理職」によって実行される手続きとして、手続きＡ４が記述されている。【００３０】
また、図３に例示したアクティビティ図では、手続きＡ１「管理用サーバにログインする」の事後条件として、［Ｌｏｇｉｎ  ｓｅｒｖｅｒ］が記述されている。かかる事後条件は、手続きＡ１が実行された後には、サーバにログインしている状態でなければならないことを示している。【００３１】
また、手続きＡ４「サーバ増設承認」の事前条件として、［Ｈａｓ＿Ａｕｔｈｏｒｉｔｙ（Ｇｒａｎｔ）］が記述されており、事後条件として、［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｉｔｉｏｎ  ｇｒａｎｔｅｄ］が記述されている。かかる事前条件は、手続きＡ４が実行される際には、手続きＡ４を実行する主体（図３の例では、管理職）が承認権限を有していなければならないことを示している。また、かかる事後条件は、手続きＡ４が実行された後には、システム管理者によって承認が得られていなければならないことを示している。【００３２】
図４は、ファカルティ図の一例を示す図である。図４に示した例のように、ファカルティ図は、アクティビティ図に記述された手続きの実行主体、および、実行主体が有する権限やスキルがＵＭＬのクラス図によって記述される図である。具体的には、実行主体は「Ｒｏｌｅ」という文字列が記述されている矩形内に記述され、権限は「Ａｕｔｈｏｒｉｔｙ」という文字列が記述されている矩形内に記述され、スキルは「Ｓｋｉｌｌ」という文字列が記述されている矩形内に記述される。【００３３】
図４に例示したファカルティ図では、実行主体「Ｍａｎａｇｅｒ（管理職）」が、承認するための権限［Ｇｒａｎｔ］を有することが記述されている。また、実行主体「Ｏｐｅｒａｔｏｒ（作業者）」が、サーバを操作するためのスキル［Ｏｐｅｒａｔｅ  ｓｅｒｖｅｒ］を有することが記述されている。【００３４】
図１に示した定義ファイル出力制御部１３０は、各種定義ファイルを定義ファイル格納部１４０へ出力する制御部であり、受付部１３１と、定義ファイル生成部１３２と、表示制御部１３３とを有する。【００３５】
受付部１３１は、入力部１１０を用いて入力された各種情報や操作指示を受け付ける処理部である。具体的には、受付部１３１は、ミッション図等を作成または編集するために入力された情報を受け付け、受け付けた情報を定義ファイル生成部１３２および表示制御部１３３へ出力する。また、受付部１３１は、利用者によって作業プロセスの整合性検査を開始する旨の操作指示が行われた場合に、定義ファイル生成部１３２に対して、整合性検査を開始するように指示する。【００３６】
定義ファイル生成部１３２は、受付部１３１から整合性検査を開始する旨の指示を受け付けた場合に、受付部１３１から入力された情報に基づいて、各種定義ファイルを生成する処理部である。具体的には、定義ファイル生成部１３２は、ミッション図を作成するために入力部１１０を用いて入力された情報に基づいて、ＸＭＩ（XML（Extensible  Markup  Language）  Metadata  Interchange）形式のミッション定義ファイル１４２を生成する。【００３７】
また、定義ファイル生成部１３２は、アクティビティ図を作成するために入力部１１０を用いて入力された情報に基づいて、ＸＭＩ形式のアクティビティ定義ファイル１４３を生成する。図５に、図３に示したアクティビティ図から生成されるアクティビティ定義ファイル１４３の一例を示す。また、定義ファイル生成部１３２は、ファカルティ図を作成するために入力部１１０を用いて入力された情報に基づいて、ＸＭＩ形式のファカルティ定義ファイル１４４を生成する。【００３８】
なお、ＥｃｌｉｐｓｅのＵＭＬプラグインなどにより実現されるＵＭＬエディタは、ＵＭＬ図からＸＭＩ形式のファイルを生成する機能を有する。したがって、定義ファイル生成部１３２による定義ファイル生成処理は、既存のアプリケーションによって実現可能である。【００３９】
表示制御部１３３は、表示部１２０に各種情報を表示させる制御部である。例えば、表示制御部１３３は、受付部１３１からミッション図等を作成または編集するために入力された情報を入力された場合に、かかる情報を表示部１２０に表示させる。【００４０】
定義ファイル格納部１４０は、各種定義ファイルが格納される記憶デバイスであり、共通定義ファイル１４１と、ミッション定義ファイル１４２と、アクティビティ定義ファイル１４３と、ファカルティ定義ファイル１４４とが格納される。【００４１】
共通定義ファイル１４１は、あらゆる作業プロセスを検査する場合における共通の規則が記述されているファイルである。例えば、共通定義ファイル１４１には、「作業プロセスに開始ノードが存在すること」や、「作業プロセスに終了ノードが存在すること」という規則が記述されている。【００４２】
検査制御部１５０は、定義ファイル格納部１４０に格納されている各種定義ファイルに基づいて、作業プロセスの整合性を検査する制御部であり、制約条件ファイル生成部１５１と、挙動モデル生成部１５２と、検査部１５３と、反例生成部１５４とを有する。【００４３】
制約条件ファイル生成部１５１は、共通定義ファイル１４１と、ミッション定義ファイル１４２とに基づいて、制約条件ファイル１６１を生成する処理部である。制約条件ファイル１６１は、各手続きが満たさなければならないゴール条件および制約条件が、ＣＴＬ（Computational  Tree  Logic：計算木論理）式によって記述されるファイルである。【００４４】
ここで、制約条件ファイル生成部１５１がミッション定義ファイル１４２に基づいて制約条件ファイル１６１を生成する処理について具体的に説明する。ここでは、まず、ミッション図の論理的なデータ構造について説明し、次に、制約条件ファイル生成部１５１による制約条件ファイル１６１の生成処理について説明する。【００４５】
まず、ミッション図の論理的なデータ構造について説明する。ミッション図ＭＤの構成要素は、
ＭＤ＝（ＮＭＤ、ＴＭＤ）・・・（１）
というデータ構造によって定義される。【００４６】
上記データ構造（１）において、ＮＭＤは、ミッション図ＭＤに記述されているノードｎＭＤの集合を示す。なお、ここでいう「ノードｎＭＤ」とは、ミッション図ＭＤに記述されている最終目標およびサブ目標を示す。【００４７】
また、ノードｎＭＤは、
ｎＭＤ＝＜ＮａｍｅＭＤ、ＴｙｐｅＭＤ、ＣｏｎｔＭＤ＞・・・（２）
というデータ構造によって定義される。【００４８】
上記データ構造（２）において、ＮａｍｅＭＤは、ノードｎＭＤの名称を示す。ＴｙｐｅＭＤは、ノードｎＭＤのタイプを示す。ＣｏｎｔＭＤは、ゴール条件や制約条件の内容を示し、時相論理式によって表される。具体的には、ノードｎＭＤのＴｙｐｅＭＤが「Ｇｏａｌ」である場合、かかるノードｎＭＤのＣｏｎｔＭＤには、ゴール条件が設定される。また、ノードｎＭＤのＴｙｐｅＭＤが「Ｃｏｎｓｔｒａｉｎｔ」である場合、かかるノードｎＭＤのＣｏｎｔＭＤには、制約条件が設定される。【００４９】
ＴＭＤは、ノード集合ＮＭＤに含まれるノードｎＭＤ間の接続関係ｔＭＤの集合を示す。接続関係ｔＭＤは、例えば、＜ｎ１ＭＤ、ｎ２ＭＤ＞というデータ構造によって定義される。かかるデータ構造は、ノードｎ１ＭＤと、ノードｎ２ＭＤとが接続されていることを示す。【００５０】
なお、ミッション定義ファイル１４２は、ミッション図ＭＤを表すＸＭＩ形式のファイルであるので、ミッション定義ファイル１４２についても、上記データ構造（１）および（２）のように定義される。【００５１】
次に、制約条件ファイル生成部１５１がミッション定義ファイル１４２に基づいて制約条件ファイル１６１を生成する処理について説明する。まず、制約条件ファイル生成部１５１は、ミッション定義ファイル１４２のノード集合ＮＭＤから、ゴール条件や制約条件を示すＣｏｎｔＭＤを抽出する。続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｃｏｎｓｔｒａｉｎｔ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行されている間、常に満たしていなければならない制約条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（ＣｏｎｔＭＤ）を生成する。【００５２】
続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｇｏａｌ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行された後に満たさなければならないゴール条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（Ｆｉｎａｌ→ＣｏｎｔＭＤ）を生成する。【００５３】
そして、制約条件ファイル生成部１５１は、ＣＴＬ式により表されたゴール条件および制約条件が記述された制約条件ファイル１６１を生成する。図６は、制約条件ファイル１６１の一例を示す図である。図６に例示した制約条件ファイル１６１において、例えば、「ＡＧ（ＥＦ  ［Ｆｉｎａｌ］）」は、「あらゆる状態から、ＡｃｔｉｖｉｔｙＦｉｎａｌＮｏｄｅへ到達している状態へ到達可能である」という条件を示している。また、例えば、「ＡＧ（！Ｐｒｅｃｏｎｄｔｉｏｎ＿ｅｒｒｏｒ）」は、「あらゆる状態において、アクティビティ実行時に事前条件違反が発生しない」という条件を示している。【００５４】
図１に示した挙動モデル生成部１５２は、アクティビティ定義ファイル１４３に基づいて、作業プロセスを実行する際の挙動モデルを生成する処理部である。具体的には、挙動モデル生成部１５２は、挙動モデルとして、後述する検査部１５３が検査処理を行うことができる形式の挙動モデルファイル１６２を生成する。なお、本実施例に係る検査用ファイル生成装置１００では、検査部１５３として、モデル検査ツールであるＮｕＳＭＶを用いるものとする。したがって、挙動モデル生成部１５２は、ＳＭＶ形式の挙動モデルファイル１６２を生成する。【００５５】
また、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４に基づいて、挙動モデルにおける初期状態を生成し、生成した初期状態を挙動モデルファイル１６２に組み込む。ここでいう「初期状態」とは、作業プロセスが実行される前に成立している事象を示し、例えば、実行主体が有する権限などを示す。【００５６】
ここで、挙動モデル生成部１５２による挙動モデルファイル１６２の生成処理、および、初期状態組込処理について具体的に説明する。ここでは、まず、アクティビティ図の論理的なデータ構造について説明し、続いて、ファカルティ図の論理的なデータ構造について説明し、続いて、挙動モデルの論理的なデータ構造について説明し、続いて、挙動モデル生成部１５２による挙動モデルファイル１６２の生成処理について説明する。【００５７】
まず、アクティビティ図の論理的なデータ構造について説明する。アクティビティ図ＡＤの構成要素は、
ＡＤ＝（ＰＡＤ、ＮＡＤ、ＴＡＤ）・・・（３）
というデータ構造によって定義される。【００５８】
上記データ構造（３）において、ＰＡＤは、アクティビティ図ＡＤに記述されているパーティションｐＡＤの集合を示す。ＮＡＤは、アクティビティ図ＡＤに記述されているノードｎＡＤの集合を示す。なお、ここでいう「ノードｎＡＤ」とは、アクティビティ図ＡＤに含まれる手続きおよびノートを示す。ＴＡＤは、ノード集合ＮＡＤに含まれるノードｎＡＤ間の順序関係ｔＡＤの集合を示す。【００５９】
また、パーティションｐＡＤは、
ｐＡＤ＝＜ＮａｍｅＡＤ、ＲｏｌｅＡＤ＞・・・（４）
というデータ構造によって定義される。【００６０】
上記データ構造（４）において、ＮａｍｅＡＤは、パーティションｐＡＤの名称を示す。ＲｏｌｅＡＤは、パーティションｐＡＤの役割や、権限、スキルを示す。図３に示したアクティビティ図の例では、ＮａｍｅＡＤが「作業者」であり、ＲｏｌｅＡＤが「Ｏｐｅｒａｔｏｒ」であるパーティションｐＡＤと、ＮａｍｅＡＤが「管理職」であり、ＲｏｌｅＡＤが「Ｍａｎａｇｅｒ」であるパーティションｐＡＤとが定義される。【００６１】
また、順序関係ｔＡＤは、
ｔＡＤ＝＜ＳｒｃＡＤ、ＤｓｔＡＤ、ＲｅｌａｔｉｏｎＡＤ＞・・・（５）
というデータ構造によって定義される。【００６２】
上記データ構造（５）において、ＳｒｃＡＤは、順序関係ｔＡＤの始点となるノードを示し、ＤｓｔＡＤは、順序関係ｔＡＤの終点となるノードを示す。ＲｅｌａｔｉｏｎＡＤは、始点ノードＳｒｃＡＤと、終点ノードＤｓｔＡＤとの間の関係を示す。具体的には、ＲｅｌａｔｉｏｎＡＤには、「ＣｏｎｔｒｏｌＦｌｏｗ」または「ＣｏｍｍｅｎｔＬｉｎｅ」が設定される。【００６３】
また、ノードｎＡＤは、
ｎＡＤ＝＜ＮａｍｅＡＤ、ＴｙｐｅＡＤ、ＰｒｅＡＤ、ＰｏｓｔＡＤ＞・・・（６）
というデータ構造によって定義される。【００６４】
上記データ構造（６）において、ＮａｍｅＡＤは、ノードｎＡＤのアクション名を示す。ＴｙｐｅＡＤは、ノードｎＡＤの種類またはステレオタイプ（Stereotype）を示す。なお、ＴｙｐｅＡＤは、ＵＭＬ２．０の記述仕様に従い、「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」、「ＩｎｉｔｉａｌＮｏｄｅ」、「ＡｃｔｉｖｉｔｙＦｉｎａｌＮｏｄｅ」、「ＦｏｒｋＮｏｄｅ」、「ＪｏｉｎＮｏｄｅ」、「ＭｅｒｇｅＮｏｄｅ」、「ＤｅｃｉｓｉｏｎＮｏｄｅ」、「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」、「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」のいずれかが設定される。【００６５】
例えば、ＴｙｐｅＡＤが「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」である場合、ＮａｍｅＡＤには、「サーバにログイン」、「承認処理の実行」などが設定される。また、例えば、ＴｙｐｅＡＤが「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」または「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」などのステレオタイプである場合、ＮａｍｅＡＤには、アクションの事前条件や事後条件を表す論理式が設定される。【００６６】
ＰｒｅＡＤは、ノードｎＡＤのアクションが実行される前に満たされなければならない事前条件を示す。具体的には、ノードｎＡＤのＴｙｐｅＡＤが「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」である場合、かかるノードｎＡＤの事前条件ＰｒｅＡＤは、ノードｎＡＤと接続されており、かつ、ＴｙｐｅＡＤが「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」であるノードｎＡＤによって表される。すなわち、２つのノードｎ１ＡＤおよびｎ２ＡＤにおいて、「Ｔｙｐｅ１ＡＤ  ＝  ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」、かつ、「Ｔｙｐｅ２ＡＤ  ＝  ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」、かつ、「＜ｎ１ＡＤ、ｎ２ＡＤ、ＣｏｍｍｅｎｔＬｉｎｅ＞  ∈  ＴＡＤ」ならば、「Ｐｒｅ１ＡＤ  ＝  Ｎａｍｅ２ＡＤ」が成り立つ。【００６７】
ＰｏｓｔＡＤは、ノードｎＡＤのアクションが実行された後の事後条件を示す。具体的には、ノードｎＡＤのＴｙｐｅＡＤが「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」である場合、かかるノードｎＡＤの事後条件ＰｏｓｔＡＤは、ノードｎＡＤと接続されており、かつ、ＴｙｐｅＡＤが「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」であるノードｎＡＤによって表される。【００６８】
なお、アクティビティ定義ファイル１４３は、アクティビティ図ＡＤを表すＸＭＩ形式のファイルであるので、アクティビティ定義ファイル１４３についても、上記データ構造（３）〜（６）のように定義される。【００６９】
続いて、ファカルティ図の論理的なデータ構造について説明する。ファカルティ図ＦＤの構成要素は、
ＦＤ＝（ＮＦＤ、ＴＦＤ）・・・（７）
というデータ構造によって定義される。【００７０】
上記データ構造（７）において、ＮＦＤは、ファカルティ図ＦＤに記述されているノードｎＦＤの集合を示す。なお、ここでいう「ノードｎＦＤ」とは、ファカルティ図ＦＤに記載される実行主体、権限およびスキルを示す。ＴＦＤは、ノード集合ＮＦＤに含まれるノードｎＦＤ間の関係ｔＦＤの集合を示す。【００７１】
また、ノードｎＦＤは、
ｎＦＤ＝＜ＮａｍｅＦＤ、ＴｙｐｅＦＤ＞・・・（８）
というデータ構造によって定義される。【００７２】
上記データ構造（８）において、ＮａｍｅＦＤは、ノードｎＦＤで表される実行主体、権限またはスキルの名称を示す。ＴｙｐｅＦＤは、ノードｎＦＤのステレオタイプを示す。具体的には、ノードｎＦＤが実行主体である場合、ＴｙｐｅＦＤには「Ｒｏｌｅ」が設定され、ノードｎＦＤが権限である場合、ＴｙｐｅＦＤには「Ａｕｔｈｏｒｉｔｙ」、ノードｎＦＤがスキルである場合、ＴｙｐｅＦＤには「Ｓｋｉｌｌ」が設定される。【００７３】
図４に示したファカルティ図の例では、ＮａｍｅＦＤが「Ｍａｎａｇｅｒ」であり、ＴｙｐｅＦＤが「Ｒｏｌｅ」であるノードｎ１ＦＤと、ＮａｍｅＦＤが「Ｇｒａｎｔ」であり、ＴｙｐｅＦＤが「Ａｕｔｈｏｒｉｔｙ」であるノードｎ２ＦＤとが定義される。また、所定の関係ｔ１ＦＤによって、ノードｎ１ＦＤとノードｎ２ＦＤとが関係していることが定義される。したがって、ノードｎ１ＦＤおよびｎ２ＦＤと、関係ｔ１ＦＤによって、実行主体「Ｍａｎａｇｅｒ」が権限「Ｇｒａｎｔ」を有していることを把握できる。【００７４】
同様に、図４に示したファカルティ図の例では、ＮａｍｅＦＤが「Ｏｐｅｒａｔｏｒ」であり、ＴｙｐｅＦＤが「Ｒｏｌｅ」であるノードｎ３ＦＤと、ＮａｍｅＦＤが「Ｏｐｅｒａｔｅ  ｓｅｒｖｅｒ」であり、ＴｙｐｅＦＤが「Ｓｋｉｌｌ」であるノードｎ４ＦＤとが定義される。また、所定の関係ｔ２ＦＤによって、ノードｎ３ＦＤとノードｎ４ＦＤとが関係していることが定義される。したがって、ノードｎ３ＦＤおよびｎ４ＦＤと、関係ｔ２ＦＤによって、実行主体「Ｏｐｅｒａｔｏｒ」がスキル「Ｏｐｅｒａｔｅ  ｓｅｒｖｅｒ」を有していることを把握できる。【００７５】
なお、ファカルティ定義ファイル１４４は、ファカルティ図ＦＤを表すＸＭＩ形式のファイルであるので、ファカルティ定義ファイル１４４についても、上記データ構造（７）および（８）のように定義される。【００７６】
続いて、挙動モデル生成部１５２が生成する挙動モデルの論理的なデータ構造について説明する。挙動モデルＭＡＤは、
ＭＡＤ＝（Ｓ、ＳＩ、Ｒ、Ｌ）・・・（９）
によって定義される。【００７７】
上記データ構図（９）において、Ｓは、アクティビティ図ＡＤにおいて到達可能な状態ｓの集合を示す。ここでいう「到達可能な状態」とは、アクティビティ図ＡＤにおいて、所定の手続きが実行される前の状態と、所定の手続きが実行されている状態と、所定の手続きが実行された後の状態とを示す。図３に示したアクティビティ図の例では、Ｓには、手続きＡ１〜Ａ８が実行される前の状態、手続きＡ１〜Ａ８が実行されている状態、手続きＡ１〜Ａ８が実行された後の状態が含まれる。【００７８】
ＳＩは、状態集合Ｓに含まれる要素であり、アクティビティ図ＡＤにおける初期状態を示す。図３に示したアクティビティ図の例では、ＳＩは、手続きＡ１が実行される前の状態を示す。【００７９】
Ｌは、状態ｓから、かかる状態ｓにおいて成立している事象を表す変数への写像を与えるための関数である。ここでいう「事象を表す変数」とは、例えば、以下の（Ａ）〜（Ｄ）に示すものが定義される。【００８０】
（Ａ）ＩＮ（ｎ）
変数ＩＮ（ｎ）は、状態ｓにおいて、ノードｎＡＤにより表されるアクションが実行中である場合に、かかる実行の多重度を示す。例えば、状態ｓが実行中でない場合、ＩＮ（ｎ）＝０が成り立つ。【００８１】
（Ｂ）ＯＮ（ｔ）
変数ＯＮ（ｔ）におけるｔは、
ｔ＝＜ｎ１ＡＤ、ｎ２ＡＤ、ＣｏｎｔｒｏｌＦｌｏｗ＞・・・（１０）
により定義される。
上記式（１０）において、ノードｎ１ＡＤは、状態ｓの直前のアクションを示し、ノードｎ２ＡＤは、状態ｓの直後のアクションを示す。そして、ＯＮ（ｔ）は、ノードｎ１ＡＤにより表されるアクションが終了し、かつ、ノードｎ２ＡＤにより表されるアクションが実行前である場合に、かかる実行の多重度を示す。【００８２】
（Ｃ）Ｈａｓ＿ａｕｔｈｏｒｉｔｙ（ｘ、ｙ）・・・（１１）
上記式（１１）において、ｘは権限を示し、ｙは実行主体を示す。例えば、ファカルティ定義ファイル１４４に、実行主体ｙが権限ｘを有していることが記述されている場合、全ての状態ｓにおいて、Ｈａｓ＿ａｕｔｈｏｒｉｔｙ（ｘ、ｙ）＝１（真）が成立する。なお、実行主体ｙがスキルｘを有しているか否かの変数は、Ｈａｓ＿ｓｋｉｌｌ（ｘ、ｙ）によって表される。【００８３】
（Ｄ）Ｆｉｎａｌ
Ｆｉｎａｌは、アクティビティ図ＡＤにおいて、ＦｉｎａｌＮｏｄｅにより表されているアクションまで到達し、アクティビティが終了したことを示す。具体的には、ＴｙｐｅＡＤ＝ＦｉｎａｌＮｏｄｅのとき、状態ｓ｜＝Ｉｎ（ｎＡＤ）ならば、状態ｓ｜＝Ｆｉｎａｌが成立する。【００８４】
なお、上記（Ａ）〜（Ｄ）に示した変数は、あくまで一例であり、アクティビティ図ＡＤやミッション図ＭＤに記述される他の変数についても、各状態ｓにおける解釈を与えることができる。以下では、関数Ｌによって決定される状態ｓにおける変数ｖの値を表す関数を、ｆ（Ｌ（ｓ）、ｖ）と表すこととする。【００８５】
Ｒは、所定の状態ｓ１から別の状態ｓ２へ遷移する条件を示す。以下に、状態ｓ１から状態ｓ２へ遷移する遷移条件Ｒについて、２つの例を示して説明する。まず、ノードｎ１ＡＤで表されるアクションが実行中である状態ｓ１から、かかるアクションが実行終了後の状態ｓ２へ遷移する遷移条件Ｒ１について説明する。遷移条件Ｒ１には、以下に示す条件Ｒ１−１〜Ｒ１−７が定義される。【００８６】
（条件Ｒ１−１）
ｆ（Ｌ（ｓ１），ＩＮ（ｎ１ＡＤ））＞０が成立すること。【００８７】
（条件Ｒ１−２）
ＴＯＵＴ＝｛ｔ２ＡＤ｜ｔ２ＡＤ＝＜ｎ１ＡＤ，Ｄｓｔ２ＡＤ，ＣｏｎｔｒｏｌＦｌｏｗ＞∈Ｔ｝が空でないこと。すなわち、ノードｎ１ＡＤを始点ノードとするＣｏｎｔｒｏｌＦｌｏｗが少なくとも１つ存在すること。【００８８】
（条件Ｒ１−３）
ＴＯＵＴ＝｛ｄ１，ｄ２，・・・，ｄｍ｝のとき、Ｔｙｐｅ１ＡＤ≠ＦｏｒｋＮｏｄｅならば、所定の１つのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ２），ＯＮ（ｄｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｄｋ））＋１が成立し、ｋ≠ｌならば、ｆ（Ｌ（ｓ２），ＯＮ（ｄｌ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｄｌ））が成立すること。【００８９】
（条件Ｒ１−４）
ＴＯＵＴ＝｛ｄ１，ｄ２，・・・，ｄｍ｝のとき、Ｔｙｐｅ１ＡＤ＝ＦｏｒｋＮｏｄｅならば、すべてのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ２），ＯＮ（ｄｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｄｋ））＋１が成立すること。【００９０】
（条件Ｒ１−５）
ｆ（Ｌ（ｓ２），ＩＮ（ｎ１ＡＤ））＝ｆ（Ｌ（ｓ１），ＩＮ（ｎ１ＡＤ））−１が成立すること。【００９１】
（条件Ｒ１−６）
所定の命題αについて、α∈Ｐｏｓｔ１ＡＤならば、ｆ（Ｌ（ｓ２），α）＝１（真）が成立し、¬α∈Ｐｏｓｔ１ＡＤならば、ｆ（Ｌ（ｓ２），α）＝０（偽）が成立すること。【００９２】
（条件Ｒ１−７）
上記条件Ｒ１−１〜条件Ｒ１−６において、指定のない変数および命題ｘについては、ｆ（Ｌ（ｓ１），ｘ）＝ｆ（Ｌ（ｓ２），ｘ）が成立すること。【００９３】
続いて、所定の状態ｓ１から、ノードｎ１ＡＤで表されるアクションが実行中である状態ｓ２へ遷移する遷移条件Ｒ２について説明する。遷移条件Ｒ２には、以下に示す条件Ｒ２−１〜Ｒ２−６が定義される。【００９４】
（条件Ｒ２−１）
ＴＩＮ＝｛ｔ１ＡＤ｜ｔ１ＡＤ＝＜ｎ２ＡＤ，ｎ１ＡＤ，ＣｏｎｔｒｏｌＦｌｏｗ＞∈Ｔ｝が空でないこと。すなわち、ノードｎ２ＡＤを終点ノードとするＣｏｎｔｒｏｌＦｌｏｗが少なくとも１つ存在すること。【００９５】
（条件Ｒ２−２）
ＴＩＮ＝｛ｅ１，ｅ２，・・・，ｅｍ｝のとき、Ｔｙｐｅ１ＡＤ≠ＦｏｒｋＮｏｄｅならば、所定の１つのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））＞０、かつ、ｆ（Ｌ（ｓ２），ＯＮ（ｅｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））−１が成立し、ｋ≠ｌならば、ｆ（Ｌ（ｓ２），ＯＮ（ｅｌ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｅｌ））が成立すること。【００９６】
（条件Ｒ２−３）
ＴＩＮ＝｛ｅ１，ｅ２，・・・，ｅｍ｝のとき、Ｔｙｐｅ１ＡＤ＝ＦｏｒｋＮｏｄｅならば、すべてのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））＞０、かつ、ｆ（Ｌ（ｓ２），ＯＮ（ｅｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））−１が成立すること。【００９７】
（条件Ｒ２−４）
ｆ（Ｌ（ｓ２），ＩＮ（ｎ１ＡＤ））＝ｆ（Ｌ（ｓ１），ＩＮ（ｎ１ＡＤ））＋１が成立すること。【００９８】
（条件Ｒ２−５）
所定の命題αについて、α∈Ｐｒｅ１ＡＤならば、ｆ（Ｌ（ｓ１），α）＝１（真）が成立し、¬α∈Ｐｒｅ１ＡＤならば、ｆ（Ｌ（ｓ１），α）＝０（偽）が成立すること。【００９９】
（条件Ｒ２−６）
上記条件Ｒ２−１〜条件Ｒ２−６において、指定のない変数および命題ｘについては、ｆ（Ｌ（ｓ１），ｘ）＝ｆ（Ｌ（ｓ２），ｘ）が成立すること。【０１００】
続いて、挙動モデル生成部１５２による挙動モデルファイル１６２の生成処理について説明する。挙動モデル生成部１５２は、アクティビティ定義ファイル１４３から、順序関係ＴＡＤを抽出する。続いて、挙動モデル生成部１５２は、抽出した順序関係ＴＡＤから各状態ｓ間の遷移関係を構築する。続いて、挙動モデル生成部１５２は、アクティビティ定義ファイル１４３から、各ノードｎＡＤの事前条件ＰｒｅＡＤと、事後状態ＰｏｓｔＡＤとを抽出する。続いて、挙動モデル生成部１５２は、事前条件ＰｒｅＡＤおよび事後状態ＰｏｓｔＡＤに基づいて、各状態ｓにおける真理値を割り当てて、挙動モデルファイル１６２を生成する。【０１０１】
図７は、ＳＭＶ形式の挙動モデルファイル１６２の一例を示す図である。図７に示した挙動モデルファイル１６２において、「ｉｎ＿０＿１」は、図３に示した手続きＡ２が実行中であることを示しており、「ｏｎ＿６」は、手続きＡ２の直前のリンクまで実行が終了したことを示す。すなわち、図７に示した挙動モデルファイル１６２は、手続きＡ２が実行される状態に遷移するとき、「ｏｎ＿６」を「１」減算し、「ｉｎ＿０＿１」を「１」加算し、「Ｕｓｅｒ＿ｃｈｅｃｋｅｄ」の値を１（真）にすることを示している。【０１０２】
次に、挙動モデル生成部１５２による初期状態組込処理について説明する。挙動モデル生成部１５２は、ファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ１ＦＤと、ＴｙｐｅＦＤが「Ａｕｔｈｏｒｉｔｙ」である権限のＮａｍｅ２ＦＤとの関係を抽出する。続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ１ＦＤが、抽出した権限Ｎａｍｅ２ＦＤを有することを示す自相論理式を生成する。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ａｕｔｏｒｉｔｙ（Ｎａｍｅ１ＦＤ、Ｎａｍｅ２ＦＤ）を生成する。【０１０３】
続いて、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ３ＦＤと、ＴｙｐｅＦＤが「Ｓｋｉｌｌ」である権限のＮａｍｅ４ＦＤとの関係を抽出する。続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ３ＦＤが、抽出したスキルＮａｍｅ４ＦＤを有することを示す自相論理式を生成する。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ｓｋｉｌｌ（Ｎａｍｅ３ＦＤ、Ｎａｍｅ４ＦＤ）を生成する。【０１０４】
図８は、挙動モデルファイル１６２に組み込む初期状態の一例を示す図である。例えば、図８中の定義８１は、「管理職は、承認権限を有している」ということを示している。挙動モデル生成部１５２は、このように定義される初期状態を、挙動モデルファイル１６２に組み込む。なお、挙動モデル生成部１５２は、初期状態を、挙動モデルファイル１６２に組み込まず、初期状態が定義されている別のファイルを生成してもよい。【０１０５】
検査部１５３は、制約条件ファイル１６１と、挙動モデルファイル１６２とに基づいて、作業プロセスの整合性が満たされているか否かを検査する処理部である。具体的には、検査部１５３は、権限またはスキルを有する実行主体によって各手続きが実行されているか否か、制約条件ファイル１６１に定義されている制約条件を満たしつつ各手続きが実行されるか否か、制約条件ファイル１６１に定義されているゴール条件を満たすか否かを検査する。そして、検査部１５３は、作業プロセスの整合性が満たされていない場合に、判定結果ファイル１６３を生成する。なお、ＮｕＳＭＶは、判定結果ファイル１６３を生成する機能を有しており、かかる判定結果ファイル１６３は、テキスト形式のファイルである。【０１０６】
反例生成部１５４は、検査部１５３によって生成されたテキスト形式の判定結果ファイル１６３から、ＸＭＩ形式の反例ファイル１６４を生成する処理部である。具体的には、反例生成部１５４は、整合性が満たされていない手続きを視覚的に把握できるように、ＸＭＩ形式の反例ファイル１６４を生成する。例えば、反例生成部１５４は、整合性が満たされていない原因となっている手続きの表示色を、他の手続きの表示色と変更するように、反例ファイル１６４を生成する。【０１０７】
そして、反例生成部１５４は、生成した反例ファイル１６４を表示制御部１３３へ出力する。反例ファイル１６４を受け付けた表示制御部１３３は、表示部１２０にアクティビティ図を表示させる。ここで、図９−１〜図９−３を用いて、反例生成部１５４によって生成された反例ファイル１６４に基づいて、表示制御部１３３が表示部１２０に表示させるアクティビティ図の例について説明する。図９−１〜図９−３は、整合性検査後に表示される画面（以下、「整合性検査結果画面」という）の一例を示す図である。【０１０８】
図９−１〜図９−３は、図３に示したアクティビティ図と比較して、手続きＡ３から手続きＡ４へのリンクが、手続きＡ３から手続きＡ５へのリンクに変更され、かつ、手続きＡ８が削除されたアクティビティ図に対する整合性検査結果画面を示している。ここでは、利用者によって入力されたミッション図は、図２に示したミッション図であり、利用者によって入力されたファカルティ図は、図４に示したファカルティ図であるものとする。【０１０９】
かかる場合、制約条件ファイル生成部１５１は、図６に示した条件Ｐ１〜Ｐ７を含む制約条件ファイル１６１を生成し、検査部１５３は、条件Ｐ４、Ｐ６およびＰ７に対する違反を検出する。このうち、図９−１に例示した整合性検査結果画面は、条件Ｐ４に対する違反を検出したことが視覚的に把握できるように表示されている。具体的には、図９−１に例示した整合性検査結果画面は、手続きＡ４の表示色を変更することで、手続きＡ４を経由せずに、作業プロセスが実行される可能性があることが把握できるように表示されている。すなわち、図９−１に例示した整合性検査結果画面によれば、ミッション図におけるサブ目標「Ｐ００１−０２：承認を得る」が達成されずに作業プロセスが終了する可能性があることを把握できる。【０１１０】
また、図９−２に例示した整合性検査結果画面は、条件Ｐ６に対する違反を検出したことが視覚的に把握できるように表示されている。具体的には、図９−２に例示した整合性検査結果画面は、手続きＡ４および手続きＡ７の表示色を変更することで、手続きＡ４を経由しなければ、「サーバ増設時に承認を得ていること」という制約条件に違反することが把握できるように表示されている。【０１１１】
また、図９−３に例示した整合性検査結果画面は、条件Ｐ７に対する違反を検出したことが視覚的に把握できるように表示されている。具体的には、図９−３に例示した整合性検査結果画面は、手続きＡ３の表示色を変更することで、管理サーバにログインした状態のままで、作業プロセスが終了することが把握できるように表示されている。【０１１２】
なお、図９−１〜図９−３に示した整合性検査結果画面は、あくまで一例であり、反例生成部１５４は、他の整合性検査結果画面が表示されるように反例ファイル１６４を生成してもよい。例えば、反例生成部１５４は、整合性が満たされない原因となっている手続き近傍に、かかる原因が文字列によって表示されるように反例ファイル１６４を生成してもよい。【０１１３】
検査結果ファイル格納部１６０は、検査結果に関する各種ファイルが格納される記憶デバイスであり、制約条件ファイル１６１と、挙動モデルファイル１６２と、判定結果ファイル１６３と、反例ファイル１６４とが格納される。【０１１４】
次に、本実施例に係る検査用ファイル生成装置１００による整合性検査処理の手順について説明する。図１０は、検査用ファイル生成装置１００による整合性検査処理手順を示すフローチャートである。図１０に示すように、検査用ファイル生成装置１００の受付部１３１は、ミッション図、アクティビティ図またはファカルティ図を作成または編集するための情報を受け付ける（ステップＳ１０１）。【０１１５】
続いて、受付部１３１によって作業プロセスの整合性検査を開始する旨の操作指示が受け付けられた場合（ステップＳ１０２肯定）、定義ファイル生成部１３２は、各種定義ファイルを生成する（ステップＳ１０３）。具体的には、定義ファイル生成部１３２は、ミッション図を作成するために入力された情報に基づいて、ミッション定義ファイル１４２を生成する。また、定義ファイル生成部１３２は、アクティビティ図を作成するために入力された情報に基づいて、アクティビティ定義ファイル１４３を生成する。また、定義ファイル生成部１３２は、ファカルティ図を作成するために入力された情報に基づいて、ファカルティ定義ファイル１４４を生成する。【０１１６】
続いて、表示制御部１３３は、定義ファイル生成部１３２によってアクティビティ定義ファイル１４３が生成されなかった場合（ステップＳ１０４否定）、表示部１２０に、アクティビティ図を作成する旨のエラーを表示させる（ステップＳ１０５）。【０１１７】
一方、定義ファイル生成部１３２によってアクティビティ定義ファイル１４３が生成された場合（ステップＳ１０４肯定）、挙動モデル生成部１５２は、アクティビティ定義ファイル１４３に基づいて、挙動モデルファイル１６２を生成する挙動モデル生成処理を行う（ステップＳ１０６）。なお、挙動モデル生成部１５２による挙動モデル生成処理については、後に詳述する。【０１１８】
続いて、定義ファイル生成部１３２によってファカルティ定義ファイル１４４が生成された場合（ステップＳ１０７肯定）、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４に基づいて、挙動モデルファイル１６２に初期状態を組み込む初期状態組込処理を行う（ステップＳ１０８）。一方、定義ファイル生成部１３２によってファカルティ定義ファイル１４４が生成されなかった場合（ステップＳ１０７否定）、挙動モデル生成部１５２は、初期状態組込処理を行わない。なお、挙動モデル生成部１５２による初期状態組込処理については、後に詳述する。【０１１９】
続いて、定義ファイル生成部１３２によってミッション定義ファイル１４２が生成された場合（ステップＳ１０９肯定）、制約条件ファイル生成部１５１は、共通定義ファイル１４１と、ミッション定義ファイル１４２とに基づいて、制約条件ファイル１６１を生成する制約条件ファイル生成処理を行う（ステップＳ１１０）。なお、制約条件ファイル生成部１５１による制約条件ファイル生成処理については、後に詳述する。【０１２０】
一方、定義ファイル生成部１３２によってミッション定義ファイル１４２が生成されなかった場合（ステップＳ１０９否定）、制約条件ファイル生成部１５１は、共通定義ファイル１４１に基づいて、制約条件ファイル１６１を生成する（ステップＳ１１１）。【０１２１】
続いて、検査部１５３は、制約条件ファイル１６１と、挙動モデルファイル１６２とに基づいて、作業プロセスの整合性が満たされているか否かを検査する（ステップＳ１１２）。作業プロセスの整合性が満たされている場合（ステップＳ１１３肯定）、検査部１５３は、処理を終了する。このとき、表示制御部１３３は、表示部１２０に、作業プロセスの整合性が満たされている旨を表示させてもよい。【０１２２】
一方、作業プロセスの整合性が満たされていない場合（ステップＳ１１３否定）、検査部１５３は、判定結果ファイル１６３を生成する（ステップＳ１１４）。続いて、反例生成部１５４は、検査部１５３によって生成された判定結果ファイル１６３から、反例ファイル１６４を生成する（ステップＳ１１５）。そして、表示制御部１３３は、反例生成部１５４によって生成された反例ファイル１６４に基づいて、表示部１２０に、整合性検査結果画面を表示させる（ステップＳ１１６）。【０１２３】
次に、挙動モデル生成部１５２による挙動モデル生成処理の手順について説明する。図１１は、挙動モデル生成部１５２による挙動モデル生成処理手順を示すフローチャートである。図１１に示すように、挙動モデル生成部１５２は、論理的なデータ構造に定義できるアクティビティ定義ファイル１４３から、順序関係ＴＡＤを抽出する（ステップＳ２０１）。【０１２４】
続いて、挙動モデル生成部１５２は、抽出した順序関係ＴＡＤから各状態ｓ間の遷移関係を構築する（ステップＳ２０２）。続いて、挙動モデル生成部１５２は、アクティビティ定義ファイル１４３から、各ノードｎＡＤの事前条件ＰｒｅＡＤと、事後状態ＰｏｓｔＡＤとを抽出する（ステップＳ２０３）。【０１２５】
続いて、挙動モデル生成部１５２は、事前条件ＰｒｅＡＤおよび事後状態ＰｏｓｔＡＤに基づいて、各状態ｓにおける真理値を割り当てて（ステップＳ２０４）、挙動モデルファイル１６２を生成する（ステップＳ２０５）。【０１２６】
次に、挙動モデル生成部１５２による初期状態組込処理の手順について説明する。図１２は、挙動モデル生成部１５２による初期状態組込処理手順を示すフローチャートである。図１２に示すように、挙動モデル生成部１５２は、論理的なデータ構造に定義できるファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ１ＦＤと、ＴｙｐｅＦＤが「Ａｕｔｈｏｒｉｔｙ」である権限のＮａｍｅ２ＦＤとの関係を抽出する（ステップＳ３０１）。【０１２７】
続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ１ＦＤが、抽出した権限Ｎａｍｅ２ＦＤを有することを示す自相論理式を生成する（ステップＳ３０２）。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ａｕｔｏｒｉｔｙ（Ｎａｍｅ１ＦＤ、Ｎａｍｅ２ＦＤ）を生成する。【０１２８】
続いて、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ３ＦＤと、ＴｙｐｅＦＤが「Ｓｋｉｌｌ」である権限のＮａｍｅ４ＦＤとの関係を抽出する（ステップＳ３０３）。続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ３ＦＤが、抽出したスキルＮａｍｅ４ＦＤを有することを示す自相論理式を生成する（ステップＳ３０４）。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ｓｋｉｌｌ（Ｎａｍｅ３ＦＤ、Ｎａｍｅ４ＦＤ）を生成する。【０１２９】
そして、挙動モデル生成部１５２は、上記ステップＳ３０２およびＳ３０４において生成した自相論理式を初期状態として、挙動モデルファイル１６２に組み込む（ステップＳ３０５）。【０１３０】
次に、制約条件ファイル生成部１５１による制約条件ファイル生成処理の手順について説明する。図１３は、制約条件ファイル生成部１５１による制約条件ファイル生成処理手順を示すフローチャートである。図１３に示すように、制約条件ファイル生成部１５１は、論理的なデータ構造に定義できるミッション定義ファイル１４２のノード集合ＮＭＤから、ゴール条件や制約条件を示すＣｏｎｔＭＤを抽出する（ステップＳ４０１）。【０１３１】
続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｃｏｎｓｔｒａｉｎｔ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行されている間、常に満たしていなければならない制約条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（ＣｏｎｔＭＤ）を生成する（ステップＳ４０２）。【０１３２】
続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｇｏａｌ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行された後に満たさなければならないゴール条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（Ｆｉｎａｌ→ＣｏｎｔＭＤ）を生成する（ステップＳ４０３）。【０１３３】
そして、制約条件ファイル生成部１５１は、ＣＴＬ式により表されたゴール条件および制約条件が記述された制約条件ファイル１６１を生成する（ステップＳ４０４）。【０１３４】
上述してきたように、本実施例に係る検査用ファイル生成装置１００は、目標が定義されるミッション図と、各種手続きが定義されるアクティビティ図と、実行主体が有する権限が定義されるファカルティ図とを図形入力により受け付け、かかるミッション図、アクティビティ図およびファカルティ図に基づいて、各種定義ファイルを生成し、生成した定義ファイルに基づいて、挙動モデルを示す挙動モデルファイル１６２を生成するので、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成することができる。【０１３５】
また、本実施例に係る検査用ファイル生成装置１００は、生成した挙動モデルファイル１６２を用いて、作業プロセスの整合性を検査するので、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うことができる。【０１３６】
なお、上記実施例では、検査用ファイル生成装置１００が、挙動モデルファイル１６２を生成して、生成した挙動モデルファイル１６２に基づいて作業プロセスの整合性を検査する例について説明したが、検査用ファイル生成装置１００は、挙動モデルファイル１６２の生成処理までを行い、作業プロセスの整合性検査処理については、他の情報処理装置を行ってもよい。【０１３７】
また、図１に示した検査用ファイル生成装置１００の構成は、要旨を逸脱しない範囲で種々に変更することができる。例えば、検査用ファイル生成装置１００の定義ファイル出力制御部１３０および検査制御部１５０の機能をソフトウェアとして実装し、これをコンピュータで実行することにより、検査用ファイル生成装置１００と同等の機能を実現することもできる。以下に、定義ファイル出力制御部１３０および検査制御部１５０の機能をソフトウェアとして実装した作業プロセス検査プログラム１０７１を実行するコンピュータの一例を示す。【０１３８】
図１４は、作業プロセス検査プログラム１０７１を実行するコンピュータ１０００を示す機能ブロック図である。このコンピュータ１０００は、各種演算処理を実行するＣＰＵ（Central  Processing  Unit）１０１０と、ユーザからのデータの入力を受け付ける入力装置１０２０と、各種情報を表示するモニタ１０３０と、記録媒体からプログラム等を読み取る媒体読取り装置１０４０と、ネットワークを介して他のコンピュータとの間でデータの授受を行うネットワークインターフェース装置１０５０と、各種情報を一時記憶するＲＡＭ（Random  Access  Memory）１０６０と、ハードディスク装置１０７０とをバス１０８０で接続して構成される。【０１３９】
そして、ハードディスク装置１０７０には、図１に示した定義ファイル出力制御部１３０および検査制御部１５０と同様の機能を有する作業プロセス検査プログラム１０７１と、図１に示した定義ファイル格納部１４０に記憶される各種データに対応する定義ファイル１０７２と、図１に示した検査結果ファイル格納部１６０に記憶される各種データに対応する検査用データ１０７３とが記憶される。なお、定義ファイル１０７２または検査用データ１０７３を、適宜分散させ、ネットワークを介して接続された他のコンピュータに記憶させておくこともできる。【０１４０】
そして、ＣＰＵ１０１０が作業プロセス検査プログラム１０７１をハードディスク装置１０７０から読み出してＲＡＭ１０６０に展開することにより、作業プロセス検査プログラム１０７１は、作業プロセス検査プロセス１０６１として機能するようになる。そして、作業プロセス検査プロセス１０６１は、定義ファイル１０７２および検査用データ１０７３から読み出した情報等を適宜ＲＡＭ１０６０上の自身に割り当てられた領域に展開し、この展開したデータ等に基づいて各種データ処理を実行する。【０１４１】
なお、上記の作業プロセス検査プログラム１０７１は、必ずしもハードディスク装置１０７０に格納されている必要はなく、ＣＤ−ＲＯＭ等の記憶媒体に記憶されたこのプログラムを、コンピュータ１０００が読み出して実行するようにしてもよい。また、公衆回線、インターネット、ＬＡＮ（Local  Area  Network）、ＷＡＮ（Wide  Area  Network）等を介してコンピュータ１０００に接続される他のコンピュータ（またはサーバ）等にこのプログラムを記憶させておき、コンピュータ１０００がこれらからプログラムを読み出して実行するようにしてもよい。
【図１】
2009144826.tif 000003
【図２】
2009144826.tif 000004
【図３】
2009144826.tif 000005
【図４】
2009144826.tif 000006
【図５】
2009144826.tif 000007
【図６】
2009144826.tif 000008
【図７】
2009144826.tif 000009
【図８】
2009144826.tif 000010
【図９−１】
2009144826.tif 000011
【図９−２】
2009144826.tif 000012
【図９−３】
2009144826.tif 000013
【図１０】
2009144826.tif 000014
【図１１】
2009144826.tif 000015
【図１２】
2009144826.tif 000016
【図１３】
2009144826.tif 000017
【図１４】
2009144826.tif 000018
【手続補正書】
【提出日】平成22年6月24日(2010.6.24)
【手続補正１】
【補正対象書類名】明細書
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法に関する。
【背景技術】
【０００２】
従来、システム管理者等が情報システムに対して作業（以下、「作業プロセス」という）を行う場合、自然言語によって記述された運用マニュアルを用いることが一般的である。例えば、サーバにパッチを適用する作業プロセスは、かかる作業の手順や規則が記述された運用マニュアルを用いて行われる。
【０００３】
ところで、近年、情報システムは大規模化、複雑化しているため、作業プロセスに求められる手順や規則も複雑化している。このことは、人手で作業プロセスの妥当性を検討することを困難にさせており、障害が発生する原因になっている。また、大規模化、複雑化している情報システムにおいては、少数の人間が断片的な知識を有している場合が多い。知識が細分化されていることは、情報システムの挙動の把握を困難にするため、障害が多発する原因になっている。情報システムは、生活インフラを支えるシステムとして重要性が非常に高まっており、情報システム運用管理上の信頼性を向上させることが強く望まれている。
【０００４】
そこで、近年では、作業プロセスの妥当性を機械的に検査する技術が提案されている。例えば、ＵＭＬ（Unified  Modeling  Language）図を用いて作業プロセスを記述して、かかるＵＭＬ図が所定の制約や規則等を満たしているか否かを検査する技術が提案されている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００５−２７５７４９号公報
【非特許文献】
【０００６】
【非特許文献１】佐々木亨  岡野浩三  楠本真二、「制約指向に基づいたＵＭＬモデルの不整合検出・解消手法の提案」、電子情報通信学会論文誌Ｄ、Ｖｏｌ．Ｊ９０−Ｄ  Ｎｏ．４  ｐｐ．１００５−１０１３、２００７年
【発明の概要】
【発明が解決しようとする課題】
【０００７】
しかしながら、上記従来技術には、単一のＵＭＬ図についてしか整合性検査を行うことができず、複数のＵＭＬ図で記述された作業プロセスについては、ＵＭＬ図間で満たされるべき制約や規則等を網羅的に検査することができないという問題があった。大規模化、複雑化している情報システムでは、作業プロセスを複数の図を用いて記述することが多く、複数のＵＭＬ図で記述された作業プロセスについても網羅的に検査することができる技術の実現が望まれていた。
【０００８】
なお、網羅的に整合性検査を行うために、コンピュータが解析しやすい方式（例えば、プログラミング言語）で作業プロセスを記述することも考えられるが、システム管理者等に膨大な手間がかかる。また、コンピュータが解析しやすい方式で記述された作業プロセスは、一般に、人間にとって把握しにくく、かえって障害を招くおそれがある。
【０００９】
開示の技術は、上述した従来技術による問題点を解消するためになされたものであり、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成する検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法を提供することを目的とする。
【課題を解決するための手段】
【００１０】
上述した課題を解決し、目的を達成するために、本願に開示する検査用ファイル生成プログラムは、作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成プログラムであって、前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手順と、前記受付手順によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手順と、前記定義ファイル生成手順によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手順とをコンピュータに実行させることを要件とする。
【００１１】
なお、本願に開示する検査用ファイル生成プログラムの構成要素、表現または構成要素の任意の組合せを、方法、装置、システム、コンピュータプログラム、記録媒体、データ構造などに適用したものも、他の態様として有効である。
【発明の効果】
【００１２】
本願に開示した検査用ファイル生成プログラムによれば、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成することができるという効果を奏する。
【図面の簡単な説明】
【００１３】
【図１】図１は、本実施例に係る検査用ファイル生成装置の構成を示す図である。
【図２】図２は、ミッション図の一例を示す図である。
【図３】図３は、アクティビティ図の一例を示す図である。
【図４】図４は、ファカルティ図の一例を示す図である。
【図５】図５は、図３に示したアクティビティ図から生成されるアクティビティ定義ファイルの一例を示す図である。
【図６】図６は、制約条件ファイルの一例を示す図である。
【図７】図７は、挙動モデルファイルの一例を示す図である。
【図８】図８は、挙動モデルファイルに組み込む初期状態の一例を示す図である。
【図９−１】図９−１は、整合性検査結果画面の一例を示す図である。
【図９−２】図９−２は、整合性検査結果画面の一例を示す図である。
【図９−３】図９−３は、整合性検査結果画面の一例を示す図である。
【図１０】図１０は、検査用ファイル生成装置による整合性検査処理手順を示すフローチャートである。
【図１１】図１１は、挙動モデル生成部による挙動モデル生成処理手順を示すフローチャートである。
【図１２】図１２は、挙動モデル生成部による初期状態組込処理手順を示すフローチャートである。
【図１３】図１３は、制約条件ファイル生成部による制約条件ファイル生成処理手順を示すフローチャートである。
【図１４】図１４は、作業プロセス検査プログラムを実行するコンピュータを示す機能ブロック図である。
【発明を実施するための形態】
【００１４】
以下に、本願に開示する検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法の実施例を図面に基づいて詳細に説明する。なお、この実施例により本願に開示する検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法が限定されるものではない。
【実施例】
【００１５】
まず、本実施例に係る検査用ファイル生成装置の概要について説明する。本実施例に係る検査用ファイル生成装置は、作業プロセスにおいて最終的に達成される目標と、作業プロセス内で行われる各種手続きと、各種手続きを実行する実行主体が有する権限に関する情報を受け付ける。具体的には、目標、手続き、実行主体が有する権限に関する情報は、利用者によってＵＭＬの記法を用いて入力される。そして、検査用ファイル生成装置は、入力された目標、手続き、実行主体が有する権限に関する情報に基づいて各種定義ファイルを生成する。続いて、検査用ファイル生成装置は、生成した定義ファイルに基づいて、作業プロセスを実行する際の挙動モデルが示す挙動モデルファイルを生成し、かかる挙動モデルファイルを用いて作業プロセスの整合性を検査する。これにより、本実施例に係る検査用ファイル生成装置では、利用者にとって可読性の高い作業プロセス図を用いて、作業プロセスの妥当性を網羅的に検査することが可能になる。
【００１６】
なお、本明細書では、目標が記述された図を「ミッション図」と呼び、手続きが記述された図を「アクティビティ図」と呼び、実行主体が有する権限が記述された図を「ファカルティ図」と呼ぶこととする。
【００１７】
このような検査用ファイル生成装置について、図１を用いて具体的に説明する。図１は、本実施例に係る検査用ファイル生成装置の構成を示す図である。図１に示すように、検査用ファイル生成装置１００は、入力部１１０と、表示部１２０と、定義ファイル出力制御部１３０と、定義ファイル格納部１４０と、検査制御部１５０と、検査結果ファイル格納部１６０とを有する。
【００１８】
入力部１１０は、各種情報や操作指示を入力するための入力デバイスであり、例えば、キーボードやマウスである。表示部１２０は、各種情報を表示する表示デバイスであり、例えば、モニタである。
【００１９】
なお、本実施例に係る検査用ファイル生成装置１００を用いる利用者は、表示部１２０に表示される所定のＵＭＬエディタを用いて、ミッション図、アクティビティ図およびファカルティ図を入力できるものとする。ＵＭＬエディタを実現するためのアプリケーションの例としては、「Ｅｃｌｉｐｓｅ」と、ＥｃｌｉｐｓｅのＵＭＬプラグインである「ＳｙｓｔｅｍＤｉｒｅｃｔｏｒ  Ａｐｐｌｉｃａｔｉｏｎ  Ｍｏｄｅｌｅｒ  ＵＭＬ  Ｅｄｉｔｏｒ」との組合せなどがある。
【００２０】
ここで、図２〜図４を用いて、ミッション図、アクティビティ図およびファカルティ図の記述例について説明する。ここでは、作業プロセスとして、サービス用サーバを増設する例を示す。具体的には、かかる作業プロセスは、サーバの利用者がいないことを確認し、システム管理者の承認を得た後に、サービスを停止し、サービス用サーバを増設し、最後にサービスを再起動するという手続きを順に行うものとする。
【００２１】
図２は、ミッション図の一例を示す図である。図２に示した例のように、ミッション図は、作業プロセスにおいて達成される目標が、ＵＭＬのクラス図によって記述される図である。具体的には、ミッション図は、作業プロセスにおいて最終的に達成される目標（以下、「最終目標」という）と、最終目標を達成するために必要な目標（以下、「サブ目標」という）が記述される。
【００２２】
また、ミッション図は、各サブ目標が達成すべき条件（以下、「ゴール条件」という）と、各サブ目標が実行されている間、常に満たしていなければならない条件（以下、「制約条件」という）とが時相論理式によって記述される。具体的には、ゴール条件は、「Ｇｏａｌ」という文字列が記述されている矩形内に記述され、制約条件は、「Ｃｏｎｓｔｒａｉｎｔ」という文字列が記述されている矩形内に記述される。
【００２３】
図２に例示したミッション図では、最終目標として、「Ｐ００１：サーバ増設」が記述されている。また、最終目標を達成するために必要なサブ目標として、「Ｐ００１−０１：利用者の確認」と、「Ｐ００１−０２：承認を得る」と、「Ｐ００１−０３：サーバを増設する」とが記述されている。また、サブ目標「Ｐ００１−０１：利用者の確認」のサブ目標として、「Ｐ００１−０１−０１：管理サーバにログイン」と、「Ｐ００１−０１−０２：利用者を確認」とが記述されている。
【００２４】
また、図２に例示したミッション図では、サブ目標「Ｐ００１−０１−０１：管理サーバにログイン」の制約条件として、［Ｌｏｇｉｎ  ｓｅｒｖｅｒ］→ＡＦ［Ｌｏｇｏｕｔ  ｓｅｒｖｅｒ］が記述されている。かかる制約条件は、サーバにログインした後は、必ずサーバからログアウトしなければならないことを示している。
【００２５】
また、サブ目標「Ｐ００１−０１−０２：利用者を確認」のゴール条件として、［Ｕｓｅｒ  ｃｈｅｃｋｅｄ］が記述されている。かかるゴール条件は、サブ目標「Ｐ００１−０１−０２：利用者を確認」が目標を達成するためには、サーバを利用するユーザが存在するか否かを確認する必要があることを示している。
【００２６】
また、サブ目標「Ｐ００１−０３：サーバを増設する」のゴール条件として、［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｅｄ］が記述されている。かかるゴール条件は、サブ目標「Ｐ００１−０３：サーバを増設する」が目標を達成するためには、新しいサーバを増設する必要があることを示している。また、サブ目標「Ｐ００１−０３：サーバを増設する」の制約条件として、［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｅｄ］→［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｉｔｉｏｎ  ｇｒａｎｔｅｄ］が記述されている。かかる制約条件は、サーバを増設する際には、システム管理者の承認が得られていなければならないことを示している。
【００２７】
図３は、アクティビティ図の一例を示す図である。図３に示した例のように、アクティビティ図は、ミッション図に記述される最終目標を達成するための手続きが、ＵＭＬのアクティビティ図によって記述される図である。具体的には、アクティビティ図は、各手続きの実行主体がアクティビティパーティションによって分離され、かかる主体によって実行される各手続きが有向リンクの結合によって記述される。
【００２８】
また、アクティビティ図は、各手続きの事前条件または事後条件が、ノート（コメント）によって記述される。具体的には、事前条件は「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」という文字列が記述されているノート内に記述され、事後条件は「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」という文字列が記述されているノート内に記述される。
【００２９】
図３に例示したアクティビティ図では、アクティビティパーティションとして、「作業者［Ｏｐｅｒａｔｏｒ］」と、「管理職［Ｍａｎａｇｅｒ］」とが記述されている。そして、実行主体「作業者」によって実行される手続きとして、手続きＡ１〜Ａ３およびＡ５〜Ａ８が記述されており、実行主体「管理職」によって実行される手続きとして、手続きＡ４が記述されている。
【００３０】
また、図３に例示したアクティビティ図では、手続きＡ１「管理用サーバにログインする」の事後条件として、［Ｌｏｇｉｎ  ｓｅｒｖｅｒ］が記述されている。かかる事後条件は、手続きＡ１が実行された後には、サーバにログインしている状態でなければならないことを示している。
【００３１】
また、手続きＡ４「サーバ増設承認」の事前条件として、［Ｈａｓ＿Ａｕｔｈｏｒｉｔｙ（Ｇｒａｎｔ）］が記述されており、事後条件として、［Ｎｅｗ  ｓｅｒｖｅｒ  ａｄｄｉｔｉｏｎ  ｇｒａｎｔｅｄ］が記述されている。かかる事前条件は、手続きＡ４が実行される際には、手続きＡ４を実行する主体（図３の例では、管理職）が承認権限を有していなければならないことを示している。また、かかる事後条件は、手続きＡ４が実行された後には、システム管理者によって承認が得られていなければならないことを示している。
【００３２】
図４は、ファカルティ図の一例を示す図である。図４に示した例のように、ファカルティ図は、アクティビティ図に記述された手続きの実行主体、および、実行主体が有する権限やスキルがＵＭＬのクラス図によって記述される図である。具体的には、実行主体は「Ｒｏｌｅ」という文字列が記述されている矩形内に記述され、権限は「Ａｕｔｈｏｒｉｔｙ」という文字列が記述されている矩形内に記述され、スキルは「Ｓｋｉｌｌ」という文字列が記述されている矩形内に記述される。
【００３３】
図４に例示したファカルティ図では、実行主体「Ｍａｎａｇｅｒ（管理職）」が、承認するための権限［Ｇｒａｎｔ］を有することが記述されている。また、実行主体「Ｏｐｅｒａｔｏｒ（作業者）」が、サーバを操作するためのスキル［Ｏｐｅｒａｔｅ  ｓｅｒｖｅｒ］を有することが記述されている。
【００３４】
図１に示した定義ファイル出力制御部１３０は、各種定義ファイルを定義ファイル格納部１４０へ出力する制御部であり、受付部１３１と、定義ファイル生成部１３２と、表示制御部１３３とを有する。
【００３５】
受付部１３１は、入力部１１０を用いて入力された各種情報や操作指示を受け付ける処理部である。具体的には、受付部１３１は、ミッション図等を作成または編集するために入力された情報を受け付け、受け付けた情報を定義ファイル生成部１３２および表示制御部１３３へ出力する。また、受付部１３１は、利用者によって作業プロセスの整合性検査を開始する旨の操作指示が行われた場合に、定義ファイル生成部１３２に対して、整合性検査を開始するように指示する。
【００３６】
定義ファイル生成部１３２は、受付部１３１から整合性検査を開始する旨の指示を受け付けた場合に、受付部１３１から入力された情報に基づいて、各種定義ファイルを生成する処理部である。具体的には、定義ファイル生成部１３２は、ミッション図を作成するために入力部１１０を用いて入力された情報に基づいて、ＸＭＩ（XML（Extensible  Markup  Language）  Metadata  Interchange）形式のミッション定義ファイル１４２を生成する。
【００３７】
また、定義ファイル生成部１３２は、アクティビティ図を作成するために入力部１１０を用いて入力された情報に基づいて、ＸＭＩ形式のアクティビティ定義ファイル１４３を生成する。図５に、図３に示したアクティビティ図から生成されるアクティビティ定義ファイル１４３の一例を示す。また、定義ファイル生成部１３２は、ファカルティ図を作成するために入力部１１０を用いて入力された情報に基づいて、ＸＭＩ形式のファカルティ定義ファイル１４４を生成する。
【００３８】
なお、ＥｃｌｉｐｓｅのＵＭＬプラグインなどにより実現されるＵＭＬエディタは、ＵＭＬ図からＸＭＩ形式のファイルを生成する機能を有する。したがって、定義ファイル生成部１３２による定義ファイル生成処理は、既存のアプリケーションによって実現可能である。
【００３９】
表示制御部１３３は、表示部１２０に各種情報を表示させる制御部である。例えば、表示制御部１３３は、受付部１３１からミッション図等を作成または編集するために入力された情報を入力された場合に、かかる情報を表示部１２０に表示させる。
【００４０】
定義ファイル格納部１４０は、各種定義ファイルが格納される記憶デバイスであり、共通定義ファイル１４１と、ミッション定義ファイル１４２と、アクティビティ定義ファイル１４３と、ファカルティ定義ファイル１４４とが格納される。
【００４１】
共通定義ファイル１４１は、あらゆる作業プロセスを検査する場合における共通の規則が記述されているファイルである。例えば、共通定義ファイル１４１には、「作業プロセスに開始ノードが存在すること」や、「作業プロセスに終了ノードが存在すること」という規則が記述されている。
【００４２】
検査制御部１５０は、定義ファイル格納部１４０に格納されている各種定義ファイルに基づいて、作業プロセスの整合性を検査する制御部であり、制約条件ファイル生成部１５１と、挙動モデル生成部１５２と、検査部１５３と、反例生成部１５４とを有する。
【００４３】
制約条件ファイル生成部１５１は、共通定義ファイル１４１と、ミッション定義ファイル１４２とに基づいて、制約条件ファイル１６１を生成する処理部である。制約条件ファイル１６１は、各手続きが満たさなければならないゴール条件および制約条件が、ＣＴＬ（Computational  Tree  Logic：計算木論理）式によって記述されるファイルである。
【００４４】
ここで、制約条件ファイル生成部１５１がミッション定義ファイル１４２に基づいて制約条件ファイル１６１を生成する処理について具体的に説明する。ここでは、まず、ミッション図の論理的なデータ構造について説明し、次に、制約条件ファイル生成部１５１による制約条件ファイル１６１の生成処理について説明する。
【００４５】
まず、ミッション図の論理的なデータ構造について説明する。ミッション図ＭＤの構成要素は、
ＭＤ＝（ＮＭＤ、ＴＭＤ）・・・（１）
というデータ構造によって定義される。
【００４６】
上記データ構造（１）において、ＮＭＤは、ミッション図ＭＤに記述されているノードｎＭＤの集合を示す。なお、ここでいう「ノードｎＭＤ」とは、ミッション図ＭＤに記述されている最終目標およびサブ目標を示す。
【００４７】
また、ノードｎＭＤは、
ｎＭＤ＝＜ＮａｍｅＭＤ、ＴｙｐｅＭＤ、ＣｏｎｔＭＤ＞・・・（２）
というデータ構造によって定義される。
【００４８】
上記データ構造（２）において、ＮａｍｅＭＤは、ノードｎＭＤの名称を示す。ＴｙｐｅＭＤは、ノードｎＭＤのタイプを示す。ＣｏｎｔＭＤは、ゴール条件や制約条件の内容を示し、時相論理式によって表される。具体的には、ノードｎＭＤのＴｙｐｅＭＤが「Ｇｏａｌ」である場合、かかるノードｎＭＤのＣｏｎｔＭＤには、ゴール条件が設定される。また、ノードｎＭＤのＴｙｐｅＭＤが「Ｃｏｎｓｔｒａｉｎｔ」である場合、かかるノードｎＭＤのＣｏｎｔＭＤには、制約条件が設定される。
【００４９】
ＴＭＤは、ノード集合ＮＭＤに含まれるノードｎＭＤ間の接続関係ｔＭＤの集合を示す。接続関係ｔＭＤは、例えば、＜ｎ１ＭＤ、ｎ２ＭＤ＞というデータ構造によって定義される。かかるデータ構造は、ノードｎ１ＭＤと、ノードｎ２ＭＤとが接続されていることを示す。
【００５０】
なお、ミッション定義ファイル１４２は、ミッション図ＭＤを表すＸＭＩ形式のファイルであるので、ミッション定義ファイル１４２についても、上記データ構造（１）および（２）のように定義される。
【００５１】
次に、制約条件ファイル生成部１５１がミッション定義ファイル１４２に基づいて制約条件ファイル１６１を生成する処理について説明する。まず、制約条件ファイル生成部１５１は、ミッション定義ファイル１４２のノード集合ＮＭＤから、ゴール条件や制約条件を示すＣｏｎｔＭＤを抽出する。続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｃｏｎｓｔｒａｉｎｔ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行されている間、常に満たしていなければならない制約条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（ＣｏｎｔＭＤ）を生成する。
【００５２】
続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｇｏａｌ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行された後に満たさなければならないゴール条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（Ｆｉｎａｌ→ＣｏｎｔＭＤ）を生成する。
【００５３】
そして、制約条件ファイル生成部１５１は、ＣＴＬ式により表されたゴール条件および制約条件が記述された制約条件ファイル１６１を生成する。図６は、制約条件ファイル１６１の一例を示す図である。図６に例示した制約条件ファイル１６１において、例えば、「ＡＧ（ＥＦ  ［Ｆｉｎａｌ］）」は、「あらゆる状態から、ＡｃｔｉｖｉｔｙＦｉｎａｌＮｏｄｅへ到達している状態へ到達可能である」という条件を示している。また、例えば、「ＡＧ（！Ｐｒｅｃｏｎｄｔｉｏｎ＿ｅｒｒｏｒ）」は、「あらゆる状態において、アクティビティ実行時に事前条件違反が発生しない」という条件を示している。
【００５４】
図１に示した挙動モデル生成部１５２は、アクティビティ定義ファイル１４３に基づいて、作業プロセスを実行する際の挙動モデルを生成する処理部である。具体的には、挙動モデル生成部１５２は、挙動モデルとして、後述する検査部１５３が検査処理を行うことができる形式の挙動モデルファイル１６２を生成する。なお、本実施例に係る検査用ファイル生成装置１００では、検査部１５３として、モデル検査ツールであるＮｕＳＭＶを用いるものとする。したがって、挙動モデル生成部１５２は、ＳＭＶ形式の挙動モデルファイル１６２を生成する。
【００５５】
また、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４に基づいて、挙動モデルにおける初期状態を生成し、生成した初期状態を挙動モデルファイル１６２に組み込む。ここでいう「初期状態」とは、作業プロセスが実行される前に成立している事象を示し、例えば、実行主体が有する権限などを示す。
【００５６】
ここで、挙動モデル生成部１５２による挙動モデルファイル１６２の生成処理、および、初期状態組込処理について具体的に説明する。ここでは、まず、アクティビティ図の論理的なデータ構造について説明し、続いて、ファカルティ図の論理的なデータ構造について説明し、続いて、挙動モデルの論理的なデータ構造について説明し、続いて、挙動モデル生成部１５２による挙動モデルファイル１６２の生成処理について説明する。
【００５７】
まず、アクティビティ図の論理的なデータ構造について説明する。アクティビティ図ＡＤの構成要素は、
ＡＤ＝（ＰＡＤ、ＮＡＤ、ＴＡＤ）・・・（３）
というデータ構造によって定義される。
【００５８】
上記データ構造（３）において、ＰＡＤは、アクティビティ図ＡＤに記述されているパーティションｐＡＤの集合を示す。ＮＡＤは、アクティビティ図ＡＤに記述されているノードｎＡＤの集合を示す。なお、ここでいう「ノードｎＡＤ」とは、アクティビティ図ＡＤに含まれる手続きおよびノートを示す。ＴＡＤは、ノード集合ＮＡＤに含まれるノードｎＡＤ間の順序関係ｔＡＤの集合を示す。
【００５９】
また、パーティションｐＡＤは、
ｐＡＤ＝＜ＮａｍｅＡＤ、ＲｏｌｅＡＤ＞・・・（４）
というデータ構造によって定義される。
【００６０】
上記データ構造（４）において、ＮａｍｅＡＤは、パーティションｐＡＤの名称を示す。ＲｏｌｅＡＤは、パーティションｐＡＤの役割や、権限、スキルを示す。図３に示したアクティビティ図の例では、ＮａｍｅＡＤが「作業者」であり、ＲｏｌｅＡＤが「Ｏｐｅｒａｔｏｒ」であるパーティションｐＡＤと、ＮａｍｅＡＤが「管理職」であり、ＲｏｌｅＡＤが「Ｍａｎａｇｅｒ」であるパーティションｐＡＤとが定義される。
【００６１】
また、順序関係ｔＡＤは、
ｔＡＤ＝＜ＳｒｃＡＤ、ＤｓｔＡＤ、ＲｅｌａｔｉｏｎＡＤ＞・・・（５）
というデータ構造によって定義される。
【００６２】
上記データ構造（５）において、ＳｒｃＡＤは、順序関係ｔＡＤの始点となるノードを示し、ＤｓｔＡＤは、順序関係ｔＡＤの終点となるノードを示す。ＲｅｌａｔｉｏｎＡＤは、始点ノードＳｒｃＡＤと、終点ノードＤｓｔＡＤとの間の関係を示す。具体的には、ＲｅｌａｔｉｏｎＡＤには、「ＣｏｎｔｒｏｌＦｌｏｗ」または「ＣｏｍｍｅｎｔＬｉｎｅ」が設定される。
【００６３】
また、ノードｎＡＤは、
ｎＡＤ＝＜ＮａｍｅＡＤ、ＴｙｐｅＡＤ、ＰｒｅＡＤ、ＰｏｓｔＡＤ＞・・・（６）
というデータ構造によって定義される。
【００６４】
上記データ構造（６）において、ＮａｍｅＡＤは、ノードｎＡＤのアクション名を示す。ＴｙｐｅＡＤは、ノードｎＡＤの種類またはステレオタイプ（Stereotype）を示す。なお、ＴｙｐｅＡＤは、ＵＭＬ２．０の記述仕様に従い、「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」、「ＩｎｉｔｉａｌＮｏｄｅ」、「ＡｃｔｉｖｉｔｙＦｉｎａｌＮｏｄｅ」、「ＦｏｒｋＮｏｄｅ」、「ＪｏｉｎＮｏｄｅ」、「ＭｅｒｇｅＮｏｄｅ」、「ＤｅｃｉｓｉｏｎＮｏｄｅ」、「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」、「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」のいずれかが設定される。
【００６５】
例えば、ＴｙｐｅＡＤが「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」である場合、ＮａｍｅＡＤには、「サーバにログイン」、「承認処理の実行」などが設定される。また、例えば、ＴｙｐｅＡＤが「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」または「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」などのステレオタイプである場合、ＮａｍｅＡＤには、アクションの事前条件や事後条件を表す論理式が設定される。
【００６６】
ＰｒｅＡＤは、ノードｎＡＤのアクションが実行される前に満たされなければならない事前条件を示す。具体的には、ノードｎＡＤのＴｙｐｅＡＤが「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」である場合、かかるノードｎＡＤの事前条件ＰｒｅＡＤは、ノードｎＡＤと接続されており、かつ、ＴｙｐｅＡＤが「ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」であるノードｎＡＤによって表される。すなわち、２つのノードｎ１ＡＤおよびｎ２ＡＤにおいて、「Ｔｙｐｅ１ＡＤ  ＝  ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」、かつ、「Ｔｙｐｅ２ＡＤ  ＝  ｌｏｃａｌＰｒｅｃｏｎｄｉｔｉｏｎ」、かつ、「＜ｎ１ＡＤ、ｎ２ＡＤ、ＣｏｍｍｅｎｔＬｉｎｅ＞  ∈  ＴＡＤ」ならば、「Ｐｒｅ１ＡＤ  ＝  Ｎａｍｅ２ＡＤ」が成り立つ。
【００６７】
ＰｏｓｔＡＤは、ノードｎＡＤのアクションが実行された後の事後条件を示す。具体的には、ノードｎＡＤのＴｙｐｅＡＤが「ＥｘｅｃｕｔａｂｌｅＮｏｄｅ」である場合、かかるノードｎＡＤの事後条件ＰｏｓｔＡＤは、ノードｎＡＤと接続されており、かつ、ＴｙｐｅＡＤが「ｌｏｃａｌＰｏｓｔｃｏｎｄｉｔｉｏｎ」であるノードｎＡＤによって表される。
【００６８】
なお、アクティビティ定義ファイル１４３は、アクティビティ図ＡＤを表すＸＭＩ形式のファイルであるので、アクティビティ定義ファイル１４３についても、上記データ構造（３）〜（６）のように定義される。
【００６９】
続いて、ファカルティ図の論理的なデータ構造について説明する。ファカルティ図ＦＤの構成要素は、
ＦＤ＝（ＮＦＤ、ＴＦＤ）・・・（７）
というデータ構造によって定義される。
【００７０】
上記データ構造（７）において、ＮＦＤは、ファカルティ図ＦＤに記述されているノードｎＦＤの集合を示す。なお、ここでいう「ノードｎＦＤ」とは、ファカルティ図ＦＤに記載される実行主体、権限およびスキルを示す。ＴＦＤは、ノード集合ＮＦＤに含まれるノードｎＦＤ間の関係ｔＦＤの集合を示す。
【００７１】
また、ノードｎＦＤは、
ｎＦＤ＝＜ＮａｍｅＦＤ、ＴｙｐｅＦＤ＞・・・（８）
というデータ構造によって定義される。
【００７２】
上記データ構造（８）において、ＮａｍｅＦＤは、ノードｎＦＤで表される実行主体、権限またはスキルの名称を示す。ＴｙｐｅＦＤは、ノードｎＦＤのステレオタイプを示す。具体的には、ノードｎＦＤが実行主体である場合、ＴｙｐｅＦＤには「Ｒｏｌｅ」が設定され、ノードｎＦＤが権限である場合、ＴｙｐｅＦＤには「Ａｕｔｈｏｒｉｔｙ」、ノードｎＦＤがスキルである場合、ＴｙｐｅＦＤには「Ｓｋｉｌｌ」が設定される。
【００７３】
図４に示したファカルティ図の例では、ＮａｍｅＦＤが「Ｍａｎａｇｅｒ」であり、ＴｙｐｅＦＤが「Ｒｏｌｅ」であるノードｎ１ＦＤと、ＮａｍｅＦＤが「Ｇｒａｎｔ」であり、ＴｙｐｅＦＤが「Ａｕｔｈｏｒｉｔｙ」であるノードｎ２ＦＤとが定義される。また、所定の関係ｔ１ＦＤによって、ノードｎ１ＦＤとノードｎ２ＦＤとが関係していることが定義される。したがって、ノードｎ１ＦＤおよびｎ２ＦＤと、関係ｔ１ＦＤによって、実行主体「Ｍａｎａｇｅｒ」が権限「Ｇｒａｎｔ」を有していることを把握できる。
【００７４】
同様に、図４に示したファカルティ図の例では、ＮａｍｅＦＤが「Ｏｐｅｒａｔｏｒ」であり、ＴｙｐｅＦＤが「Ｒｏｌｅ」であるノードｎ３ＦＤと、ＮａｍｅＦＤが「Ｏｐｅｒａｔｅ  ｓｅｒｖｅｒ」であり、ＴｙｐｅＦＤが「Ｓｋｉｌｌ」であるノードｎ４ＦＤとが定義される。また、所定の関係ｔ２ＦＤによって、ノードｎ３ＦＤとノードｎ４ＦＤとが関係していることが定義される。したがって、ノードｎ３ＦＤおよびｎ４ＦＤと、関係ｔ２ＦＤによって、実行主体「Ｏｐｅｒａｔｏｒ」がスキル「Ｏｐｅｒａｔｅ  ｓｅｒｖｅｒ」を有していることを把握できる。
【００７５】
なお、ファカルティ定義ファイル１４４は、ファカルティ図ＦＤを表すＸＭＩ形式のファイルであるので、ファカルティ定義ファイル１４４についても、上記データ構造（７）および（８）のように定義される。
【００７６】
続いて、挙動モデル生成部１５２が生成する挙動モデルの論理的なデータ構造について説明する。挙動モデルＭＡＤは、
ＭＡＤ＝（Ｓ、ＳＩ、Ｒ、Ｌ）・・・（９）
によって定義される。
【００７７】
上記データ構図（９）において、Ｓは、アクティビティ図ＡＤにおいて到達可能な状態ｓの集合を示す。ここでいう「到達可能な状態」とは、アクティビティ図ＡＤにおいて、所定の手続きが実行される前の状態と、所定の手続きが実行されている状態と、所定の手続きが実行された後の状態とを示す。図３に示したアクティビティ図の例では、Ｓには、手続きＡ１〜Ａ８が実行される前の状態、手続きＡ１〜Ａ８が実行されている状態、手続きＡ１〜Ａ８が実行された後の状態が含まれる。
【００７８】
ＳＩは、状態集合Ｓに含まれる要素であり、アクティビティ図ＡＤにおける初期状態を示す。図３に示したアクティビティ図の例では、ＳＩは、手続きＡ１が実行される前の状態を示す。
【００７９】
Ｌは、状態ｓから、かかる状態ｓにおいて成立している事象を表す変数への写像を与えるための関数である。ここでいう「事象を表す変数」とは、例えば、以下の（Ａ）〜（Ｄ）に示すものが定義される。
【００８０】
（Ａ）ＩＮ（ｎ）
変数ＩＮ（ｎ）は、状態ｓにおいて、ノードｎＡＤにより表されるアクションが実行中である場合に、かかる実行の多重度を示す。例えば、状態ｓが実行中でない場合、ＩＮ（ｎ）＝０が成り立つ。
【００８１】
（Ｂ）ＯＮ（ｔ）
変数ＯＮ（ｔ）におけるｔは、
ｔ＝＜ｎ１ＡＤ、ｎ２ＡＤ、ＣｏｎｔｒｏｌＦｌｏｗ＞・・・（１０）
により定義される。
上記式（１０）において、ノードｎ１ＡＤは、状態ｓの直前のアクションを示し、ノードｎ２ＡＤは、状態ｓの直後のアクションを示す。そして、ＯＮ（ｔ）は、ノードｎ１ＡＤにより表されるアクションが終了し、かつ、ノードｎ２ＡＤにより表されるアクションが実行前である場合に、かかる実行の多重度を示す。
【００８２】
（Ｃ）Ｈａｓ＿ａｕｔｈｏｒｉｔｙ（ｘ、ｙ）・・・（１１）
上記式（１１）において、ｘは権限を示し、ｙは実行主体を示す。例えば、ファカルティ定義ファイル１４４に、実行主体ｙが権限ｘを有していることが記述されている場合、全ての状態ｓにおいて、Ｈａｓ＿ａｕｔｈｏｒｉｔｙ（ｘ、ｙ）＝１（真）が成立する。なお、実行主体ｙがスキルｘを有しているか否かの変数は、Ｈａｓ＿ｓｋｉｌｌ（ｘ、ｙ）によって表される。
【００８３】
（Ｄ）Ｆｉｎａｌ
Ｆｉｎａｌは、アクティビティ図ＡＤにおいて、ＦｉｎａｌＮｏｄｅにより表されているアクションまで到達し、アクティビティが終了したことを示す。具体的には、ＴｙｐｅＡＤ＝ＦｉｎａｌＮｏｄｅのとき、状態ｓ｜＝Ｉｎ（ｎＡＤ）ならば、状態ｓ｜＝Ｆｉｎａｌが成立する。
【００８４】
なお、上記（Ａ）〜（Ｄ）に示した変数は、あくまで一例であり、アクティビティ図ＡＤやミッション図ＭＤに記述される他の変数についても、各状態ｓにおける解釈を与えることができる。以下では、関数Ｌによって決定される状態ｓにおける変数ｖの値を表す関数を、ｆ（Ｌ（ｓ）、ｖ）と表すこととする。
【００８５】
Ｒは、所定の状態ｓ１から別の状態ｓ２へ遷移する条件を示す。以下に、状態ｓ１から状態ｓ２へ遷移する遷移条件Ｒについて、２つの例を示して説明する。まず、ノードｎ１ＡＤで表されるアクションが実行中である状態ｓ１から、かかるアクションが実行終了後の状態ｓ２へ遷移する遷移条件Ｒ１について説明する。遷移条件Ｒ１には、以下に示す条件Ｒ１−１〜Ｒ１−７が定義される。
【００８６】
（条件Ｒ１−１）
ｆ（Ｌ（ｓ１），ＩＮ（ｎ１ＡＤ））＞０が成立すること。
【００８７】
（条件Ｒ１−２）
ＴＯＵＴ＝｛ｔ２ＡＤ｜ｔ２ＡＤ＝＜ｎ１ＡＤ，Ｄｓｔ２ＡＤ，ＣｏｎｔｒｏｌＦｌｏｗ＞∈Ｔ｝が空でないこと。すなわち、ノードｎ１ＡＤを始点ノードとするＣｏｎｔｒｏｌＦｌｏｗが少なくとも１つ存在すること。
【００８８】
（条件Ｒ１−３）
ＴＯＵＴ＝｛ｄ１，ｄ２，・・・，ｄｍ｝のとき、Ｔｙｐｅ１ＡＤ≠ＦｏｒｋＮｏｄｅならば、所定の１つのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ２），ＯＮ（ｄｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｄｋ））＋１が成立し、ｋ≠ｌならば、ｆ（Ｌ（ｓ２），ＯＮ（ｄｌ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｄｌ））が成立すること。
【００８９】
（条件Ｒ１−４）
ＴＯＵＴ＝｛ｄ１，ｄ２，・・・，ｄｍ｝のとき、Ｔｙｐｅ１ＡＤ＝ＦｏｒｋＮｏｄｅならば、すべてのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ２），ＯＮ（ｄｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｄｋ））＋１が成立すること。
【００９０】
（条件Ｒ１−５）
ｆ（Ｌ（ｓ２），ＩＮ（ｎ１ＡＤ））＝ｆ（Ｌ（ｓ１），ＩＮ（ｎ１ＡＤ））−１が成立すること。
【００９１】
（条件Ｒ１−６）
所定の命題αについて、α∈Ｐｏｓｔ１ＡＤならば、ｆ（Ｌ（ｓ２），α）＝１（真）が成立し、¬α∈Ｐｏｓｔ１ＡＤならば、ｆ（Ｌ（ｓ２），α）＝０（偽）が成立すること。
【００９２】
（条件Ｒ１−７）
上記条件Ｒ１−１〜条件Ｒ１−６において、指定のない変数および命題ｘについては、ｆ（Ｌ（ｓ１），ｘ）＝ｆ（Ｌ（ｓ２），ｘ）が成立すること。
【００９３】
続いて、所定の状態ｓ１から、ノードｎ１ＡＤで表されるアクションが実行中である状態ｓ２へ遷移する遷移条件Ｒ２について説明する。遷移条件Ｒ２には、以下に示す条件Ｒ２−１〜Ｒ２−６が定義される。
【００９４】
（条件Ｒ２−１）
ＴＩＮ＝｛ｔ１ＡＤ｜ｔ１ＡＤ＝＜ｎ２ＡＤ，ｎ１ＡＤ，ＣｏｎｔｒｏｌＦｌｏｗ＞∈Ｔ｝が空でないこと。すなわち、ノードｎ２ＡＤを終点ノードとするＣｏｎｔｒｏｌＦｌｏｗが少なくとも１つ存在すること。
【００９５】
（条件Ｒ２−２）
ＴＩＮ＝｛ｅ１，ｅ２，・・・，ｅｍ｝のとき、Ｔｙｐｅ１ＡＤ≠ＦｏｒｋＮｏｄｅならば、所定の１つのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））＞０、かつ、ｆ（Ｌ（ｓ２），ＯＮ（ｅｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））−１が成立し、ｋ≠ｌならば、ｆ（Ｌ（ｓ２），ＯＮ（ｅｌ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｅｌ））が成立すること。
【００９６】
（条件Ｒ２−３）
ＴＩＮ＝｛ｅ１，ｅ２，・・・，ｅｍ｝のとき、Ｔｙｐｅ１ＡＤ＝ＦｏｒｋＮｏｄｅならば、すべてのｋ（１≦ｋ≦ｍ）について、ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））＞０、かつ、ｆ（Ｌ（ｓ２），ＯＮ（ｅｋ））＝ｆ（Ｌ（ｓ１），ＯＮ（ｅｋ））−１が成立すること。
【００９７】
（条件Ｒ２−４）
ｆ（Ｌ（ｓ２），ＩＮ（ｎ１ＡＤ））＝ｆ（Ｌ（ｓ１），ＩＮ（ｎ１ＡＤ））＋１が成立すること。
【００９８】
（条件Ｒ２−５）
所定の命題αについて、α∈Ｐｒｅ１ＡＤならば、ｆ（Ｌ（ｓ１），α）＝１（真）が成立し、¬α∈Ｐｒｅ１ＡＤならば、ｆ（Ｌ（ｓ１），α）＝０（偽）が成立すること。
【００９９】
（条件Ｒ２−６）
上記条件Ｒ２−１〜条件Ｒ２−６において、指定のない変数および命題ｘについては、ｆ（Ｌ（ｓ１），ｘ）＝ｆ（Ｌ（ｓ２），ｘ）が成立すること。
【０１００】
続いて、挙動モデル生成部１５２による挙動モデルファイル１６２の生成処理について説明する。挙動モデル生成部１５２は、アクティビティ定義ファイル１４３から、順序関係ＴＡＤを抽出する。続いて、挙動モデル生成部１５２は、抽出した順序関係ＴＡＤから各状態ｓ間の遷移関係を構築する。続いて、挙動モデル生成部１５２は、アクティビティ定義ファイル１４３から、各ノードｎＡＤの事前条件ＰｒｅＡＤと、事後状態ＰｏｓｔＡＤとを抽出する。続いて、挙動モデル生成部１５２は、事前条件ＰｒｅＡＤおよび事後状態ＰｏｓｔＡＤに基づいて、各状態ｓにおける真理値を割り当てて、挙動モデルファイル１６２を生成する。
【０１０１】
図７は、ＳＭＶ形式の挙動モデルファイル１６２の一例を示す図である。図７に示した挙動モデルファイル１６２において、「ｉｎ＿０＿１」は、図３に示した手続きＡ２が実行中であることを示しており、「ｏｎ＿６」は、手続きＡ２の直前のリンクまで実行が終了したことを示す。すなわち、図７に示した挙動モデルファイル１６２は、手続きＡ２が実行される状態に遷移するとき、「ｏｎ＿６」を「１」減算し、「ｉｎ＿０＿１」を「１」加算し、「Ｕｓｅｒ＿ｃｈｅｃｋｅｄ」の値を１（真）にすることを示している。
【０１０２】
次に、挙動モデル生成部１５２による初期状態組込処理について説明する。挙動モデル生成部１５２は、ファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ１ＦＤと、ＴｙｐｅＦＤが「Ａｕｔｈｏｒｉｔｙ」である権限のＮａｍｅ２ＦＤとの関係を抽出する。続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ１ＦＤが、抽出した権限Ｎａｍｅ２ＦＤを有することを示す自相論理式を生成する。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ａｕｔｏｒｉｔｙ（Ｎａｍｅ１ＦＤ、Ｎａｍｅ２ＦＤ）を生成する。
【０１０３】
続いて、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ３ＦＤと、ＴｙｐｅＦＤが「Ｓｋｉｌｌ」である権限のＮａｍｅ４ＦＤとの関係を抽出する。続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ３ＦＤが、抽出したスキルＮａｍｅ４ＦＤを有することを示す自相論理式を生成する。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ｓｋｉｌｌ（Ｎａｍｅ３ＦＤ、Ｎａｍｅ４ＦＤ）を生成する。
【０１０４】
図８は、挙動モデルファイル１６２に組み込む初期状態の一例を示す図である。例えば、図８中の定義８１は、「管理職は、承認権限を有している」ということを示している。挙動モデル生成部１５２は、このように定義される初期状態を、挙動モデルファイル１６２に組み込む。なお、挙動モデル生成部１５２は、初期状態を、挙動モデルファイル１６２に組み込まず、初期状態が定義されている別のファイルを生成してもよい。
【０１０５】
検査部１５３は、制約条件ファイル１６１と、挙動モデルファイル１６２とに基づいて、作業プロセスの整合性が満たされているか否かを検査する処理部である。具体的には、検査部１５３は、権限またはスキルを有する実行主体によって各手続きが実行されているか否か、制約条件ファイル１６１に定義されている制約条件を満たしつつ各手続きが実行されるか否か、制約条件ファイル１６１に定義されているゴール条件を満たすか否かを検査する。そして、検査部１５３は、作業プロセスの整合性が満たされていない場合に、判定結果ファイル１６３を生成する。なお、ＮｕＳＭＶは、判定結果ファイル１６３を生成する機能を有しており、かかる判定結果ファイル１６３は、テキスト形式のファイルである。
【０１０６】
反例生成部１５４は、検査部１５３によって生成されたテキスト形式の判定結果ファイル１６３から、ＸＭＩ形式の反例ファイル１６４を生成する処理部である。具体的には、反例生成部１５４は、整合性が満たされていない手続きを視覚的に把握できるように、ＸＭＩ形式の反例ファイル１６４を生成する。例えば、反例生成部１５４は、整合性が満たされていない原因となっている手続きの表示色を、他の手続きの表示色と変更するように、反例ファイル１６４を生成する。
【０１０７】
そして、反例生成部１５４は、生成した反例ファイル１６４を表示制御部１３３へ出力する。反例ファイル１６４を受け付けた表示制御部１３３は、表示部１２０にアクティビティ図を表示させる。ここで、図９−１〜図９−３を用いて、反例生成部１５４によって生成された反例ファイル１６４に基づいて、表示制御部１３３が表示部１２０に表示させるアクティビティ図の例について説明する。図９−１〜図９−３は、整合性検査後に表示される画面（以下、「整合性検査結果画面」という）の一例を示す図である。
【０１０８】
図９−１〜図９−３は、図３に示したアクティビティ図と比較して、手続きＡ３から手続きＡ４へのリンクが、手続きＡ３から手続きＡ５へのリンクに変更され、かつ、手続きＡ８が削除されたアクティビティ図に対する整合性検査結果画面を示している。ここでは、利用者によって入力されたミッション図は、図２に示したミッション図であり、利用者によって入力されたファカルティ図は、図４に示したファカルティ図であるものとする。
【０１０９】
かかる場合、制約条件ファイル生成部１５１は、図６に示した条件Ｐ１〜Ｐ７を含む制約条件ファイル１６１を生成し、検査部１５３は、条件Ｐ４、Ｐ６およびＰ７に対する違反を検出する。このうち、図９−１に例示した整合性検査結果画面は、条件Ｐ４に対する違反を検出したことが視覚的に把握できるように表示されている。具体的には、図９−１に例示した整合性検査結果画面は、手続きＡ４の表示色を変更することで、手続きＡ４を経由せずに、作業プロセスが実行される可能性があることが把握できるように表示されている。すなわち、図９−１に例示した整合性検査結果画面によれば、ミッション図におけるサブ目標「Ｐ００１−０２：承認を得る」が達成されずに作業プロセスが終了する可能性があることを把握できる。
【０１１０】
また、図９−２に例示した整合性検査結果画面は、条件Ｐ６に対する違反を検出したことが視覚的に把握できるように表示されている。具体的には、図９−２に例示した整合性検査結果画面は、手続きＡ４および手続きＡ７の表示色を変更することで、手続きＡ４を経由しなければ、「サーバ増設時に承認を得ていること」という制約条件に違反することが把握できるように表示されている。
【０１１１】
また、図９−３に例示した整合性検査結果画面は、条件Ｐ７に対する違反を検出したことが視覚的に把握できるように表示されている。具体的には、図９−３に例示した整合性検査結果画面は、手続きＡ３の表示色を変更することで、管理サーバにログインした状態のままで、作業プロセスが終了することが把握できるように表示されている。
【０１１２】
なお、図９−１〜図９−３に示した整合性検査結果画面は、あくまで一例であり、反例生成部１５４は、他の整合性検査結果画面が表示されるように反例ファイル１６４を生成してもよい。例えば、反例生成部１５４は、整合性が満たされない原因となっている手続き近傍に、かかる原因が文字列によって表示されるように反例ファイル１６４を生成してもよい。
【０１１３】
検査結果ファイル格納部１６０は、検査結果に関する各種ファイルが格納される記憶デバイスであり、制約条件ファイル１６１と、挙動モデルファイル１６２と、判定結果ファイル１６３と、反例ファイル１６４とが格納される。
【０１１４】
次に、本実施例に係る検査用ファイル生成装置１００による整合性検査処理の手順について説明する。図１０は、検査用ファイル生成装置１００による整合性検査処理手順を示すフローチャートである。図１０に示すように、検査用ファイル生成装置１００の受付部１３１は、ミッション図、アクティビティ図またはファカルティ図を作成または編集するための情報を受け付ける（ステップＳ１０１）。
【０１１５】
続いて、受付部１３１によって作業プロセスの整合性検査を開始する旨の操作指示が受け付けられた場合（ステップＳ１０２肯定）、定義ファイル生成部１３２は、各種定義ファイルを生成する（ステップＳ１０３）。具体的には、定義ファイル生成部１３２は、ミッション図を作成するために入力された情報に基づいて、ミッション定義ファイル１４２を生成する。また、定義ファイル生成部１３２は、アクティビティ図を作成するために入力された情報に基づいて、アクティビティ定義ファイル１４３を生成する。また、定義ファイル生成部１３２は、ファカルティ図を作成するために入力された情報に基づいて、ファカルティ定義ファイル１４４を生成する。
【０１１６】
続いて、表示制御部１３３は、定義ファイル生成部１３２によってアクティビティ定義ファイル１４３が生成されなかった場合（ステップＳ１０４否定）、表示部１２０に、アクティビティ図を作成する旨のエラーを表示させる（ステップＳ１０５）。
【０１１７】
一方、定義ファイル生成部１３２によってアクティビティ定義ファイル１４３が生成された場合（ステップＳ１０４肯定）、挙動モデル生成部１５２は、アクティビティ定義ファイル１４３に基づいて、挙動モデルファイル１６２を生成する挙動モデル生成処理を行う（ステップＳ１０６）。なお、挙動モデル生成部１５２による挙動モデル生成処理については、後に詳述する。
【０１１８】
続いて、定義ファイル生成部１３２によってファカルティ定義ファイル１４４が生成された場合（ステップＳ１０７肯定）、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４に基づいて、挙動モデルファイル１６２に初期状態を組み込む初期状態組込処理を行う（ステップＳ１０８）。一方、定義ファイル生成部１３２によってファカルティ定義ファイル１４４が生成されなかった場合（ステップＳ１０７否定）、挙動モデル生成部１５２は、初期状態組込処理を行わない。なお、挙動モデル生成部１５２による初期状態組込処理については、後に詳述する。
【０１１９】
続いて、定義ファイル生成部１３２によってミッション定義ファイル１４２が生成された場合（ステップＳ１０９肯定）、制約条件ファイル生成部１５１は、共通定義ファイル１４１と、ミッション定義ファイル１４２とに基づいて、制約条件ファイル１６１を生成する制約条件ファイル生成処理を行う（ステップＳ１１０）。なお、制約条件ファイル生成部１５１による制約条件ファイル生成処理については、後に詳述する。
【０１２０】
一方、定義ファイル生成部１３２によってミッション定義ファイル１４２が生成されなかった場合（ステップＳ１０９否定）、制約条件ファイル生成部１５１は、共通定義ファイル１４１に基づいて、制約条件ファイル１６１を生成する（ステップＳ１１１）。
【０１２１】
続いて、検査部１５３は、制約条件ファイル１６１と、挙動モデルファイル１６２とに基づいて、作業プロセスの整合性が満たされているか否かを検査する（ステップＳ１１２）。作業プロセスの整合性が満たされている場合（ステップＳ１１３肯定）、検査部１５３は、処理を終了する。このとき、表示制御部１３３は、表示部１２０に、作業プロセスの整合性が満たされている旨を表示させてもよい。
【０１２２】
一方、作業プロセスの整合性が満たされていない場合（ステップＳ１１３否定）、検査部１５３は、判定結果ファイル１６３を生成する（ステップＳ１１４）。続いて、反例生成部１５４は、検査部１５３によって生成された判定結果ファイル１６３から、反例ファイル１６４を生成する（ステップＳ１１５）。そして、表示制御部１３３は、反例生成部１５４によって生成された反例ファイル１６４に基づいて、表示部１２０に、整合性検査結果画面を表示させる（ステップＳ１１６）。
【０１２３】
次に、挙動モデル生成部１５２による挙動モデル生成処理の手順について説明する。図１１は、挙動モデル生成部１５２による挙動モデル生成処理手順を示すフローチャートである。図１１に示すように、挙動モデル生成部１５２は、論理的なデータ構造に定義できるアクティビティ定義ファイル１４３から、順序関係ＴＡＤを抽出する（ステップＳ２０１）。
【０１２４】
続いて、挙動モデル生成部１５２は、抽出した順序関係ＴＡＤから各状態ｓ間の遷移関係を構築する（ステップＳ２０２）。続いて、挙動モデル生成部１５２は、アクティビティ定義ファイル１４３から、各ノードｎＡＤの事前条件ＰｒｅＡＤと、事後状態ＰｏｓｔＡＤとを抽出する（ステップＳ２０３）。
【０１２５】
続いて、挙動モデル生成部１５２は、事前条件ＰｒｅＡＤおよび事後状態ＰｏｓｔＡＤに基づいて、各状態ｓにおける真理値を割り当てて（ステップＳ２０４）、挙動モデルファイル１６２を生成する（ステップＳ２０５）。
【０１２６】
次に、挙動モデル生成部１５２による初期状態組込処理の手順について説明する。図１２は、挙動モデル生成部１５２による初期状態組込処理手順を示すフローチャートである。図１２に示すように、挙動モデル生成部１５２は、論理的なデータ構造に定義できるファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ１ＦＤと、ＴｙｐｅＦＤが「Ａｕｔｈｏｒｉｔｙ」である権限のＮａｍｅ２ＦＤとの関係を抽出する（ステップＳ３０１）。
【０１２７】
続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ１ＦＤが、抽出した権限Ｎａｍｅ２ＦＤを有することを示す自相論理式を生成する（ステップＳ３０２）。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ａｕｔｏｒｉｔｙ（Ｎａｍｅ１ＦＤ、Ｎａｍｅ２ＦＤ）を生成する。
【０１２８】
続いて、挙動モデル生成部１５２は、ファカルティ定義ファイル１４４の関係ＴＦＤに基づいて、ＴｙｐｅＦＤが「Ｒｏｌｅ」である実行主体のＮａｍｅ３ＦＤと、ＴｙｐｅＦＤが「Ｓｋｉｌｌ」である権限のＮａｍｅ４ＦＤとの関係を抽出する（ステップＳ３０３）。続いて、挙動モデル生成部１５２は、抽出した実行主体Ｎａｍｅ３ＦＤが、抽出したスキルＮａｍｅ４ＦＤを有することを示す自相論理式を生成する（ステップＳ３０４）。具体的には、挙動モデル生成部１５２は、自相論理式として、Ｈａｓ＿ｓｋｉｌｌ（Ｎａｍｅ３ＦＤ、Ｎａｍｅ４ＦＤ）を生成する。
【０１２９】
そして、挙動モデル生成部１５２は、上記ステップＳ３０２およびＳ３０４において生成した自相論理式を初期状態として、挙動モデルファイル１６２に組み込む（ステップＳ３０５）。
【０１３０】
次に、制約条件ファイル生成部１５１による制約条件ファイル生成処理の手順について説明する。図１３は、制約条件ファイル生成部１５１による制約条件ファイル生成処理手順を示すフローチャートである。図１３に示すように、制約条件ファイル生成部１５１は、論理的なデータ構造に定義できるミッション定義ファイル１４２のノード集合ＮＭＤから、ゴール条件や制約条件を示すＣｏｎｔＭＤを抽出する（ステップＳ４０１）。
【０１３１】
続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｃｏｎｓｔｒａｉｎｔ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行されている間、常に満たしていなければならない制約条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（ＣｏｎｔＭＤ）を生成する（ステップＳ４０２）。
【０１３２】
続いて、制約条件ファイル生成部１５１は、抽出したＣｏｎｔＭＤのうち、ＴｙｐｅＭＤが「Ｇｏａｌ」であるＣｏｎｔＭＤに基づいて、ノードｎＭＤが実行された後に満たさなければならないゴール条件を示すＣＴＬ式を生成する。具体的には、制約条件ファイル生成部１５１は、ＣＴＬ式として、ＡＧ（Ｆｉｎａｌ→ＣｏｎｔＭＤ）を生成する（ステップＳ４０３）。
【０１３３】
そして、制約条件ファイル生成部１５１は、ＣＴＬ式により表されたゴール条件および制約条件が記述された制約条件ファイル１６１を生成する（ステップＳ４０４）。
【０１３４】
上述してきたように、本実施例に係る検査用ファイル生成装置１００は、目標が定義されるミッション図と、各種手続きが定義されるアクティビティ図と、実行主体が有する権限が定義されるファカルティ図とを図形入力により受け付け、かかるミッション図、アクティビティ図およびファカルティ図に基づいて、各種定義ファイルを生成し、生成した定義ファイルに基づいて、挙動モデルを示す挙動モデルファイル１６２を生成するので、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成することができる。
【０１３５】
また、本実施例に係る検査用ファイル生成装置１００は、生成した挙動モデルファイル１６２を用いて、作業プロセスの整合性を検査するので、複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うことができる。
【０１３６】
なお、上記実施例では、検査用ファイル生成装置１００が、挙動モデルファイル１６２を生成して、生成した挙動モデルファイル１６２に基づいて作業プロセスの整合性を検査する例について説明したが、検査用ファイル生成装置１００は、挙動モデルファイル１６２の生成処理までを行い、作業プロセスの整合性検査処理については、他の情報処理装置を行ってもよい。
【０１３７】
また、図１に示した検査用ファイル生成装置１００の構成は、要旨を逸脱しない範囲で種々に変更することができる。例えば、検査用ファイル生成装置１００の定義ファイル出力制御部１３０および検査制御部１５０の機能をソフトウェアとして実装し、これをコンピュータで実行することにより、検査用ファイル生成装置１００と同等の機能を実現することもできる。以下に、定義ファイル出力制御部１３０および検査制御部１５０の機能をソフトウェアとして実装した作業プロセス検査プログラム１０７１を実行するコンピュータの一例を示す。
【０１３８】
図１４は、作業プロセス検査プログラム１０７１を実行するコンピュータ１０００を示す機能ブロック図である。このコンピュータ１０００は、各種演算処理を実行するＣＰＵ（Central  Processing  Unit）１０１０と、ユーザからのデータの入力を受け付ける入力装置１０２０と、各種情報を表示するモニタ１０３０と、記録媒体からプログラム等を読み取る媒体読取り装置１０４０と、ネットワークを介して他のコンピュータとの間でデータの授受を行うネットワークインターフェース装置１０５０と、各種情報を一時記憶するＲＡＭ（Random  Access  Memory）１０６０と、ハードディスク装置１０７０とをバス１０８０で接続して構成される。
【０１３９】
そして、ハードディスク装置１０７０には、図１に示した定義ファイル出力制御部１３０および検査制御部１５０と同様の機能を有する作業プロセス検査プログラム１０７１と、図１に示した定義ファイル格納部１４０に記憶される各種データに対応する定義ファイル１０７２と、図１に示した検査結果ファイル格納部１６０に記憶される各種データに対応する検査用データ１０７３とが記憶される。なお、定義ファイル１０７２または検査用データ１０７３を、適宜分散させ、ネットワークを介して接続された他のコンピュータに記憶させておくこともできる。
【０１４０】
そして、ＣＰＵ１０１０が作業プロセス検査プログラム１０７１をハードディスク装置１０７０から読み出してＲＡＭ１０６０に展開することにより、作業プロセス検査プログラム１０７１は、作業プロセス検査プロセス１０６１として機能するようになる。そして、作業プロセス検査プロセス１０６１は、定義ファイル１０７２および検査用データ１０７３から読み出した情報等を適宜ＲＡＭ１０６０上の自身に割り当てられた領域に展開し、この展開したデータ等に基づいて各種データ処理を実行する。
【０１４１】
なお、上記の作業プロセス検査プログラム１０７１は、必ずしもハードディスク装置１０７０に格納されている必要はなく、ＣＤ−ＲＯＭ等の記憶媒体に記憶されたこのプログラムを、コンピュータ１０００が読み出して実行するようにしてもよい。また、公衆回線、インターネット、ＬＡＮ（Local  Area  Network）、ＷＡＮ（Wide  Area  Network）等を介してコンピュータ１０００に接続される他のコンピュータ（またはサーバ）等にこのプログラムを記憶させておき、コンピュータ１０００がこれらからプログラムを読み出して実行するようにしてもよい。
【符号の説明】
【０１４２】
１００  検査用ファイル生成装置
１１０  入力部
１２０  表示部
１３０  定義ファイル出力制御部
１３１  受付部
１３２  定義ファイル生成部
１３３  表示制御部
１４０  定義ファイル格納部
１４１  共通定義ファイル
１４２  ミッション定義ファイル
１４３  アクティビティ定義ファイル
１４４  ファカルティ定義ファイル
１５０  検査制御部
１５１  制約条件ファイル生成部
１５２  挙動モデル生成部
１５３  検査部
１５４  反例生成部
１６０  検査結果ファイル格納部
１６１  制約条件ファイル
１６２  挙動モデルファイル
１６３  判定結果ファイル
１６４  反例ファイル
１０００  コンピュータ
１０１０  ＣＰＵ
１０２０  入力装置
１０３０  モニタ
１０４０  媒体読取り装置
１０５０  ネットワークインターフェース装置
１０６０  ＲＡＭ
１０６１  作業プロセス検査プロセス
１０７０  ハードディスク装置
１０７１  作業プロセス検査プログラム
１０７２  定義ファイル
１０７３  検査用データ
１０８０  バス
【手続補正２】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成プログラムであって、
前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手順と、
前記受付手順によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手順と、
前記定義ファイル生成手順によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手順と
をコンピュータに実行させることを特徴とする検査用ファイル生成プログラム。
【請求項２】
前記受付手順は、前記各種定義情報として、該各種定義情報が図形および文字列により表された図である定義図を受け付け、
前記定義ファイル生成手順は、前記受付手順によって受け付けられた定義図に基づいて、定義ファイルを生成することを特徴とする請求項１に記載の検査用ファイル生成プログラム。
【請求項３】
前記受付手順は、前記定義図として、前記最終目標、前記サブ目標および前記制約条件が定義された定義図であるミッション図と、前記各種手続き、前記実行順序および前記実行主体が定義された定義図であるアクティビティ図と、前記実行主体が有する権限が定義された定義図であるファカルティ図とを受け付けることを特徴とする請求項２に記載の検査用ファイル生成プログラム。
【請求項４】
前記受付手順は、ＵＭＬ（Unified  Modeling  Language）の記法に則って記述された定義図を受け付けることを特徴とする請求項２または３に記載の検査用ファイル生成プログラム。
【請求項５】
前記挙動モデル生成手順によって生成された挙動モデルに基づいて、前記作業プロセスの整合性が満たされているか否かを検査する検査手順と、
前記検査手順によって前記作業プロセスが整合性を満たさないと判定された場合に、整合性を満たさない原因となっている手続きを識別できるように所定の表示部に表示させる表示制御手順をさらにコンピュータに実行させることを特徴とする請求項１〜３のいずれか一つに記載の検査用ファイル生成プログラム。
【請求項６】
作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成装置であって、
前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手段と、
前記受付手段によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手段と、
前記定義ファイル生成手段によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手段と
を備えたことを特徴とする検査用ファイル生成装置。
【請求項７】
作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成装置における検査用ファイル生成方法であって、
前記検査用ファイル生成装置が、
前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付工程と、
前記受付工程によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成工程と、
前記定義ファイル生成工程によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成工程と
を含んだことを特徴とする検査用ファイル生成方法。
【国際調査報告】
2009144826.tif 000019
2009144826.tif 000020