WO2009144826A1

WO2009144826A1 - 検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法

Info

Publication number: WO2009144826A1
Application number: PCT/JP2008/060071
Authority: WO
Inventors: 菊池　慎司
Original assignee: Fujitsu Ltd
Current assignee: Fujitsu Ltd
Priority date: 2008-05-30
Filing date: 2008-05-30
Publication date: 2009-12-03
Anticipated expiration: 2010-11-30
Also published as: GB201020003D0; US20110066889A1; US8103914B2; JP5246258B2; JPWO2009144826A1; GB2472944A

Abstract

　複数のＵＭＬ図で記述された作業プロセスに対して網羅的に整合性検査を行うための検査用ファイルを生成することを目的とする。目標が定義されるミッション図と、各種手続きが定義されるアクティビティ図と、実行主体が有する権限が定義されるファカルティ図とを図形入力により受け付け、かかるミッション図、アクティビティ図およびファカルティ図に基づいて、各種定義ファイルを生成し、生成した定義ファイルに基づいて、挙動モデルを示す挙動モデルファイル（１６２）を生成する。

Description

検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法

　本発明は、検査用ファイル生成プログラム、検査用ファイル生成装置および検査用ファイル生成方法に関する。

　従来、システム管理者等が情報システムに対して作業（以下、「作業プロセス」という）を行う場合、自然言語によって記述された運用マニュアルを用いることが一般的である。例えば、サーバにパッチを適用する作業プロセスは、かかる作業の手順や規則が記述された運用マニュアルを用いて行われる。

　ところで、近年、情報システムは大規模化、複雑化しているため、作業プロセスに求められる手順や規則も複雑化している。このことは、人手で作業プロセスの妥当性を検討することを困難にさせており、障害が発生する原因になっている。また、大規模化、複雑化している情報システムにおいては、少数の人間が断片的な知識を有している場合が多い。知識が細分化されていることは、情報システムの挙動の把握を困難にするため、障害が多発する原因になっている。情報システムは、生活インフラを支えるシステムとして重要性が非常に高まっており、情報システム運用管理上の信頼性を向上させることが強く望まれている。

　そこで、近年では、作業プロセスの妥当性を機械的に検査する技術が提案されている。例えば、ＵＭＬ（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）等を介してコンピュータ１０００に接続される他のコンピュータ（またはサーバ）等にこのプログラムを記憶させておき、コンピュータ１０００がこれらからプログラムを読み出して実行するようにしてもよい。

Claims

　作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成プログラムであって、
　前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手順と、
　前記受付手順によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手順と、
　前記定義ファイル生成手順によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手順と
　をコンピュータに実行させることを特徴とする検査用ファイル生成プログラム。
　前記受付手順は、前記各種定義情報として、該各種定義情報が図形および文字列により表された図である定義図を受け付け、
　前記定義ファイル生成手順は、前記受付手順によって受け付けられた定義図に基づいて、定義ファイルを生成することを特徴とする請求項１に記載の検査用ファイル生成プログラム。
　前記受付手順は、前記定義図として、前記最終目標、前記サブ目標および前記制約条件が定義された定義図であるミッション図と、前記各種手続き、前記実行順序および前記実行主体が定義された定義図であるアクティビティ図と、前記実行主体が有する権限が定義された定義図であるファカルティ図とを受け付けることを特徴とする請求項２に記載の検査用ファイル生成プログラム。
　前記受付手順は、ＵＭＬ（Unified　Modeling　Language）の記法に則って記述された定義図を受け付けることを特徴とする請求項２または３に記載の検査用ファイル生成プログラム。
　前記挙動モデル生成手順によって生成された挙動モデルに基づいて、前記作業プロセスの整合性が満たされているか否かを検査する検査手順をさらにコンピュータに実行させることを特徴とする請求項１～３のいずれか一つに記載の検査用ファイル生成プログラム。
　前記検査手順は、前記各種手続きが実行される際に前記サブ目標が達成されるか否か、前記各種手続きが実行される際に前記制約条件が遵守されるか否か、前記各種手続きが前記権限を有する主体によって実行されるか否か、前記最終目標が達成されるか否かを検査することを特徴とする請求項５に記載の検査用ファイル生成プログラム。
　前記検査手順によって前記作業プロセスが整合性を満たさないと判定された場合に、整合性を満たさない原因となっている手続きを識別できるように所定の表示部に表示させる表示制御手順をさらにコンピュータに実行させることを特徴とする請求項５に記載の検査用ファイル生成プログラム。
　作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成装置であって、
　前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付手段と、
　前記受付手段によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成手段と、
　前記定義ファイル生成手段によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成手段と
　を備えたことを特徴とする検査用ファイル生成装置。
　前記受付手段は、前記各種定義情報として、該各種定義情報が図形および文字列により表された図である定義図を受け付け、
　前記定義ファイル生成手段は、前記受付手段によって受け付けられた定義図に基づいて、定義ファイルを生成することを特徴とする請求項８に記載の検査用ファイル生成装置。
　前記受付手段は、前記定義図として、前記最終目標、前記サブ目標および前記制約条件が定義された定義図であるミッション図と、前記各種手続き、前記実行順序および前記実行主体が定義された定義図であるアクティビティ図と、前記実行主体が有する権限が定義された定義図であるファカルティ図とを受け付けることを特徴とする請求項９に記載の検査用ファイル生成装置。
　前記受付手段は、ＵＭＬ（Unified　Modeling　Language）の記法に則って記述された定義図を受け付けることを特徴とする請求項９または１０に記載の検査用ファイル生成装置。
　前記挙動モデル生成手段によって生成された挙動モデルに基づいて、前記作業プロセスの整合性が満たされているか否かを検査する検査手段をさらに備えたことを特徴とする請求項８～１０のいずれか一つに記載の検査用ファイル生成装置。
　前記検査手段は、前記各種手続きが実行される際に前記サブ目標が達成されるか否か、前記各種手続きが実行される際に前記制約条件が遵守されるか否か、前記各種手続きが前記権限を有する主体によって実行されるか否か、前記最終目標が達成されるか否かを検査することを特徴とする請求項１２に記載の検査用ファイル生成装置。
　前記検査手段によって前記作業プロセスが整合性を満たさないと判定された場合に、整合性を満たさない原因となっている手続きを識別できるように所定の表示部に表示させる表示制御手段をさらに備えたことを特徴とする請求項１２に記載の検査用ファイル生成装置。
　作業プロセスの整合性を検査するための検査用ファイルを生成する検査用ファイル生成装置における検査用ファイル生成方法であって、
　前記検査用ファイル生成装置が、
　前記作業プロセスに含まれる各種手続きと、前記各種手続きの実行順序と、前記作業プロセスにおいて最終的に達成される目標である最終目標と、前記各種手続きにおいて達成される目標であるサブ目標と、前記各種手続きが実行される際に遵守されるべき制約条件と、前記各種手続きを実行する実行主体と、前記実行主体が実行できる手続きを判別するための権限とに関する各種定義情報を受け付ける受付工程と、
　前記受付工程によって受け付けられた各種定義情報に基づいて、定義ファイルを生成する定義ファイル生成工程と、
　前記定義ファイル生成工程によって生成された定義ファイルに基づいて、前記作業プロセスを実行する場合における挙動モデルを示す検査用ファイルを生成する挙動モデル生成工程と
　を含んだことを特徴とする検査用ファイル生成方法。