(57)【要約】【課題】処理フローが表現している処理の流れが、業務要件を満たしているか否かを検査できる設計支援装置、プログラム、および設計支援方法を提供する【解決手段】本発明の設計支援装置は、ジョブの実行順序を記述した処理フロー１１１の検査を行うための設計支援装置１００であって、処理フロー１１１の設計情報に基づいて、処理フロー１１１を検査するための検査用モデル１２０を生成する検査用モデル生成部１０１と、検査用モデル１２０と該検査用モデル１２０が満たすべき性質の検査性質１２５の情報である検査性質情報とを入力とし、検査用モデル１２０が検査性質１２５を満たすかを検査した結果を出力するモデル検査部１０２とを備えている。【選択図】図１
2010198240.tif 000002
【特許請求の範囲】
【請求項１】
ジョブの実行順序を記述した処理フローの検査を行うための設計支援装置であって、
前記処理フローの設計情報に基づいて、前記処理フローを検査するための検査用モデルを生成する検査用モデル生成部と、
前記検査用モデルと該検査用モデルが満たすべき性質の検査性質の情報である検査性質情報とを入力とし、前記検査用モデルが前記検査性質を満たすか検査した結果を出力するモデル検査部とを
備えることを特徴とする設計支援装置。
【請求項２】
請求項１記載の設計支援装置において、
前記処理フローの設計情報は、前記処理フローが動作する問題領域を定義する情報と、前記処理フローを定義する情報とを有する
ことを特徴とする設計支援装置。
【請求項３】
請求項２記載の設計支援装置において、
前記処理フローが動作する問題領域を定義する情報は、
前記処理フローが動作する問題領域に存在するリソースであって前記処理フローを構成する前記ジョブの作用の対象である前記リソースを特定するリソース構造情報と、前記リソース構造情報に記述された前記各リソースが従う状態遷移を記述したリソース状態遷移情報とを有し、
前記処理フローを定義する情報は、
前記処理フローの情報と、前記処理フローを構成する前記ジョブの実行時の作用の結果として起こる前記リソースの状態遷移を記述したジョブ作用情報と、前記処理フローが実行を開始する時点での前記各リソースの状態を定義した処理フロー事前条件情報とを有する
ことを特徴とする設計支援装置。
【請求項４】
請求項３記載の設計支援装置において、
前記検査用モデル生成部は、前記検査用モデルに加えて、前記検査用モデルの構成要素を、前記ジョブまたは前記リソースに関連付けるモデル関連情報を生成し、
かつ、
前記処理フローが満たすべき性質の情報と前記モデル関連情報とに基づいて、前記検査性質情報を生成する検査性質生成部を備える
ことを特徴とする設計支援装置。
【請求項５】
請求項４記載の設計支援装置において、
前記モデル検査部は、前記検査用モデルが前記検査性質を満たさない場合に、該検査性質を満たさない反例情報を検査結果の一部として出力し、
かつ、
前記反例情報から、前記モデル関連情報に基づいて、前記処理フローの実行時に起こり得る状態である処理フロー状態を生成する処理フロー状態抽出部を備える
ことを特徴とする設計支援装置。
【請求項６】
請求項３記載の設計支援装置において、
前記ジョブの状態に関する命題と前記リソースの状態に関する命題とを組み合わせて表現した前記処理フローが満たすべき性質の情報が入力される入力部と、前記性質の情報を前記検査性質生成部の入力となる形式に変換する変換部とを有する業務要件記述支援部を備える
ことを特徴とする設計支援装置。
【請求項７】
請求項５記載の設計支援装置において、
前記モデル検査部は、複数のモデル検査エンジンを有し、
前記設計支援装置は、前記各モデル検査エンジンに対応した検査用モデル生成方法情報と検査性質生成方法情報と処理フロー状態抽出方法情報とを有するとともに、前記複数のモデル検査エンジンから前記モデル検査部が使用すべきモデル検査エンジンを選択する選択部を備え、
前記検査用モデル生成部は、前記選択部で選択されたモデル検査エンジンに対応する前記検査用モデル生成方法情報に基づいて前記検査用モデルを生成し、
前記検査性質生成部は、前記選択されたモデル検査エンジンに対応する前記検査性質生成方法情報に基づいて前記検査性質を生成し、
前記モデル検査部は、前記選択されたモデル検査エンジンを用いて前記検査用モデルの検査を行い、
前記処理フロー状態抽出部は、前記選択されたモデル検査エンジンに対応する前記処理フロー状態抽出方法情報に基づいて前記処理フロー状態を抽出する
ことを特徴とする設計支援装置。
【請求項８】
ジョブの実行順序を記述した処理フローの検査を行うためのプログラムであって、
コンピュータを、
前記処理フローの設計情報に基づいて、前記処理フローを検査するための検査用モデルを生成する検査用モデル生成部、
前記検査用モデルと該検査用モデルが満たすべき性質の検査性質の情報である検査性質情報とを入力とし、前記検査用モデルが前記検査性質を満たすか検査した結果を出力するモデル検査部、
として機能させるためのプログラム。
【請求項９】
請求項８記載のプログラムにおいて、
前記処理フローの設計情報は、前記処理フローが動作する問題領域を定義する情報と、前記処理フローを定義する情報とを有する
ことを特徴とするプログラム。
【請求項１０】
請求項９記載のプログラムにおいて、
前記処理フローが動作する問題領域を定義する情報は、
前記処理フローが動作する問題領域に存在するリソースであって前記処理フローを構成する前記ジョブの作用の対象である前記リソースを特定するリソース構造情報と、前記リソース構造情報に記述された前記各リソースが従う状態遷移を記述したリソース状態遷移情報とを有し、
前記処理フローを定義する情報は、
前記処理フローの情報と、前記処理フローを構成する前記ジョブの実行時の作用の結果として起こる前記リソースの状態遷移を記述したジョブ作用情報と、前記処理フローが実行を開始する時点での前記各リソースの状態を定義した処理フロー事前条件情報とを有する
ことを特徴とするプログラム。
【請求項１１】
請求項１０記載のプログラムにおいて、
前記検査用モデル生成部は、前記検査用モデルに加えて、前記検査用モデルの構成要素を、ジョブまたはリソースに関連付けるモデル関連情報を生成し、
コンピュータを、
前記処理フローが満たすべき性質の情報と前記モデル関連情報とに基づいて、前記検査性質情報を生成する検査性質生成部として機能させる
ことを特徴とするプログラム。
【請求項１２】
請求項１１記載のプログラムにおいて、
前記モデル検査部は、前記検査用モデルが前記検査性質を満たさない場合に、該検査性質を満たさない反例情報を検査結果の一部として出力し、
コンピュータを、
前記反例情報から、前記モデル関連情報に基づいて、前記処理フローの実行時に起こり得る状態である処理フロー状態を生成する処理フロー状態抽出部として機能させる
ことを特徴とするプログラム。
【請求項１３】
請求項１０記載のプログラムにおいて、
コンピュータを、
前記ジョブの状態に関する命題とリソースの状態に関する命題とを組み合わせて表現した前記処理フローが満たすべき性質の情報が入力される入力部と、前記性質の情報を前記検査性質生成部の入力となる形式に変換する変換部とを有する業務要件記述支援部として機能させる
ことを特徴とするプログラム。
【請求項１４】
請求項１２記載のプログラムにおいて、
前記モデル検査部は、複数のモデル検査エンジンを有し、
コンピュータを、
前記複数のモデル検査エンジンから前記モデル検査部が使用すべきモデル検査エンジンを選択する選択部として機能させ、
前記検査用モデル生成部は、前記選択部で選択されたモデル検査エンジンに対応する検査用モデル生成方法情報に基づいて前記検査用モデルを生成し、
前記検査性質生成部は、前記選択されたモデル検査エンジンに対応する検査性質生成方法情報に基づいて前記検査性質を生成し、
前記モデル検査部は、前記選択されたモデル検査エンジンを用いて前記検査用モデルの検査を行い、
前記処理フロー状態抽出部は、前記選択されたモデル検査エンジンに対応する処理フロー状態抽出方法情報に基づいて前記処理フロー状態を抽出する
ことを特徴とするプログラム。
【請求項１５】
ジョブの実行順序を記述した処理フローの検査をコンピュータが行うための設計支援方法であって、
前記処理フローの情報と、
前記処理フローが動作する問題領域に存在するリソースであって前記処理フローを構成する前記ジョブの作用の対象である前記リソースを特定するリソース構造情報と、
前記リソース構造情報に記述された前記各リソースが従う状態遷移を記述したリソース状態遷移情報と、
前記処理フローを構成する前記ジョブの実行時の作用であって当該ジョブの実行の結果として起こる前記リソースの状態遷移を記述したジョブ作用情報と、
前記処理フローが実行を開始する時点での前記各リソースの状態を定義した処理フロー事前条件情報とに基づいて、
前記処理フローの構成要素である前記ジョブの振る舞いと前記リソース構造情報の構成要素である前記リソースの振る舞いを記述した検査用モデルを生成し、さらに、前記検査用モデルの構成要素を、前記ジョブまたは前記リソースに関連付けるモデル関連情報を生成する検査用モデル生成ステップと、
前記処理フローが満たすべき性質の情報と前記モデル関連情報に基づいて、前記検査用モデルが満たすべき検査性質の情報を生成する検査性質生成ステップと、
前記検査用モデルが前記検査性質を満たすかを検査し、満たしていない場合は、該満たしていない反例情報を生成するモデル検査ステップと、
前記反例情報から、前記モデル関連情報に基づいて、前記処理フローを構成する前記ジョブと前記リソース構造を構成する前記リソースのそれぞれの前記処理フロー実行時に起こり得る処理フロー状態を生成する処理フロー状態抽出ステップと、
を含むことを特徴とする設計支援方法。
【請求項１６】
請求項１５記載の設計支援方法であって、
前記モデル検査ステップにおいて使用すべきモデル検査エンジンが複数のモデル検査エンジンの中から選択されるステップを含み、
前記検査用モデル生成ステップでは、前記選択されたモデル検査エンジンに対応する検査用モデル生成方法情報に基づいて前記検査用モデルを生成し、
前記検査性質生成ステップでは、前記選択されたモデル検査エンジンに対応する検査性質生成方法情報に基づいて前記検査性質を生成し、
前記モデル検査ステップでは、前記選択されたモデル検査エンジンを用いて前記検査用モデルの検査を行い、
前記処理フロー状態抽出ステップでは、前記選択されたモデル検査エンジンに対応する処理フロー状態抽出方法情報に基づいて前記処理フロー状態を抽出する
ことを特徴とする設計支援方法。
【請求項１７】
ジョブの実行順序を記述した処理フローの検査を行うための設計支援方法であって、
コンピュータが、
前記処理フローの設計情報に基づいて、前記処理フローを検査するための検査用モデルを生成し、
前記検査用モデルと該検査用モデルが満たすべき性質の検査性質の情報である検査性質情報とを入力とし、前記検査用モデルが前記検査性質を満たすか検査した結果を出力する
ことを特徴とする設計支援方法。
【請求項１８】
請求項１７記載の設計支援方法において、
前記処理フローの設計情報は、前記処理フローが動作する問題領域を定義する情報と、前記処理フローを定義する情報とを有する
ことを特徴とする設計支援方法。
【請求項１９】
請求項１８記載の設計支援方法において、
前記処理フローが動作する問題領域を定義する情報は、
前記処理フローが動作する問題領域に存在するリソースであって前記処理フローを構成する前記ジョブの作用の対象である前記リソースを特定するリソース構造情報と、前記リソース構造情報に記述された前記各リソースが従う状態遷移を記述したリソース状態遷移情報とを有し、
前記処理フローを定義する情報は、
前記処理フローの情報と、前記処理フローを構成する前記ジョブの実行時の作用の結果として起こる前記リソースの状態遷移を記述したジョブ作用情報と、前記処理フローが実行を開始する時点での前記各リソースの状態を定義した処理フロー事前条件情報とを有する
ことを特徴とする設計支援方法。
【請求項２０】
請求項１９記載の設計支援方法において、
コンピュータが、
前記検査用モデルに加えて、前記検査用モデルの構成要素を、前記ジョブまたは前記リソースに関連付けるモデル関連情報を生成し、
前記処理フローが満たすべき性質の情報と前記モデル関連情報とに基づいて、前記検査性質情報を生成する
ことを特徴とする設計支援方法。
【請求項２１】
請求項２０記載の設計支援方法において、
コンピュータが、
前記検査用モデルが前記検査性質を満たさない場合に、該検査性質を満たさない反例情報を検査結果の一部として出力し、
前記反例情報から、前記モデル関連情報に基づいて、前記処理フローの実行時に起こり得る状態である処理フロー状態を生成する
ことを特徴とする設計支援方法。
【請求項２２】
請求項１９記載の設計支援方法において、
前記ジョブの状態に関する命題と前記リソースの状態に関する命題とを組み合わせて表現した前記処理フローが満たすべき性質の情報がコンピュータに入力された後、
コンピュータが、前記性質の情報を前記検査性質情報に変換する
ことを特徴とする設計支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータによって自動化される処理の流れを記述した処理フローの設計を支援する設計支援装置、プログラム、および設計支援方法に関する。
【背景技術】
【０００２】
従来、ソフトウェア開発の工程においては、各種のモデルが成果物として作成される。
その１つである処理フローは、コンピュータによって自動化される対象である処理の流れを表現したモデルである。処理フローの具体的な記述方法としては、業務フロー、フローチャート、ジョブネット、ペトリネット、ビジネスプロセスなどに代表される図による表現や、ＪＣＬ（Job  Control  Language）、ＢＰＥＬ（Business  Process  Execution  Language）などのプログラミング言語で記述したテキスト表現がある。
処理フローの作成を支援する従来技術としては、実際の業務をシステム的にモデル化した業務モデルを構成する各構成要素の種別を判別し、その種別に応じた検証ルールにより検証を行い、不適合と判定された場合、不適合を解消するために操作すべき位置を表示する技術がある（例えば、特許文献１を参照）。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特願２００６−５３６２９０号公報(ＷＯ２００６／０３３１５９Ａ１)
【発明の概要】
【発明が解決しようとする課題】
【０００４】
ところで、従来技術では、検証可能な性質は、処理フローが画面上でアイコン(構成要素)から他アイコン(他構成要素)への関連線のひき方等の描画ルールに適合しているか否か等である。
例えば、処理フローが描画ルールに適合しているが、処理フローが表現している処理の流れが業務要件を満たしていない場合を判別することができない。
本発明は上記実状に鑑み、処理フローが表現している処理の流れが、業務要件を満たしているか否かを検査できる設計支援装置、プログラム、および設計支援方法の提供を目的とする。
【課題を解決するための手段】
【０００５】
上記目的を達成すべく、第１の本発明に関わる設計支援装置は、ジョブの実行順序を記述した処理フローの検査を行うための設計支援装置であって、前記処理フローの設計情報に基づいて、前記処理フローを検査するための検査用モデルを生成する検査用モデル生成部と、前記検査用モデルと該検査用モデルが満たすべき性質の検査性質の情報である検査性質情報とを入力とし、前記検査用モデルが前記検査性質を満たすか検査した結果を出力するモデル検査部とを備えている。
【０００６】
第２の本発明に関わるプログラムは、ジョブの実行順序を記述した処理フローの検査を行うためのプログラムであって、コンピュータを、前記処理フローの設計情報に基づいて、前記処理フローを検査するための検査用モデルを生成する検査用モデル生成部、前記検査用モデルと該検査用モデルが満たすべき性質の検査性質の情報である検査性質情報とを入力とし、前記検査用モデルが前記検査性質を満たすか検査した結果を出力するモデル検査部、として機能させている。
【０００７】
第３の本発明に関わる設計支援方法は、ジョブの実行順序を記述した処理フローの検査をコンピュータが行うための設計支援方法であって、前記処理フローの情報と、前記処理フローが動作する問題領域に存在するリソースであって前記処理フローを構成する前記ジョブの作用の対象である前記リソースを特定するリソース構造情報と、前記リソース構造情報に記述された前記各リソースが従う状態遷移を記述したリソース状態遷移情報と、前記処理フローを構成する前記ジョブの実行時の作用であって当該ジョブの実行の結果として起こる前記リソースの状態遷移を記述したジョブ作用情報と、前記処理フローが実行を開始する時点での前記各リソースの状態を定義した処理フロー事前条件情報とに基づいて、前記処理フローの構成要素である前記ジョブの振る舞いと前記リソース構造情報の構成要素である前記リソースの振る舞いを記述した検査用モデルを生成し、さらに、前記検査用モデルの構成要素を、前記ジョブまたは前記リソースに関連付けるモデル関連情報を生成する検査用モデル生成ステップと、前記処理フローが満たすべき性質の情報と前記モデル関連情報に基づいて、前記検査用モデルが満たすべき検査性質の情報を生成する検査性質生成ステップと、前記検査用モデルが前記検査性質を満たすかを検査し、満たしていない場合は、該満たしていない反例情報を生成するモデル検査ステップと、前記反例情報から、前記モデル関連情報に基づいて、前記処理フローを構成する前記ジョブと前記リソース構造を構成する前記リソースのそれぞれの前記処理フロー実行時に起こり得る処理フロー状態を生成する処理フロー状態抽出ステップと、を含んでいる。
【０００８】
第４の本発明に関わる設計支援方法は、ジョブの実行順序を記述した処理フローの検査を行うための設計支援方法であって、コンピュータが、前記処理フローの設計情報に基づいて、前記処理フローを検査するための検査用モデルを生成し、前記検査用モデルと該検査用モデルが満たすべき性質の検査性質の情報である検査性質情報とを入力とし、前記検査用モデルが前記検査性質を満たすか検査した結果を出力している。
【発明の効果】
【０００９】
本発明によれば、処理フローが表現している処理の流れが、業務要件を満たしているか否かを検査できる設計支援装置、プログラム、および設計支援方法を実現できる。
【図面の簡単な説明】
【００１０】
【図１】本発明に係る第１実施形態の設計支援装置の概略を示した図である。
【図２】第１実施形態の設計支援装置を実現するハードウェア構成を示す図である。
【図３】第１実施形態のジョブネット形式で表現した処理フロー例を示す図である。
【図４】第１実施形態の１例のリソース構造モデル例を示す図である。
【図５】第１実施形態の１例のリソース状態遷移モデル例を示す図である。
【図６】第１実施形態のジョブ作用情報を記述した１例のジョブ作用テーブル例を示す図である。
【図７】第１実施形態の処理フロー事前条件の例である処理フロー事前条件テーブルを示す図である
【図８】第１実施形態のジョブ状態遷移モデルを示す図である。
【図９】第１実施形態の要素名変換情報の例である要素名変換テーブルを示す図である。
【図１０】第１実施形態のリソース状態名変換情報の例であるリソース状態名変換テーブルを示す図である。
【図１１】第１実施形態の検査用モデル生成処理の全体のフローチャートである。
【図１２】第１実施形態の検査用モデル生成処理における宣言部生成処理のフローチャートである。
【図１３】第１実施形態のPROMELAの宣言部のPROMELAのソースコード例である。
【図１４】第１実施形態のPROMELAのinitプロセスの定義を生成する処理のフローチャートである。
【図１５】第１実施形態のPROMELAのinitプロセスの定義のソースコードの出力例である。
【図１６】第１実施形態のジョブネットプロセスの定義を生成する生成処理のフローチャートである。
【図１７】第１実施形態のジョブネットプロセスの定義を生成する生成処理のPROMELAのソースコードの出力例である。
【図１８】第１実施形態のリソースプロセスの定義を生成する処理のフローチャートである。
【図１９】第１実施形態のリソースプロセスの定義を生成する処理のPROMELAのソースコードの出力例である。
【図２０】第１実施形態のＤＢのインスタンスである昼用ＤＢに対応するリソースプロセスDay_DBのPROMELAのソースコードである。
【図２１】第１実施形態のイベントジョブのジョブプロセスの定義を生成する処理のフローチャートである。
【図２２】第１実施形態のイベントジョブであるジョブＡに対応して生成されるPROMELAのソースコードである。
【図２３】第１実施形態のORジョブの定義を生成する処理のフローチャートである。
【図２４】第１実施形態のORジョブであるジョブＣに対応して生成されるPROMELAのソースコードである。
【図２５】第１実施形態の判定ジョブのジョブプロセスの定義を生成する処理のフローチャートである。
【図２６】第１実施形態の判定ジョブであるジョブＤに対応して生成されるPROMELAのソースコードである。
【図２７】第１実施形態の標準ジョブとアクションジョブと従属ジョブのジョブプロセスの定義を生成する処理のフローチャートである。
【図２８】第１実施形態の標準ジョブであるジョブＦに対応して生成されるPROMELAのソースコードである。
【図２９】第１実施形態のジョブＩに対応するジョブプロセスの定義である。
【図３０】第１実施形態のジョブＪに対応するジョブプロセスの定義である。
【図３１】第１実施形態のジョブＥに対応するジョブプロセスの定義である。
【図３２】第１実施形態の処理フローと業務要件の整合性を確認する方法の一例を示したジョブネット設計画面の図である。
【図３３】第１実施形態のSpinのグラフィカル・インターフェイスであるXspinが出力するデータバリュー情報を示す図である。
【図３４】第１実施形態の処理フロー状態生成部が出力した処理フロー状態の出力例を示す図である
【図３５】第１実施形態の処理フロー状態を表示する処理フロー状態画面を示す図である
【図３６】第１実施形態の状態遷移整合性が破られた時点でのリソースの状態を表示するリソース状態画面を示す図である。
【図３７】第２実施形態の状態遷移整合性を持つようにした新しい第２処理フロー例を示した図である。
【図３８】第２実施形態の第２ジョブ作用テーブル例を示した図である。
【図３９】第２実施形態の設計者が業務要件を入力することができる業務要件入力画面を示す図である
【図４０】第２実施形態の検証性質生成部が事後条件をSpin向けの検査性質に変換する手順を示したフローチャートである。
【図４１】第２実施形態の事後条件を、検証性質生成部が変換した結果のソースコードを示す図である。
【図４２】第２実施形態の検査性質の検証を、第２処理フロー例、リソース構造モデル例、リソース状態遷移モデル例、第２ジョブ作用テーブル例から検査用モデル生成部が生成した検査用モデルに対して行った場合に出力される検査結果を示す図である。
【図４３】第２実施形態の検査結果から処理フロー状態生成部が生成する処理フロー状態を示す図である。
【図４４】第３実施形態の業務要件を入力することができる業務要件入力画面を示す図である。
【図４５】第３実施形態の検査性質生成部による不変条件の検査性質を生成するためのフローチャートである。
【図４６】第３実施形態の検査性質の出力例を示す図である。
【図４７】第３実施形態の検査性質の検査を行った際に、モデル検査部が出力する検査結果を示す図である。
【図４８】第３実施形態の検査結果から処理フロー状態生成部が生成する処理フロー状態を示す図である。
【図４９】第４実施形態の設計支援装置の概略を示した図である。
【発明を実施するための形態】
【００１１】
以下、本発明の実施形態について添付図面を参照して説明する。
＜＜実施形態の概要＞＞
図１は、本発明に係わる第１実施形態の設計支援装置１００の概略を示した図である。
本実施形態の設計支援装置１００は、ソフトウェアの設計時に処理フロー１１１の不具合、すなわち下記の業務要件を満たさないケースを見つけ、処理フロー１１１の設計を支援する装置である。
【００１２】
具体的な処理フロー１１１の検査に用いる業務要件の例として以下の３つが挙げられる。
第１に、処理フロー１１１が実現するジョブの実行順序が、既定の後記のリソース状態遷移モデル１１３と整合している必要がある。この第１の性質を状態遷移整合性と呼称する。
第２に、処理フロー１１１が正常に終了した時点での満たすべき条件である。例として、処理フロー１１１が正常に終了した時点では、昼系サービスが停止し、夜系サービスが提供されていなければならない等がある。この第２の性質を事後条件と呼称する。
【００１３】
第３に、処理フロー１１１の稼動時の不変的に満たすべき条件である。例として、処理フロー１１１が動作している場合は、アプリケーションプログラム(以下、アプリケーションと称する)が動作している間は常に当該アプリケーションが使用するデータベースが稼働していなければならない等がある。この第３の性質を不変条件と呼称する。
なお、以下の実施形態の業務要件１２４には、事後条件、不変条件を含み、業務要件の状態遷移整合性は、後記の設計情報１１０から取得されるものとする。
【００１４】
以下、第１実施形態〜第４実施形態について、詳細に説明する。
＜＜第１実施形態＞＞
＜第１実施形態の設計支援装置１００の全体構成＞
本実施形態の設計支援装置１００は、前記したように、ソフトウェアの実装前に処理フロー１１１の不具合、すなわち業務要件(状態遷移整合性)を満たさないケースを見つけ、処理フロー１１１の設計を支援する装置である。
なお、業務要件１２４の事後条件に係わる検査は、第２実施形態で説明し、業務要件１２４の不変条件に係わる検査は、第３実施形態で説明することとし、第１実施形態では、業務要件のうちの状態遷移整合性に係わる検査の説明を行うこととする。
図１において、円筒形(符号１１１〜１１５、１２０〜１２５)の要素はデータを表し、例えば、該データが格納されるデータファイルを表している。なお、データファイルに限定されないのは勿論である。
また、四角形(符号１０１〜１０６)の要素は、設計支援装置１００の機能を実現する構成要素を表し、例えば、各機能を実現するための処理部を示している。
【００１５】
データと構成要素間の矢印のうち、データ(図１の円筒形の要素)から構成要素(図１の四角形の要素)に向かう矢印は、当該データが当該構成要素への入力であることを示し、構成要素(図１の四角形の要素)からデータ(図１の円筒形の要素)に向かう矢印は、当該データが当該構成要素からの出力であることを示している。
設計情報１１０と業務要件１２４は、設計者が設計支援装置１００に入力として与える情報である。
設計情報１１０は、後記する入力装置３６０４から入力されるか、或いは他システムから取り込んで後記する外部記憶装置３６０３に記憶される。業務要件１２４は、設計支援装置１００の業務要件記述支援部１０５によっても生成される。
【００１６】
図１に示す設計情報１１０は、ジョブの流れを表す処理フロー１１１と、処理フローが自動化する対象に存在し、ジョブの作用対象であるリソースの構造を表すリソース構造モデル１１２と、リソースの状態遷移を表すリソース状態遷移モデル１１３と、ジョブの実行結果として起こるリソースの状態遷移を定義するジョブ作用情報１１４と、各リソースの初期状態を表す処理フロー事前条件１１５とを備えている。本実施形態の説明では、リソースの例としてアプリケーションとデータベースを用いる。
【００１７】
図１に示すように、設計支援装置１００は、処理フローの設計情報１１０を入力として、処理フローの検査用の検査用モデル１２０およびジョブ、リソース等の各要素およびその状態変数を結び付けるモデル関連情報１２１を出力する検査用モデル生成部１０１と、設計情報１１０を入力として設計者による検査条件の業務要件１２４(事後条件、不変条件)の記述を支援する業務要件記述支援部１０５と、モデル関連情報１２１と業務要件１２４とを入力として業務要件１２４を検査に使用できる形式の検査性質１２５として出力する検査性質生成部１０６と、検査用モデル１２０を検査性質１２５等に従って検査(処理フローの検査)を行うモデル検査部１０２と、モデル検査部１０２の出力の検査結果１２２を入力として設計者に確認し易い形式の検査結果の処理フロー状態１２３を出力する処理フロー状態生成部１０４とを備えている。
【００１８】
＜ハードウェア構成＞
図２は、第１実施形態の設計支援装置１００を実現するハードウェア構成を示す図である。
設計支援装置１００を実現する装置は、コンピュータであり、該コンピュータは、ＣＰＵ(Central  Processing  Unit)３６０１、ＲＡＭ(Random Access Memory)等の主メモリ３６０２と、ＨＤＤ(Hard Disk Drive)等の外部記憶装置３６０３と、入力装置３６０４と、出力装置のディスプレイ３６０５とを有し構成されている。
【００１９】
本第１実施形態の設計支援装置１００はソフトウェアであり、検査用モデル生成部１０１、モデル検査部１０２、モデル検査エンジン１０３、処理フロー状態生成部１０４、業務要件記述支援部１０５、および検査性質生成部１０６は、プログラムとしてＨＤＤ等の外部記憶装置３６０３に保存されている。
外部記憶装置３６０３に保存されるプログラムは、ＣＰＵ３６０１により、主メモリ３６０２にロードされて実行され、検査用モデル生成部１０１、モデル検査部１０２、モデル検査エンジン１０３、処理フロー状態生成部１０４、業務要件記述支援部１０５、および検査性質生成部１０６が具現化される。
【００２０】
プログラムの実行の結果として生成される情報、すなわち、図１に示す検査用モデル１２０、モデル関連情報１２１、検査結果１２２、処理フロー状態１２３、業務要件１２４、および検査性質１２５は、主メモリ３６０２のワークエリアまたは外部記憶装置３６０３に保存される。
前記したように、図１に示す処理フロー１１１、リソース構造モデル１１２、リソース状態遷移モデル１１３、ジョブ作用情報１１４、処理フロー事前条件１１５等の設計情報１１０は、図２に示す入力装置３６０４から入力されて外部記憶装置３６０３に記憶されるか、或いは、他システムから取り込んで外部記憶装置３６０３に記憶される。なお、設計情報１１０は、主メモリ３６０２(図２参照)に一時記憶されるように構成してもよい。
また、設計者は、設計支援装置１００がディスプレイ３６０５に表示する情報(例えば、後記する図３９、図４４に示す業務要件入力画面３９０１、４４０１)を目視でき、マウスやキーボードなどの入力装置３６０４を用いて設計支援装置１００に対して情報を入力することができる。例えば、後記する図３９、図４４に示す業務要件入力画面３９０１、４４０１に情報を入力することができる。
【００２１】
＜検査対象＞
本第１実施形態は、設計支援装置１００によるジョブ管理製品であるJP1（登録商標）の入力であるジョブネットの設計支援に関するものを例示して説明する。
JP1（登録商標）においては、コマンド投入などの処理を１つのジョブとしてモデル化し、ジョブの実行順序をジョブネットとして表現する。JP１（登録商標）は、入力されたジョブネットを、あらかじめ設定された状況下で自動的に実行する。
【００２２】
まず、図１に示す設計支援装置１００の検査用モデル生成部１０１の働きを説明する。
検査用モデル生成部１０１が入力とする設計情報１１０は、処理フローが動作する問題領域を定義する情報と、処理フローを定義する情報とを有し構成される。ここで、前者の処理フローが動作する問題領域を定義する情報は、リソース構造モデル１１２とリソース状態遷移モデル１１３とから構成され、後者の処理フローを定義する情報は、処理フロー１１１とジョブ作用情報１１４と処理フロー事前条件１１５とを有し構成される。
【００２３】
＜処理フロー１１１＞
次に、図１に示す処理フロー１１１について説明する。
図３は、処理フロー１１１の例であるジョブネット形式(実行順序を付けた複数のジョブの集まり)で表現した処理フロー例２０１を示す図である。
図３に示すジョブネットの目的は、昼系から夜系にサービス切替えを行うための処理の自動化である。ここで、サービスは、アプリケーションとデータベースによって提供されており、例えばＷｅｂサーバがクライアントからのリクエストを昼系アプリケーションまたは夜系アプリケーションに振り分けていると想定している。
【００２４】
図３に示す処理フロー例２０１は、２１１から２２０の１０個のジョブから構成されている。ジョブネットは、一般的に図中の左に位置するジョブから右に位置するジョブへの処理が流れるように記述するが、本第１実施形態では、スペースの関係上、図３の上部に位置するジョブから下部に位置するジョブへと処理が流れるように記述している。
ジョブの実行順序は、ジョブネット中の矢印で示される。あるジョブが矢印の終点である場合、その矢印の起点であるジョブを、矢印の終点であるジョブの先行ジョブであると定義する。ここで、ジョブは、複数の先行ジョブを持つことができることに留意する。この先行ジョブに対し、矢印の終点のジョブは後続ジョブであると定義する。同様に、ジョブは、複数の後続ジョブを持つことができる。例えば、ジョブ２１３の先行ジョブはジョブ２１１とジョブ２１２の２つであり、ジョブ２１３の後続ジョブはジョブ２１４である。
【００２５】
先行ジョブを持たないジョブを、ジョブネットの起点ジョブと呼称する。後続ジョブを持たないジョブを、ジョブネットの終点ジョブと呼称する。例えば、図２に示す処理フロー例の起点ジョブはジョブ２１１とジョブ２１２であり、終点ジョブはジョブ２２０である。このように、起点ジョブ、終点ジョブとも、複数存在する場合がある。
一般に、ジョブは、全ての先行ジョブが終了状態になった時に実行可能となる。判定ジョブ、従属ジョブ、ＯＲジョブの扱いは例外的であるが、これは後記する。ジョブネットの起点ジョブは、ジョブネットが実行を開始した時点で実行可能である。一方、ジョブネットは、その終点ジョブが全て完了した時点で終了状態となる。
なお、ジョブネットは、ジョブの１つでも異常終了状態になった場合に、異常終了状態となる。これは、一般に、ジョブネットの処理が途中で異常終了状態となるため、ジョブネットが自動化している処理がその目的を達成できなかったことを意味する。
【００２６】
ジョブネット中の各ジョブは、それぞれいくつかのプロパティ(各オブジェクトに関する情報をまとめたもの)を持つ。図３には、本実施形態に関係するプロパティのみを示している。ＩＤ(identification)とは、ジョブを一意に識別するための識別情報である。図３に示す処理フロー例２０１を構成するジョブのＩＤは、「ジョブＡ」から「ジョブＪ」である。
種別は、ジョブの種類を示すプロパティであり、イベントジョブ、ＯＲジョブ、判定ジョブ、従属ジョブ、標準ジョブ、アクションジョブがある。これらのジョブの性質については、JP1（登録商標）のマニュアル等で参照できる。本第１実施形態においては、以下の簡潔な解説に留める。
【００２７】
イベントジョブとは、特定の時刻の到来や、電子メールの受信等のイベントをモデル化したものであり、予め設定されたイベントが起こった時に実行され、終了状態となる。イベントジョブは、先行ジョブを持つことはできない。
ＯＲジョブは、イベントジョブのみを先行ジョブとして持つことができる。ＯＲジョブは、先行ジョブのどれか１つが終了状態となった時に実行可能となる。
【００２８】
判定ジョブは、設定された条件に基づいた判定を行う。判定条件は、特定のファイルの有無や、特定のファイルの更新などが設定可能である。判定結果が「真」である場合は、後続ジョブが実行可能となる。判定結果が「偽」である場合は、後続ジョブではなく従属ジョブが実行可能となる。判定ジョブの後続ジョブは、判定ジョブの判定結果が「真」である場合と、判定ジョブの判定結果が「偽」であって従属ジョブが終了状態になった場合に実行可能となる。
【００２９】
標準ジョブは、ＵＮＩＸ（登録商標）搭載ホストコンピュータやWindows（登録商標）搭載ホストコンピュータで処理を実行させたり、特定のキューにジョブを送って処理を実行させるためのジョブである。
アクションジョブは、電子メール送信やJP1（登録商標）イベント送信など特定のアクションを行うジョブである。
【００３０】
各ジョブの名称は、設計者がジョブを識別するために付けることができる名称である。
プロパティの終了判定は、該当ジョブが、「常に正常終了するジョブ」、「常に異常終了するジョブ」、「状況によって、正常終了と異常終了のどちらかが可能なジョブ」の３種類のうちどれに当たるかを示すプロパティである。本実施例では、終了判定プロパティ「１」が「常に正常終了するジョブ」、「−１」が「常に異常終了するジョブ」、「０」が「状況によって、正常終了と異常終了のどちらかが可能なジョブ」に該当するものとして表現している。図３においては、ジョブ２１５のみが終了判定「０」なので、正常終了と異常終了の両方があり得る。他のジョブは、全て終了判定「１」なので、常に正常終了するジョブであり、図３に示す処理フロー例２０１には、常に「異常終了するジョブ」が存在しない。
【００３１】
ここで、図３に示す処理フロー例２０１の処理の流れの概要を説明する。
昼系から夜系への切替えを指示する電子メールの受信（ジョブ２１１）またはコマンド投入（ジョブ２１２）を、ジョブ２１３が検知し、後続するジョブ２１４へと処理を渡す。ジョブ２１４は、システム切替えを開始する前に、適切なログファイルが存在することを確認するための判定ジョブである。
【００３２】
上記ログファイルが存在しない場合、判定ジョブのジョブ２１４が「偽」であるので、従属ジョブのジョブ２１５が実行される。ジョブ２１５でリカバリー処理を行い、それが成功した場合は正常終了し、ジョブ２１６とジョブ２１７が実行可能となる。一方、ジョブ２１５でのリカバリー処理が失敗した場合は、異常を通知し、ジョブ２１５自身も異常終了する。この場合、図３に示す処理フロー例２０１のジョブネット全体が異常終了する。
【００３３】
ジョブ２１４で適切なログファイルが存在することを確認した場合(ジョブ２１４が「真」の場合)またはジョブ２１５が正常終了した場合、ジョブ２１６は、夜用のアプリケーションを起動するとともに、ジョブ２１７は、昼用のアプリケーションを停止する。ジョブ２１６に続くジョブ２１８は、夜用のアプリケーションが使用する夜用のデータベースをコマンドで起動する。ジョブ２１７に続くジョブ２１９は、クライアントからのリクエストの振り分け先を、昼用アプリケーションから夜用アプリケーションに変更する。
ジョブ２１８、２１９が正常終了した場合、ジョブ２２０は、システム切替えが正常に終了したことを通知する電子メールを管理者に送信する。
【００３４】
＜リソース構造モデル１１２＞
次に、図１に示すリソース構造モデル１１２の１例であるリソース構造モデル例３０１について説明する。
図４は、リソース構造モデル１１２の１例のリソース構造モデル例３０１を示す図である。
リソース構造モデル１１２(図１参照)は、自動化の対象である業務の問題領域に存在し、ジョブによる作用の対象となるリソースを定義する。
【００３５】
本第１実施形態では、リソース構造モデル１１２はＵＭＬ（登録商標）のクラス図の記法に従って記述するが、矢印は誘導可能性ではなく汎化関係を表している。図４に示すリソース構造モデル１１２のリソース構造モデル例３０１は、問題領域に、ＡＰ３１０とＤＢ３２０の２種類のリソースが存在することを示す。なお、ＡＰは「アプリケーション」、ＤＢは「データベース」を示す。図３において、ＡＰ３１０のインスタンスとして、昼用ＡＰ３１１と夜用ＡＰ３１２があることが示されており、ＤＢ３２０のインスタンスとして、昼用ＤＢ３２１と夜用ＤＢ３２２があることが示されている。
【００３６】
＜リソース状態遷移モデル１１３＞
次に、図１に示すリソース状態遷移モデル１１３について説明する。
図５は、リソース状態遷移モデル１１３の１例のリソース状態遷移モデル例４０１を示す図である。
リソース状態遷移モデル１１３は、リソース構造モデル１１２(図１参照)で定義されているリソースの種類それぞれについて、その状態遷移を定義する。
リソース状態遷移モデル１１３(図１参照)である図５に示すリソース状態遷移モデル例４０１は、ＡＰ３１０とＤＢ３２０の状態遷移を定義している。
【００３７】
ＡＰ３１０の状態遷移４１０は、リクエスト対応状態４１１と稼動状態４１２と停止状態４１３とから構成されている。ここで、リクエスト対応状態４１１とは、ＡＰ３１０がクライアントからのリクエストを受け取り、処理することが可能である状態を指しており、より具体的には、Ｗｅｂサーバによるリクエスト振り分け先である状態を示している。稼動状態４１２とは、ＡＰ３１０は稼働中であるが、リクエストを振り分けられていない状態を指す。停止状態４１３は、ＡＰ３１０が停止している状態を指す。
ＤＢ３２０の状態遷移４２０は、アクセス可能な稼動状態４２１とアクセス不可能な停止状態４２２から構成されている。
【００３８】
＜ジョブ作用情報１１４＞
次に、図１に示すジョブ作用情報１１４について説明する。
図６は、ジョブ作用情報１１４を記述した１例のジョブ作用テーブル例５０１を示す図である。
ジョブ作用情報１１４(図１参照)は、ジョブネットを構成するジョブの実行結果として起こるリソースの状態遷移を定義したものである。
【００３９】
図６に示すジョブ作用テーブル例５０１は、ジョブＩＤと対象リソースと遷移先状態のカラムから構成される。ジョブ作用テーブル例５０１の各行は、ＩＤで特定されるジョブが実行され終了状態になる際の作用として、対象リソースが遷移する先の状態(遷移先状態)を定義する。例えば、ジョブ作用テーブル例５０１の第１行目は、ジョブＦ（図３のジョブ２１６）が実行され終了状態になると、夜用ＡＰ３１２が稼働中になる作用を持っていることを示している。
【００４０】
＜処理フロー事前条件１１５＞
図７は、図１に示す処理フロー事前条件１１５の例である処理フロー事前条件テーブル６０１を示す図である。
処理フロー事前条件１１５は、処理フロー１１１に対応するものであり、図７に示す処理フロー事前条件テーブル６０１は、図３に示す処理フロー例２０１の事前条件を定義する。
処理フロー事前条件テーブル６０１の各行は、対応する処理フロー例２０１の実行開始時点での各リソースの初期状態を定義する。例えば、処理フロー事前条件テーブル６０１の１行目は、昼用ＡＰの初期状態はリクエスト対応状態であることを示している。また、昼用ＤＢは、稼動状態であり、夜用ＡＰ、夜用ＤＢの初期状態は、それぞれ停止状態であることを示している。
すなわち、処理フロー事前条件テーブル６０１全体で、図３に示す処理フロー例２０１の初期状態は、昼系のサービスが提供中であり、夜系のサービスは停止中であることを表している。
以上が、検査用モデル生成部１０１が入力とする設計情報１１０である。
【００４１】
＜業務要件＞
従来のソフトウェア開発では、設計者は、図１に示すリソース構造モデル１１２とリソース状態遷移モデル１１３を参照しながら処理フロー１１１を設計する。リソース構造モデル１１２とリソース状態遷移モデル１１３は明示されない場合もある。その場合は、設計者は、これらの情報を暗黙的に考慮しながら処理フロー１１１を作成する。
処理フロー１１１を作成する際には、処理フロー１１１が業務要件と合致している必要がある。例えば、図３に示す処理フロー例２０１の作成においては、この処理フローが正しく昼系から夜系へのサービス切替え手順を自動化している必要がある。
【００４２】
具体的な業務要件の例として、前記したように、以下の３つが挙げられる。
第１に、処理フロー１１１が実現するジョブの実行順序が、リソース状態遷移モデル１１３と整合している必要があるという状態遷移整合性である。
第２に、例えば、処理フロー１１１が正常に終了した時点では、昼系サービスが停止し、夜系サービスが提供されていなければならないという処理フロー１１１が正常に終了した時点での要件を表す事後条件である。
第３に、処理フロー例２０１が動作している場合は、常にアプリケーションが動作している間は当該アプリケーションが使用するデータベースが稼働していなければならないという第３の不変条件である。この場合、この不変条件がなければ、当該アプリケーションが当該データベースにアクセスできず、障害の原因となるからである。
【００４３】
上記３つの業務要件を処理フロー例２０１(図３参照)が満たしていることを設計者が目視して確認することは困難であり、テスト、デバック等に時間がかかり、ソフトウェア開発のコスト増大の要因の１つとなっている。例えば、テストよって上記の性質を確認する場合には、テストデータの準備や、処理フローが動作する環境の構築にコストがかかる。また、テストデータの品質によっては、上記性質の確認が不十分に終わる可能性があり、さらに作業時間を要する可能性が潜在する。
【００４４】
また、多くの企業の情報システムは、数百から数万のジョブネットを運用することで業務の自動化を実現している。この場合、個々のジョブネットについて、上述の第１の状態遷移整合性、第２の事後条件、第３の不変条件の充足性を目視で確認することは容易であっても、全てのジョブネットについて確認することは困難であるのが実状である。
これに対して、本実施形態の技術は、処理フローが業務要件(状態遷移整合性、事後条件、不変条件等)と合致していることの確認を自動化するものである。さらに、本実施形態によれば、処理フローを実際に動作させることなく、上記業務要件(状態遷移整合性、事後条件、不変条件等)の充足性、すなわち充足しているか否かの確認を行うことができる。
【００４５】
以下、図１に示す設計支援装置１００の各構成要素について説明する。
＜検査用モデル生成部１０１＞
図１に示す検査用モデル生成部１０１が行う処理の手順を説明する。
検査用モデル生成部１０１は、設計情報１１０を入力とし、検査用モデル１２０とモデル関連情報１２１を出力する。
検査用モデル１２０は、図３に示す処理フロー例２０１を構成するジョブの実行順序と各ジョブの作用や、リソースの状態遷移、事後条件(第２実施形態で説明)、不変条件(第３実施形態で説明)の業務要件等をシミュレートするものである。
モデル関連情報１２１は、検査用モデル１２０の構成要素と、ジョブまたはリソースとの関連性の情報である。
【００４６】
図１に示すように、検査用モデル１２０は、モデル検査部１０２が入力として用いる。モデル検査部１０２は、モデル検査エンジン１０３を用いて、検査用モデル１２０を検査する。本第１実施形態では、モデル検査エンジン１０３は、既存のツールであるSpinを使用する。検査用モデル１２０は、モデル検査エンジン１０３が入出力する形式で記述する。Spinは、モデル記述言語PROMELAで記述したモデルを入力とするため、本実施例の検査用モデル１２０は、PROMELA言語で記述したソースコードである。
【００４７】
検査用モデル生成部１０１の出力である検査用モデル１２０は、１つのテキストファイルとして記述されたPROMELAプログラムであり、宣言部、initプロセス定義、ジョブネットプロセスの定義、各リソースプロセスの定義、各ジョブプロセスの定義から構成される。
なお、ジョブネット、リソース、ジョブとは、設計者が作成したものをそれぞれ示し、検査用モデル１２０内のジョブネット、リソース、ジョブをそれぞれジョブネットプロセス、リソースプロセス、ジョブプロセスと称する。
【００４８】
本第１実施形態における検査用モデル１２０は、ジョブネットとジョブとリソースを、並行動作するプロセスとしてモデル化する。各プロセスは状態を持つ。リソースプロセスの状態遷移は、リソース状態遷移モデル１１３(図５のリソース状態遷移モデル例４０１参照)に基づいて生成する。
図８は、ジョブ状態遷移モデル７０１を示す図である。
ジョブプロセスの状態遷移は、図８に示すジョブ状態遷移モデル７０１に基づいて生成する。ジョブ状態遷移モデル７０１は、設計者が設計支援装置１００に入力する情報ではない。
ジョブ状態遷移モデル７０１を説明すると、ジョブの初期状態は停止状態（Not_Started７１０）であり、そこから実行中状態（Running７１１）に遷移可能である。実行中状態（Running７１１）からは、４種類の終了状態の何れかに遷移可能である。
【００４９】
Completed７１２は、正常終了状態である。Completed_Abnormal７１３は、異常終了状態である。判定ジョブ以外の全ての種類のジョブは、正常終了状態(Completed７１２)または異常終了状態(Completed_Abnormal７１３)に遷移しなければならない。判定ジョブは、判定が真である終了状態（Completed_True７１４）か、判定が偽である終了状態（Completed_False７１５）に遷移しなければならない。
ジョブネットは、実行前状態（JN_Not_Started）と、実行中状態（JN_Running）と、正常終了状態（JN_Completed）と、異常終了状態（JN_Completed_Abnormal）を持つ。これらの状態遷移は単純であるので、図示を省略する。ジョブネットの状態遷移は、設計者が設計支援装置１００に入力する情報ではない。
【００５０】
＜モデル関連情報１２１＞
図１に示す検査用モデル生成部１０１が出力するモデル関連情報１２１は、要素名変換情報とリソース状態名変換情報から構成される。
図９は、要素名変換情報の例である要素名変換テーブル８０１を示す図であり、図１０は、リソース状態名変換情報の例であるリソース状態名変換テーブル９０１を示す図である。
【００５１】
＜モデル関連情報１２１の要素名変換テーブル８０１＞
図９に示す要素名変換テーブル８０１の１行目から１０行目は、処理フロー１１１の要素であるジョブが対応する検査用モデル１２０(図１参照)の要素を示し、検査用モデル１２０の要素の状態を示す変数名も示している。例えば、１行目は、ジョブＡは検査用モデル１２０(図１参照)においては「Job1」という名称の変換名で記述され、その状態は状態変数「Job1_state」で表されることを示す。要素名変換テーブル８０１の１１行目から１４行目は、リソースが対応する検査用モデル１２０の要素名とその変換名とその状態変数を示す。例えば、１１行目は、昼用ＡＰ３１１(図３参照)は「Day_AP」という名称の変換名で記述され、その状態は状態変数「Day_AP_state」で表されることを示す。
【００５２】
要素名変換テーブル８０１の生成方法は以下の通りである。
まず、処理フロー１１１(図１参照)に登場する各ジョブのＩＤを取得する。変換名は「Job」の後に、新規に採番した番号をつけたものとする。リソース名は、リソース構造モデル１１２(図４のリソース構造モデル例３０１参照)からリソース名を取得する。変換名は、一意でありさえすれば任意の文字列でよいが、本実施例では、理解を容易にするために、リソースの英語名に該当する文字列を便宜的に使用している。ジョブについてもリソースについても、状態変数は、変換名の後ろに「_state」をつけたものとする。
図９に示す要素名変換テーブル８０１に基づけば、ジョブＩＤ(要素名)から当該ジョブに対応するジョブプロセスの名称(変換名)を取得することができ、その逆も可能である。また、リソース名(要素名)から当該リソースに対応するリソースプロセスの名称(変換名)を取得することができ、その逆も可能である。
【００５３】
＜モデル関連情報１２１のリソース状態名変換テーブル９０１＞
図１０に示すリソース状態名変換テーブル９０１は、リソース種類およびリソースの状態名と検査用モデル１２０の定数名(変換名)の対応関係を表す。例えば、リソース状態名変換テーブル９０１の１行目は、ＡＰ３１０(図５参照)のリクエスト対応状態４１１は、「AP_Serving」という定数名(変換名)で表現されることを示す。
【００５４】
リソース状態名変換テーブル９０１の生成方法は以下の通りである。リソース構造モデル１１２(図４のリソース構造モデル例３０１参照)に含まれる各リソースについて、そのリソースが取り得る状態をリソース状態遷移モデル１１３(図５のリソース状態遷移モデル例４０１参照)から取得する。変換名は一意である任意の文字列でよい。本第１実施形態では、理解を容易にするために、リソース種類と状態名と状態名の英語名にあたる文字列(変換名)とを便宜的に使用している。
リソース状態名変換テーブル９０１に基づけば、リソースの状態の検査用モデル１２０における名称(変換名)を取得することができ、その逆も可能である。
【００５５】
＜検査用モデル生成部１０１による検査用モデル生成処理＞
次に、検査用モデル生成部１０１(図１参照)による検査用モデル生成処理の概要について説明する。
図１１は、検査用モデル生成処理の全体のフローチャートを示す図である。
本第１実施形態における検査用モデル１２０(図１参照)は、ジョブネットの振る舞いをモデリングしたジョブネットプロセスと、リソースの振る舞いをモデリングしたリソースプロセスと、ジョブの振る舞いをモデリングしたジョブプロセスとを有して構成されている。PROMELAによる記述は、上記ジョブネットプロセス、リソースプロセス、ジョブプロセス等の各プロセスを定義するソースコードと、各種の変数や定数を定義した宣言部と、各種のプロセスを起動する役割を担うinitプロセスの定義から構成される。
【００５６】
図１１のステップ１００１において、宣言部を生成する。このステップの詳細は図１２を用いて後記する。
続いて、ステップ１００２において、initプロセスの定義を生成する。このステップの詳細は図１４を用いて後記する。
続いて、ステップ１００３において、ジョブネットプロセスの定義を生成する。このステップの詳細は図１６を用いて後記する。
【００５７】
ステップ１００４からステップ１００６では、各リソースに対応するリソースプロセスの定義を生成する。１つのリソースに対応するリソースプロセスの生成手順の詳細は図１８を用いて後記する。
ステップ１００７から１００９では、各ジョブに対応するジョブプロセスの定義を生成する。１つのジョブプロセスの生成手順の詳細は、イベントジョブの場合は図２１、ORジョブの場合は図２３、判定ジョブの場合は図２５、標準ジョブの場合は図２７を用いて後記する。以上が、図１０に示す検査用モデル生成処理の概要である。
【００５８】
＜検査用モデル生成部１０１による検査用モデル生成処理の手順の詳細＞
以下に、検査用モデル生成部１０１による検査用モデル生成処理の手順の詳細を、PROMELAのソースコード例を用いながら説明する。図１３、図１５、図１７等に示すPROMELAのソースコード例は、図３に示す処理フロー例２０１と、図４に示すリソース構造モデル例３０１と、図５に示すリソース状態遷移例４０１と、図６に示すジョブ作用テーブル例５０１と、図７に示す処理フロー事前条件テーブル６０１を入力として検査用モデル生成を行った場合の出力例である。
【００５９】
＜検査用モデル(１２０)生成処理における宣言部生成処理＞
次に、検査用モデル生成処理における宣言部生成処理(図１１のステップ１００１)を、図１２、図１３を用いて説明する。
図１２は、検査用モデル生成処理における宣言部生成処理のフローチャートを示す図であり、図１３は、宣言部のPROMELAのソースコード例である。
図１２のステップ１１０１では、ジョブネットプロセスが取り得る状態の宣言を生成する。前述したように、ジョブネットプロセスは「JN_Not_Started」、「JN_Running」、「JN_Completed」、「JN_Completed_Abnormal」の４つの状態を持つ。ステップ１１０１の出力は設計情報に依存しない。図１３の１２０１がこのステップの出力例である。
【００６０】
図１２のステップ１１０１においては、ジョブネットが取り得る状態の宣言を生成する。
ステップ１１０２においては、ジョブが取り得る状態の宣言を生成する。ジョブが取り得る状態は、図８に示した通りである。ステップ１１０２の出力は設計情報１１０に依存しない。図１３の１２０２がこのステップの出力例である。
図１２のステップ１１０３からステップ１１０６においては、リソース構造モデル１１２(図１参照)で定義されているリソースの種類それぞれについて、当該リソースが取り得る状態の宣言と、そのリソースがジョブから受信することができるメッセージの宣言を生成する。
【００６１】
ステップ１１０３では、リソース構造モデル１１２の中のリソース型のうち、未選択のものを選択する。図４に示すリソース構造モデル例３０１では、リソース型としてＡＰ３１０とＤＢ３２０が定義されている。ＡＰ３１０を選択した場合の処理手順を説明する。
ステップ１１０４では、選択したリソース型が取り得る状態の宣言を生成する。リソース型が取り得る状態は、リソース状態遷移モデル１１３(図５に示すリソース状態遷移例４０１参照)から取得する。検査用モデル１２０(図１参照)における状態名は、図１０に示すリソース状態名変換テーブル９０１に基づいて取得する。例えば、ＡＰ３１０(図５参照)が取り得る状態であるリクエスト対応状態４１１、稼動状態４１２、停止状態４１３を図５のリソース状態遷移モデル例４０１から取得する。次に、リソース状態名変換テーブル９０１(図１０参照)に基づいて、前記の各状態の変換名を取得する。その結果、「AP_Serving」、「AP_Running」、「AP_Stopped」が取得される。これらの宣言を、１つのmtype文として出力する。図１３の１２０３の１行目がこのステップの出力例である。
【００６２】
ステップ１１０５では、選択したリソース型がジョブプロセスと送受信するメッセージの宣言を生成する。検査用モデル１２０(図１参照)においては、リソースプロセスは、ジョブプロセスから状態遷移を促すメッセージを受信することで状態遷移を行う。メッセージは、「To_」に状態名を付けた文字列として生成する。これは、「該当する状態に遷移せよ」との意味を持つ。APが選択されている例においては、図１３の１２０３の２行目のこのステップの出力例に示すように、「To_AP_Serving」、「To_AP_Running」、「To_AP_Stopped」の３つのメッセージを宣言するmtype文を生成する。
図１２のステップ１１０４とステップ１１０５を、ＤＢ３２０(図５参照)について繰り返した場合の出力例は、図１３の１２０４である。１行目がＤＢの状態名を定義したmtype文であり、２行目がＤＢが受信可能なメッセージを定義したmtype文である。
【００６３】
ステップ１１０７では、ジョブネットの状態変数の定義を生成する。図１３の１２０５がこのステップの出力例である。これは設計情報１１０に依存せず、一律に「JN_state」と定義し、その初期状態は「JN_Not_Started」である。
ステップ１１０８からステップ１１１０では、ジョブネット中の各ジョブについて、その状態変数を生成する。状態変数は、図９の要素名変換テーブル８０１で定義した通りである。全てのジョブについての状態変数の定義を１つのmtype文として生成する。図１３の１２０６が、ステップ１１０８からステップ１１１０の繰り返しを全て実行した際の出力例である。
【００６４】
ステップ１１１１からステップ１１１３は、上記と同様の方法で、各リソースの状態変数を宣言するmtype文を生成する。状態変数の名称は図１０のリソース状態名変換テーブル９０１で定義したとおりである。状態変数の初期値は、図７に示す処理フロー事前条件テーブル６０１の初期状態に基づく。昼用ＡＰと夜用ＡＰに関する状態変数の定義は図１３の１２０７であり、昼用ＤＢと夜用ＤＢに関する状態変数の定義は図１３の１２０８である。
以上が、検査用モデル生成処理における図１２に示す宣言部生成処理である。
【００６５】
＜検査用モデル(１２０)生成処理におけるinitプロセスの定義を生成する処理＞
次に、検査用モデル生成処理における各種のプロセスを起動する役割を担うinitプロセスの定義を生成する処理(図１１のステップ１００２)を、図１４、図１５を用いて説明する。
図１４は、PROMELAのinitプロセスの定義を生成する処理のフローチャートを示す図であり、図１５は、そのPROMELAのソースコードの出力例である。
PROMELA言語においては、initプロセスは最初に実行されるプロセスであり、前記したように、他の各種のプロセスを起動する役割を持つ。
【００６６】
図１４のステップ１３０１においては、initプロセスのシグナチャと終端記号を生成する。図１５の１４０１と１４０８がこのステップの出力例である。
図１４のステップ１３０２からステップ１３０４では、各リソースがジョブとの通信に使用するチャネルの宣言を生成する。リソース構造モデル１１２(図４に示すリソース構造モデル例３０１参照)で定義されているリソースそれぞれについてチャネルを１つ定義する。
このステップ１３０２からステップ１３０４を実行した場合の出力例は、図１５の１４０３である。チャネル名は、「Chan_」の後に当該リソースの変換名を付けたものである。リソースの変換名は、図９の要素名変換テーブル８０１に基づいてその変換名から取得する。チャネルで送受信可能なデータ型はmtypeであり、チャネルのサイズは０である。
【００６７】
図１４のステップ１３０５において、ジョブネットプロセスを起動するソースコードを生成する。図１５の１４０４がこのステップの出力例である。run文でジョブネットプロセスを起動し、その次の文でジョブネットの状態を「JN_Running」に変更する。
ステップ１３０６からステップ１３０８においては、各リソースについて、対応するリソースプロセスを起動するrun文を生成する。図１５の１４０５がこれらのステップの出力例である。リソースプロセスを起動するrun文では、そのリソースプロセスが使用するチャネルを引数として与える。１つのリソースプロセスに対し、１つのチャネルが対応する。例えば、１４０５の１行目は、昼用ＡＰに対応するリソースプロセスであるDay_APを起動するrun 文である。引数はチャネルChan_Day_APである。チャネル名の特定方法は、宣言部の生成手順で説明した通りである。なお、１４０５の最初の行は、コメント欄であり、以下の説明でも最初の行のコメント欄を除いた行数を用いて説明する。
【００６８】
図１４のステップ１３０９からステップ１３１１においては、各ジョブについて、対応するジョブプロセスを起動するrun文を生成する。図１５の１４０６がステップ１３０９からステップ１３１１の出力例である。run文が起動するジョブプロセス名は、図９の要素名変換テーブル８０１で定義した変換名から取得する。
ジョブプロセスを起動するrun文では、そのジョブプロセスが使用するチャネルを引数として与える(図１５の１４０６の６行目〜９行目参照)。ジョブプロセスが使用するチャネルは、当該ジョブが作用するリソースごとに１つ必要であり、チャネルの情報は、図６に示すジョブ作用テーブル５０１(ジョブ作用情報１１４(図１参照))から抽出する。
【００６９】
例えば、図６に示すように、ジョブＦは夜用ＡＰにメッセージ送信を行うためのチャネルが必要であり、ジョブＧは昼用ＡＰへのチャネルが必要である。ジョブＨは夜用ＤＢへのチャネルが必要であり、ジョブＩは昼用ＡＰと夜用ＡＰそれぞれに通信するためにチャネルが１つずつ必要である(図９、図６参照)。このように、ジョブプロセスへの引数は、図６のジョブ作用テーブル５０１と図９の要素名変換テーブル８０１とから取得する。
なお、チャネル名の特定方法は、宣言部の生成手順で説明した通りである。
図１４のステップ１３１２において、initプロセスを実行中に他のプロセスに処理が移らないようにするためのatomic文を生成する。図１５の１４０２と１４０７がこのステップの出力例である。atomic文は、initプロセス内に生成した全てのソースコードをスコープとするように生成する。以上が、検査用モデル(１２０)生成処理における図１４に示すinitプロセスの定義を生成する処理である。
【００７０】
＜検査用モデル(１２０)生成処理におけるジョブネットプロセスの定義を生成する生成処理＞
次に、検査用モデル生成処理におけるジョブネットプロセスの定義を生成する生成処理(図１１のステップ１００３)を、図１６、図１７を用いて説明する。
図１６は、検査用モデル生成処理におけるジョブネットプロセスの定義を生成する生成処理のフローチャートを示す図であり、図１７は、そのPROMELAのソースコードの出力例である。
図１６のステップ１５０１において、ジョブネットプロセスのシグナチャと終端記号を生成する。図１７の１６０１がシグナチャの出力例であり、１６０６が終端記号の出力例である。ジョブネットプロセスの名称は、図１７の１６０１に示すように、JobNetである。
【００７１】
ステップ１５０２では、if文の開始と終了部分を生成する。出力例の開始部分は、図１７の１６０２であり、出力例の終了部分は、図１７の１６０５である。
ステップ１５０３では、ジョブネットの全ての終点ジョブの変換名を取得する。ジョブネットの終点ジョブは、処理フロー１１１(図１参照)の情報から取得する。終点ジョブの変換名は、図８に示す要素名変換テーブル８０１を用いて取得する。
ステップ１５０４では、ジョブネットの終点ジョブが全て正常終了状態にある場合、ジョブネットが正常終了状態に遷移する処理を、ステップ１５０２で生成したif文の中のケースとして生成する。具体的には、ガード条件を「全ての終点ジョブがCompleted状態にある」という条件で示し、ガード条件が満たされた場合の処理を、ジョブネットがJN_Completed状態に遷移する処理として記述する。図１７の１６０３が出力例である。終点ジョブはJob１０のみであるが、これは処理フロー例２０１の終点ジョブはジョブIのみであり、ジョブIの変換名は要素名変換テーブル８０１によるとJob10であるためである。
【００７２】
ステップ１５０５から１５０７においては、ジョブのどれか１つが異常終了した場合に、ジョブネットが異常終了状態に遷移する処理を生成する。具体的には、異常終了可能なジョブそれぞれについて、if文のケースを生成する。ケースのガード条件は、該当ジョブが異常終了した場合であり、ガード条件が満たされた場合の処理は、ジョブネットのJN_Completed_Abnormal状態への遷移である。
ステップ１５０５では、異常終了可能なジョブを取得する。これは、処理フロー１１１(図１参照)から、終了判定プロパティが「０」または「−１」であるジョブを取得する。図３に示す処理フロー例２０１では、ジョブＥのみが該当する。
【００７３】
ステップ１５０６においては、選択したジョブが異常終了状態にある場合に、ジョブネットが異常終了状態に遷移する処理を、if文のケースとして生成する。図１７の１６０４がこのステップの出力例である。上記の例の場合、ジョブＥの変換名であるJob5がCompleted_Abnormal状態であることをガード条件とし、ガード条件が満たされた場合の処理はジョブネット状態がJN_Completed_Abnormalに遷移することである。
図３に示す処理フロー例２０１では、異常終了可能なジョブはジョブＥのみであるため、ステップ１５０６は１度しか実行されない。異常終了可能なジョブが複数ある場合は、それぞれについてステップ１５０６が実行される。
以上が、検査用モデル(１２０)生成処理における図１６に示すジョブネットプロセスの定義を生成する生成処理である。
【００７４】
＜検査用モデル(１２０)生成処理におけるリソースプロセスの定義を生成する生成処理＞
次に、検査用モデル生成処理におけるリソースプロセスの定義を生成する生成処理(図１１のステップ１００５)を、図１８、図１９を用いて説明する。
図１８は、検査用モデル生成処理におけるリソースプロセスの定義を生成する処理のフローチャートを示す図であり、図１９は、そのPROMELAのソースコードの出力例である。特に、図１９は、昼用ＡＰに対応するリソースプロセスである、Day_APの定義である。これらを用いてリソースプロセスの定義の生成処理を説明する。この図１９は、昼用ＡＰ３１１(図４参照)に対応するリソースプロセスDay_APのPROMELAのソースコードである。ＡＰのインスタンスは夜用ＡＰ３１２(図４参照)もあるが、対応するリソースプロセスNight_APのPROMELAのソースコードは、シグナチャと終端記号のコメントを除き同一であるので省略する。
【００７５】
図１８のステップ１７０１では、リソースプロセスのシグナチャと終端記号を生成する。図１９の出力例では、１８０１がシグナチャであり、１８１２が終端記号である。
シグナチャは、予約語である「proctype」と、リソースプロセス名(変換名)と、括弧内の引数から構成される。リソースプロセス名(変換名)は、リソース名(要素名)を用いて要素名変換テーブル８０１(図９参照)から取得する。図１９の例は、昼用ＡＰ３１１の例であるので、リソースプロセス名(変換名)はDay_APである。前記の図１４のステップ１３０３の説明で述べたように、リソースプロセスは１つのチャネルを引数として持つ。チャネルは変数chで表す。
【００７６】
図１８のステップ１７０２では、リソースプロセスが行う処理のメインループであるdo文の開始部分と終了部分を生成する。図１９の出力例では、１８０３と１８１０にそれぞれ対応する。
図１８のステップ１７０３からステップ１７０８で、リソースが取り得る状態のそれぞれについて、do文のケースを生成する。Day_APの例では、図５、図１０に示すように、取り得る状態が「AP_Serving」、「AP_Running」、「AP_Stopped」の３つである。
ステップ１７０３では、未選択の状態を選択する。図１９の出力例を用いた説明では、以後「AP_Running」を選択したと想定して説明を行う。
【００７７】
ステップ１７０４では、状態名に基づき、do文のケースのガード条件とエンドラベルとif文を生成する。ガード条件には、当該リソースプロセスが選択した状態にあることを記述する。ステップ１７０４の出力例は、図１９の１８０４である。図１９の出力例では「Day_AP_state == AP_Running」がガード条件となる。エンドラベルは、「end」の後ろに、図１８のステップ１７０３の実行回数をつけたものとする。１度目の実行であるので、エンドラベルは「end1」となる。ガード条件が満たされた場合の処理として、if文を生成する。上記のエンドラベルは、このif文に対して付与する。
【００７８】
ステップ１７０５からステップ１７０７では、現在選択している状態から遷移可能な状態それぞれについて、if文のケースを生成する。ここでの説明では、現在選択している状態から遷移可能な状態を「遷移先状態」と呼称する。
ステップ１７０５では、未選択の遷移先状態を取得する。現在の状態は「AP_Running」であるので、リソース状態遷移情報のリソース状態遷移モデル例４０１(図５参照)と要素名変換テーブル８０１(図９参照)から、「AP_Serving」と「AP_Stopped」の２つの状態が遷移先状態の候補であることが取得できる。図１９の出力例を用いた説明では、ここで後者を選択したと想定する。
【００７９】
図１８のステップ１７０６では、ジョブプロセスからのメッセージ受信をガード条件とし、ステップ１７０５で選択した遷移先状態へリソースプロセスが遷移する処理を、if文のケースとして生成する。このステップ１７０６の出力例が図１９の１８０５である。現在の遷移先状態は「AP_Stopped」であるので、受信するメッセージは「To_AP_Stopped」である。このメッセージの受信を記述したガード条件は「ch?To_AP_Stopped」である。
さらに、現在の状態の「AP_Running」からの遷移先として「AP_Serving」の未選択の状態があるので、ステップ１７０７からステップ１７０５に処理が戻り、「AP_Serving」が遷移先として選択される。図１８のステップ１７０６の処理結果は、図１９の１８０６である。
【００８０】
以上で、図１８のステップ１７０３からステップ１７０８の処理を、「AP_Running」について繰り返した。この一連の処理を「AP_Stopped」について繰り返した場合の出力が、図１９の１８０８であり、「AP_Serving」について繰り返した場合の出力が、図１９の１８０９である。
全ての状態について図１８のステップ１７０３からステップ１７０８を実行した後で、ステップ１７０９を実行し、リソースプロセス内の全ての文を囲むatomic文を生成する。このステップ１７０９のatomic文の出力例が、図１９の１８０２と１８１１である。
図２０は、ＤＢ３２０のインスタンスである昼用ＤＢ３２１に対応するリソースプロセスDay_DBのPROMELAのソースコードである。ＤＢ３２０は、図５に示すように、状態を２つ持ち、それぞれからの遷移先は１つである。よって、do文のケースは２つであり、それぞれif文のケースを１つ持つ。
以上が、検査用モデル生成処理における図１８に示すリソースプロセスの定義を生成する処理である。
【００８１】
＜検査用モデル生成処理のイベントジョブのジョブプロセスの定義を生成する処理＞
次に、検査用モデル(１２０)生成処理におけるイベントジョブのジョブプロセスの定義を生成する処理(図１１のステップ１００８)を説明する。
図２１は、検査用モデル生成処理におけるイベントジョブのジョブプロセスの定義を生成する処理のフローチャートであり、図２２はイベントジョブであるジョブＡ（図３のジョブ２１１）に対応して生成されるPROMELAのソースコードである。これらを用いて、イベントジョブに対応するジョブプロセスの定義の生成処理を説明する。
【００８２】
図２１のステップ２００１では、イベントジョブのジョブプロセスのシグナチャと終端記号とエンドラベルを生成する。図２２の２１０１がシグナチャとエンドラベルの出力例であり、エンドラベルは「end」であり、シグナチャの次の行に生成する。図２２の２１０４が終端記号である。
イベントジョブはリソースへの作用を持たないので、引数を持たない。よって、シグナチャは、予約語「proctype」とジョブプロセス名から構成される。ジョブプロセス名(変換名)は、処理フロー１１１の情報(図３のジョブフロー例参照)から取得するジョブＩＤ(図３参照)と図９の要素名変換テーブル８０１に基づいて取得する。
【００８３】
図２１のステップ２００２では、ジョブプロセスがRunning状態へ遷移するソースコードを生成する。生成結果は、図２２の２１０２である。ガード条件は、常に真であるskip文を使用する。
図２１のステップ２００３では、ジョブプロセスがCompleted状態へ遷移するソースコードを生成する。生成結果は、図２２の２１０３である。イベントジョブは異常終了しないので、異常終了のケースは考慮しない。
以上が、検査用モデル(１２０)生成処理における図２１に示すイベントジョブの定義を生成する処理である。
【００８４】
前記したように、図２２は図３のジョブＡに対応するジョブプロセスのPROMELAのソースコードである。図３に示すジョブＢもイベントジョブであるが、それに対応するPROMELAのソースコードは、図２２とほぼ同じであり、相違点はジョブプロセス名称(図９に示す変換名)のみである。
【００８５】
＜検査用モデル生成処理におけるORジョブのジョブプロセスの定義を生成する処理＞
次に、検査用モデル(１２０)生成処理におけるORジョブに対応するジョブプロセスの定義の生成処理(図１１のステップ１００８)を、図２３、図２４を用いて説明する。
図２３は、ORジョブの定義を生成する処理のフローチャートであり、図２４は、ORジョブであるジョブＣ(図３のジョブ２１３)に対応して生成されるPROMELAのソースコードである。
図２３のステップ２２０１では、イベントジョブのジョブプロセスのシグナチャと終端記号とエンドラベルを生成する。この出力例は、図２４の２３０１と２３０４である。この部分は、図２１に示すイベントジョブの場合と同様である。
【００８６】
図２３のステップ２２０２では、先行ジョブの１つ以上が正常終了状態にある場合にジョブプロセスがRunning状態へ遷移するソースコードを生成する。「先行ジョブの１つ以上が正常終了状態」をガード条件として記述する。具体的には、各先行ジョブについて、そのジョブが正常終了であるという条件式を生成し、それら全ての論理和をガード条件とする。
ジョブＣの場合、ジョブＡとジョブＢという２つの先行ジョブを持つので、ガード条件は２つの論理式の論理和となる。生成結果は、図２４の２３０２である。先行ジョブは、処理フロー１１１(図３の処理フロー例２０１参照)から取得し、先行ジョブの変換名は、図９に示す要素名変換テーブル８０１に基づいて取得する。
【００８７】
ステップ２２０３では、ジョブプロセスがCompleted状態へ遷移するソースコードを生成する。生成結果は、図２４の２３０３である。ORジョブは異常終了しないので、異常終了のケースは考慮しない。
以上が、検査用モデル(１２０)生成処理における図２３に示すORジョブに対応するジョブプロセスの定義の生成処理である。
【００８８】
＜検査用モデル生成処理における判定ジョブのジョブプロセスの定義を生成する処理＞
次に、検査用モデル(１２０)生成処理における判定ジョブのジョブプロセスの定義を生成する処理(図１１のステップ１００８)、すなわち判定ジョブに対応するジョブプロセスの定義の生成処理を、図２５、図２６を用いて説明する。
図２５は、判定ジョブのジョブプロセスの定義を生成する処理のフローチャートであり、図２６は、判定ジョブであるジョブＤ（図３のジョブ２１４）に対応して生成されるPROMELAのソースコードである。
図２５のステップ２４０１では、判定ジョブのジョブプロセスのシグナチャと終端記号とエンドラベルを生成する。出力例は図２６の２５０１と２５０４である。このステップ２４０１は、図２１に示すイベントジョブ、図２３に示すORジョブの場合と同様である。
【００８９】
ステップ２４０２では、全ての先行ジョブが正常終了状態にある場合にジョブプロセスがRunning状態へ遷移するソースコードを生成する。具体的には、各先行ジョブについて、そのジョブが正常終了であるという条件式を生成し、それら全ての論理積をガード条件とする。図３に示すように、ジョブＤの場合、ジョブＣのみが先行ジョブであるので、ガード条件は論理積を使用する必要がない。生成結果例は、図２６の２５０２である。先行ジョブは、処理フロー１１１(図１参照)(図３に示す処理フロー例２０１)から取得し、先行ジョブの変換名は、図９に示す要素名変換テーブル８０１に基づいて取得する。
【００９０】
ステップ２４０３では、ジョブプロセスが非決定的にCompleted_True状態またはCompleted_False状態へ遷移するソースコードを生成する。非決定的な処理は、ケースがガード条件を持たないようなif文を用いて表現する。これは、判定結果による分岐をモデル化したものである。実際の判定を行わず、真である場合と偽である場合の両方の振る舞いが可能であることのみをモデル化している。判定ジョブの終了状態がCompleted_TrueとCompleted_Falseであることは、図８とその説明を参照のこと。ステップ２４０３の生成結果例は、図２６の２５０３である。判定ジョブは異常終了しないので、異常終了のケースは考慮しない。
以上が、検査用モデル(１２０)生成処理における図２５に示す判定ジョブの定義を生成する処理である。
【００９１】
＜検査用モデル生成処理における標準・アクションジョブ・従属ジョブプロセスの定義の生成処理＞
次に、検査用モデル(１２０)生成処理における標準ジョブとアクションジョブと従属ジョブのジョブプロセスの定義の生成処理(図１１のステップ１００８)を、図２７、図２８を用いて説明する。
図２７は、標準ジョブとアクションジョブと従属ジョブのジョブプロセスの定義を生成する処理のフローチャートであり、図２８は、標準ジョブであるジョブＦ（図３のジョブ２１６）に対応して生成されるPROMELAのソースコードである。
図２７のステップ２６０１では、ジョブプロセスのシグナチャと終端記号とエンドラベルを生成する。リソースに対して作用する標準ジョブの場合、ジョブプロセスの引数としてチャネルを持たせる。チャネル名は、図１４のステップ１３１０と図１５の１４０６で説明した方法で取得する。
【００９２】
すなわち、チャネルの情報は、図６に示すジョブ作用テーブル例５０１(ジョブ作用情報１１４(図１参照))から抽出する。複数のリソースに対して作用するジョブの場合は、複数のチャネルを引数として持つ。この場合、引数の順番は、図１４のステップ１３１０で生成した順番と同じであるようにする。ジョブＦ(図９参照)の例では、図２８の２７０１と２７０４が対応する。特に、ジョブＦは、図６に示すジョブ作用テーブル例５０１によると、１つのリソースに対して作用するので、１つのチャネルが引数となっている。
【００９３】
図２７のステップ２６０２では、該当ジョブが実行可能となった場合にジョブプロセスがRunning状態へ遷移するソースコードを生成する。該当ジョブが実行可能となる条件は、先行ジョブに判定ジョブが含まれない場合は、全ての先行ジョブが正常終了状態にある場合である。これに対して、先行ジョブに判定ジョブが含まれる場合は、該当ジョブが標準ジョブであるか従属ジョブであるかに依存する。該当ジョブが標準ジョブである場合は、判定ジョブがCompleted_False状態にある場合または判定ジョブに付随する従属ジョブが正常終了状態にある場合に、該当ジョブが実行可能となる。該当ジョブが従属ジョブである場合は、判定ジョブがCompleted_True状態にある場合に、該当ジョブが実行可能となる。なお、ガード条件の生成方法は、既に前記した通りである。
【００９４】
この図２７のステップ２６０２の出力例は、図２８の２７０２である。
標準ジョブに対応するジョブプロセスは、Running状態からCompleted状態に遷移する前に、作用対象であるリソースへ状態遷移を促すメッセージを送信し、自身の状態遷移を行う。
図２７のステップ２６０３からステップ２６０５は、作用対象であるリソースそれぞれに対し、状態遷移を促すメッセージを送信するソースコードを生成するステップである。
ステップ２６０３と２６０４では、未選択の作用対象リソースを取得する。作用対象リソースは、ジョブ作用情報１１４(図１参照)であるジョブ作用テーブル例５０１(図６参照)から取得する。図６に示すジョブＦの例では、夜用ＡＰが唯一の作用対象リソースであるのでこれを選択する。
【００９５】
ステップ２６０５では、選択した作用対象リソースへ遷移メッセージを送信するソースコードを生成する。作用対象リソースの遷移先状態は、ジョブ作用情報１１４(図１参照)において、ジョブ作用テーブル例５０１(図６参照)のように定義されている。ジョブＦの例では、図２８の２７０３の１行目に該当する。送信すべきメッセージは、「To_」の後に遷移先状態の変換名を付けた文字列である。ジョブＦの例においては、夜用ＡＰを稼働中状態にするためのメッセージであるので、「To_AP_Running」を送信する。メッセージ送信のためのPROMELAのソースコードは、チャネル名に「!」をつけ、その後ろにメッセージ名をつけたものである。
【００９６】
図２７のステップ２６０６では、正常終了可能なジョブであるか否かを判定する。これは、処理フロー１１１(図３の処理フロー例２０１参照)における該当ジョブの終了判定プロパティが「１」または「０」である場合に真となる。
ステップ２６０７では、ジョブプロセスが正常終了状態に遷移するため、Completed状態に遷移するソースコードを生成する。例では、図２８の２７０３の２行目に該当する。
ステップ２６０８では、ジョブプロセスが異常終了可能なジョブであるかを判定する。これは、処理フロー１１１(図３の処理フロー例２０１参照)における該当ジョブの終了判定プロパティが「０」または「−１」である場合に真となる。
【００９７】
ステップ２６０９では、ジョブプロセスが異常終了状態に遷移するため、Completed_Abnormal状態に遷移するソースコードを生成する。図２８には該当するソースコードは、例示していない。
ステップ２６１０では、ジョブプロセスが正常終了と異常終了の両方が可能なジョブであるかを判定する。これは、処理フロー１１１(図３の処理フロー例２０１参照)における該当ジョブの終了判定プロパティが「０」である場合に真となる。
ステップ２６１１では、ジョブプロセスが非決定的に正常終了または異常終了を選択するif文を生成する。図２８には該当するソースコードは、例示していない。
以上が、図２７に示す標準ジョブ、アクションジョブ、従属ジョブに対応するジョブプロセスを生成する手順の説明である。
【００９８】
図２９は、ジョブＩ（図３のジョブ２１９）に対応するジョブプロセスの定義である。これは、作用対象リソースが２つあるジョブのジョブプロセスの例である。図６に示すジョブ作用テーブル例５０１によると、ジョブＩは、昼用ＡＰを稼働状態にし、夜用ＡＰをリクエスト対応状態にする作用を持つ。この性質は、図２９の２８０３において２つのメッセージ送信が行われることに反映されている。
図３０は、ジョブＪ（図３のジョブ２２０）に対応するジョブプロセスの定義である。これは、作用対象リソースがないジョブに対応するジョブプロセスのソースコード例である。
【００９９】
図３１は、ジョブＥ（図３のジョブ２１５）に対応するジョブプロセスの定義であり、従属ジョブに対応するソースコードの例である。図３１の３００２のガード条件において、判定ジョブである先行ジョブの状態がCompleted_Trueである場合に実行可能となることを反映している。
以上が、図１に示す検査用モデル生成部１０１が行う処理の説明である。
前記したように、検査用モデル生成部１０１の出力の１つである検査用モデル１２０は１つのテキストファイルとして記述されたPROMELAプログラムである。検査用モデル生成部１０１は、さらに、設計情報１１０に基づいて、図９に示す要素名変換テーブル８０１と図１０に示すリソース状態名変換テーブル９０１をモデル関連情報１２１として出力する。
【０１００】
＜設計支援装置１００のモデル検査部１０２＞
次に、図１に示す設計支援装置１００におけるモデル検査部１０２が行う処理を説明する。
図３２は、処理フローと業務要件の整合性を確認する機能を設計者が起動する方法の一例を示したジョブネット設計画面３１０１の図である。
ジョブネットを設計するジョブネット設計画面３１０１の上部に、状態遷移整合性の検査を実行するために押下される状態遷移整合性の検証ボタン３１０２、事後条件の検査を実行するために押下される事後条件の検証ボタン３１０３、不変条件の検査を実行するために押下される不変条件の検証ボタン３１０４がある。
【０１０１】
以下に、状態遷移整合性の検証ボタン３１０２を押下し、状態遷移整合性の検証を行った場合の処理を説明する。事後条件と不変条件については、第２実施形態と第３実施形態でそれぞれ説明する。
状態遷移整合性とは、処理フロー例２０１(図３参照)が、リソース状態遷移モデル例４０１(図５参照)と整合している性質である。
本第１実施形態での検査用モデル１２０においては、状態遷移整合性は、PROMELAで記述された検査用モデル１２０がデッドロック状態を持たないことで表現されている。図１に示すモデル検査エンジン１０３の例であるSpinは、PROMELAモデルがデッドロックを起こさないことを検証する機能を備えており、検査性質１２５を新たに入力する必要はない。よって、検査性質１２５では単に、Spinにデッドロックの不在を検証させるためのコマンドを有していればよい。
【０１０２】
設計者が、図３２に示すジョブネット設計画面３１０１の状態遷移整合性の検証ボタン３１０２を押下すると、モデル検査部１０２は、検査性質１２５に保存されているデッドロック検証のコマンドを、モデル検査エンジン１０３（Spin）に対して発行する。モデル検査エンジン１０３（Spin）は、状態遷移整合性に係るモデル検査を行い、その結果を出力する。モデル検査部１０２は、その出力情報のうち、設計者にフィードバックするべき情報を取得し、検査結果１２２として出力する。
【０１０３】
ここで、検査用モデル１２０にデッドロックが存在しない場合、検査結果１２２はその事実のみを記述する。検査用モデル１２０にデッドロックが存在する場合、検査用モデル１２０はデッドロックに至る実行パスの情報を検査結果１２２として出力する。実行パスとは、ジョブネットが実行を開始した状態から各ジョブが順次実行してゆく過程を表す情報である。
この場合にモデル検査部１０２が出力する検査結果１２２の例を図３３に示す。
図３３は、Spinのグラフィカル・インターフェイスであるXspinが出力するデータバリュー情報を示す図である。これは、検査用モデル１２０がデッドロック状態にある時の状態変数の値を表す。例えば、図３３の３２１３の１行目は、状態変数Day_AP_stateの値はAP_Servingであることを示す。
【０１０４】
＜処理フロー状態生成部１０４＞
次に、図１に示す処理フロー状態生成部１０４が行う処理を説明する。
処理フロー状態生成部１０４は、検査結果１２２と設計情報１１０とモデル関連情報１２１を入力とし、状態遷移整合性が破られた時点でのジョブネットとジョブとリソースの状態をそれぞれ示す処理フロー状態１２３を出力する。
図３４は、処理フロー状態生成部１０４が出力した処理フロー状態１２３の出力例を示す図である。
図３４に示す処理フロー状態１２３は、図２のディスプレイ３６０５の画面上に表示される。
【０１０５】
図３４の処理フロー状態１２３の３３１１は、状態遷移整合性が破られた時点でのジョブネットの状態を示し、図３４の３３１２は、状態遷移整合性が破られた時点でのジョブの状態を示し、図３４の３３１３は、状態遷移整合性が破られた時点でのリソースの状態を示す。
図３４の処理フロー状態１２３の３３１１は、図３３のデータバリュー情報(検査結果１２２)の３２１１の右辺をジョブネットの状態として取得することができる。
【０１０６】
図３４の処理フロー状態１２３の３３１２は、図３３の３２１２のそれぞれの行のジョブプロセス名を、図９に示す要素名変換テーブル８０１に基づいて、処理フロー１１１(図３の処理フロー例２０１参照)におけるジョブＩＤに変換することで取得する。ここで、要素名変換テーブル８０１(図９参照)の「要素名」はジョブＩＤに相当し、「変換名」はジョブプロセス名に相当する。
図３４の処理フロー状態１２３の３３１３は、図３３の３２１３のそれぞれの行の左辺をリソース構造モデル１１２(図１参照)のリソース構造モデル例３０１(図４参照)におけるリソース名に変換し、図３３の３２１３の右辺をリソース状態遷移モデル１１３(図１参照)のリソース状態遷移モデル例４０１(図５参照)における状態名に変換することで取得する。
【０１０７】
ここで、図３３の３２１３の左辺の変換は、要素名変換テーブル８０１(図９参照)に基づいて、変換名であるリソースプロセス名に対応する要素名を取得することで行われる。この時、要素名はリソース名に相当する。図３３の３２１３の右辺の変換は、リソース状態名変換テーブル９０１(図１０参照)に基づいて、図３３の３２１３の右辺の変換名に対応する状態名を取得することで行われる。
以上が、図１に示す処理フロー状態生成部１０４が行う処理である。
【０１０８】
設計者は、図３４の処理フロー状態１２３から、ジョブＧを実行する時点でリソース状態遷移モデル１１３との不整合が顕在化する実行パスが存在することがわかる。ジョブＧは昼用ＡＰを停止状態にする作用を持つ(図３参照)が、その実行パスでは、ジョブＧの実行時に昼用ＡＰはリクエスト対応状態(図３４の３３１３の１行目参照)にあり、停止状態に遷移することができないためである。
このように、本第１実施形態によれば、ジョブネットとリソース状態遷移モデル１１３(図１参照)の不整合を自動検知し、設計者によるジョブネット設計作業を支援することができる。
【０１０９】
図３５は、処理フロー状態１２３を表示する処理フロー状態画面３４０１を示す図である。
処理フロー状態画面３４０１は、処理フロー例２０１(図３参照)の各ジョブそれぞれの上に、状態遷移整合性が破られた時点での状態を表示している。既に実行を終了したジョブは、灰色で示しており(図３５中、網掛けで示す)、ジョブネットのどの部分までが実行済みかがわかる。ジョブＧが実行中であり、ジョブＨとジョブＩとジョブＪは未実行である。
すなわち、図３５の処理フロー状態画面３４０１は、ジョブＧが終了できないことを示しており、ジョブＧで何らかのエラーが発生したことが分る。
【０１１０】
図３６は、状態遷移整合性が破られた時点でのリソースの状態を表示するリソース状態画面３５０１を示す図である。
図３６のリソース状態画面３５０１は、リソース構造モデル１１２(図４のリソース構造モデル例３０１参照)で定義された各リソースのリソース状態遷移モデル１１３(図５のリソース状態遷移モデル例４０１参照)を表示し、処理フロー状態１２３から取得した各リソースの状態を色付きで示す(図３６、網掛けで示す)。このリソース状態画面３５０１では、状態遷移整合性が破られた時点では、昼用ＡＰはリクエスト対応状態にあり、夜用ＡＰは稼動状態にあることが、設計者により目視され、処理フローに状態遷移整合性(処理フロー例２０１(図３参照)が、リソース状態遷移モデル例４０１(図５参照)と整合している性質)に係るエラーが存在することを発見できる。
【０１１１】
＜＜第２実施形態＞＞
次に、本発明の第２実施形態として、実施形態で説明する処理フロー１１１(処理フロー例２０１(図３参照))が満たすべき条件の業務要件、すなわち、状態遷移整合性(第１実施形態で説明)、事後条件、不変条件のうちの事後条件について、説明する。
第２実施形態では、設計者による事後条件の記述、および設計支援装置１００による事後条件の検査を説明する。
【０１１２】
＜＜設計支援装置１００による事後条件の検査＞＞
図３７は、第２実施形態の図２に示す処理フロー例２０１を修正し、状態遷移整合性を持つようにした新しい第２処理フロー例３７０１を示した図である。
第２処理フロー例３７０１と処理フロー例２０１との相違点は、図２に示す処理フロー例２０１のジョブＧ（ジョブ２１７）とジョブＩ（ジョブ２１９）とジョブＪ（ジョブ２２０）を、それぞれ図３７に示す第２処理フロー例３７０１のジョブＧＡ（ジョブ３７１７）とジョブＩＡ８（ジョブ３７１９）とジョブＪＡ（ジョブ３７２０）に変更した点である。
【０１１３】
図３８に示す第２ジョブ作用テーブル例３８０１は、図６に示すジョブ作用テーブル例５０１を図３７の第２処理フロー例３７０１に整合するよう修正をした結果である。図３８の第２ジョブ作用テーブル例３８０１の２行目、３行目、５行目のジョブＩＤのみ修正されている。
図３７の第２処理フロー例３７０１では、図２の処理フロー例２０１が持っていた状態遷移不整合性を排除してある。これは、昼用ＡＰを停止する作用を持つジョブが実行される前に、昼用ＡＰをリクエスト対応状態から稼動状態に遷移させる作用を持つジョブ（ジョブＧＡ「Ｗｅｂサーバ切替」３７１７）を実行するように変更したことによる。
【０１１４】
第２処理フロー例３７０１に対するリソース構造モデル１１２(図４のリソース構造モデル例３０１参照)とリソース状態遷移モデル１１３(図５のリソース状態遷移モデル例４０１参照)に変更は無い。
以下の実施例では、第２処理フロー例３７０１、リソース構造モデル例３０１(図４参照)、リソース状態遷移モデル例４０１(図５参照)、ジョブ作用情報の第２ジョブ作用テーブル例３８０１(図３８参照)から、検査用モデル生成部１０１が生成する検査用モデル１２０を用いて説明する。
検査用モデル１２０の生成方法には変更は無いため、この新しい検査用モデル１２０についての詳細は省略する。
第２処理フロー例３７０１(図３７参照)を入力情報として、図１に示す業務要件１２４、業務要件記述支援部１０５、検査性質生成部１０６、検査性質１２５について説明する。
【０１１５】
＜業務要件記述支援部１０５＞
業務要件記述支援部１０５は、処理フロー１１１が満たすべき要件の設計者による記述を支援する。
図３９は、第２実施形態の設計者が業務要件１２４を入力することができる業務要件入力画面３９０１を示す図である。
設計者は、業務要件入力画面３９０１のテキストボックス３９１１に業務要件名をテキスト入力し、種別プルダウンメニュー３９１２で業務要件１２４の種別を選択する。
【０１１６】
業務要件１２４の選択可能な種別は、事後条件と不変条件の２種類である。事後条件とは、ジョブネットが正常終了した時点で満たしているべき性質であり、不変条件とは、ジョブネットが起動されて正常終了に至る間の全ての時点において常に満たされているべき性質である。例えば、不変条件とは、ＡＰが稼動状態にあるとき、該ＡＰに対応するＤＢは、停止状態でなく、稼働状態にある等である。
図３９の業務要件入力画面３９０１では、設計者が事後条件を選択した場合を示している。
【０１１７】
業務要件入力画面３９０１の論理式テキストボックス３９１３に、設計者は条件要素を組み合わせるための論理式を入力する。図３９の例では、設計者は、番号１から４で示されている４つの条件要素の論理積を入力している。ここで、論理積は「＆＆」、論理和は「｜｜」、論理否定は「！」、論理包含は「→」または「->」で表される。
業務要件入力画面３９０１の条件要素テキスト３９１４は、設計者によって入力済みである条件要素が表示される。各条件要素がそれぞれ１つの行に表示されている。条件要素の記述形式は、「ＡはＢ状態にある」であり、Ａ(３９１４ａ)にはリソースまたはジョブが、Ｂ(３９１４ｂ)にはＡに記入したリソースまたはジョブが取り得る状態が入る。
【０１１８】
条件要素テキスト３９１４に表示される条件要素の記述は、業務要件入力画面３９０１の下部の複数のプルダウンメニューを用いて行う。リソース・ジョブプルダウンメニュー３９１６では、上記の条件要素のＡ(３９１４ａ)に相当するリソースまたはジョブを選択する。
図３９に示すリソース・ジョブプルダウンメニュー３９１６では、設計者が「切替メール送信」ジョブを選択した場合を示している。
状態プルダウンメニュー３９１７の内容は、リソース・ジョブプルダウンプルダウンメニュー３９１６の選択内容(リソースまたはジョブ)に基づいて表示される。すなわち、状態プルダウンメニュー３９１７には、リソースの状態(図５参照)またはジョブの状態(図８参照)が表示される。
【０１１９】
業務要件入力画面３９０１のリソース・ジョブプルダウンメニュー３９１６では、「切替メール送信」ジョブが選択されているので、状態プルダウンメニュー３９１７には、「切替メール送信」ジョブが取り得る状態が選択肢として示されている。設計者は、状態プルダウンメニュー３９１７にRunning状態を選択している。
そして、設計者は、条件の追加ボタン３９１８を押下することで、業務要件入力画面３９０１のリソース・ジョブプルダウンメニュー３９１６、状態プルダウンメニュー３９１７で入力した条件要素をワークエリアに保存することができる。
保存した条件要素は、図３９に示すように、条件要素テキスト３９１４に表示され、論理式テキストボックス３９１３に記述する論理式で使用可能となる。
こうして、ジョブの状態に関する命題とリソースの状態に関する命題とを組み合わせて表現した処理フロー１１１が満たすべき性質の情報がコンピュータの設計支援装置１００に入力される。すなわち、論理式で表され、使用可能となる。
【０１２０】
設計者が、業務要件入力画面３９０１上部の保存ボタン３９１９を押下すると、業務要件記述支援部１０５(図１参照)は、業務要件入力画面３９０１で設計者が記述した要件を、図１に示す業務要件１２４に保存する。
上述した如く、業務要件記述支援部１０５は、設計者による業務要件１２４の記述を支援する。
【０１２１】
図３９の業務要件入力画面３９０１で、設計者が記述(入力)した事後条件とは、第２処理フロー例３７０１(図３７参照)(図３に示す処理フロー例２０１を修正したもの)が正常終了した時点で、昼用ＡＰと昼用ＤＢは停止状態にあり、夜用ＡＰはリクエスト対応状態であり、夜用ＤＢは稼働状態にあるというものである。
第２処理フロー例３７０１(図３７参照)の目的は、昼系から夜系への切り替えであるので、この事後条件を検査することで、第２処理フロー例３７０１(図３７参照)(図３に示す処理フロー例２０１を修正したもの)の実行結果が、その業務要件の一つの事後条件に合致することを検査することができる。
【０１２２】
＜検査性質生成部１０６＞
次に、図１に示す検査性質生成部１０６が行う処理を説明する。
検査性質生成部１０６は、業務要件１２４とモデル関連情報１２１を入力とし、検査性質１２５を出力する。検査性質１２５は、モデル検査部１０２の入力の一部となるものであり、検査用モデル１２０が満たすべき性質を記述するものである。
前記した検査用モデル１２０と同様に、検査性質１２５は、モデル検査部１０２が使用するモデル検査エンジン１０３が想定する形式で記述する必要がある。本実施形態では、モデル検査エンジン１０３はSpinであるので、検査性質１２５はSpinが想定する形式で記述する。
【０１２３】
図４０は、第２実施形態の検証性質生成部１０６(図１参照)が、業務要件１２４に格納されている事後条件をSpin向けの検査性質１２５に変換する手順を示したフローチャートである。図４１は、図３９に記載の事後条件を、図４０のフローチャートに従って検証性質生成部１０６が変換した結果のソースコードを示す図である。
検証性質生成部１０６による業務要件１２４に格納されている事後条件をSpin(モデル検査エンジン１０３)向けの検証性質に変換する手順を、図４１のソースコードを用いながら、図４０のフローチャートに従って、説明する。
【０１２４】
図４０のステップ４００１では、図４１の４１１１のdefine文を生成する。これは、ジョブネットが正常終了している状態でのみ「真」となる式に対し、f0という名称を定義するdefine文である。
ステップ４００２からステップ４００４は、事後条件の論理式を構成する条件要素それぞれについて、define文を生成する処理である。
図３９の説明で述べた通り、条件要素は「ＡはＢ状態にある」との形式であり、Ａはジョブまたはリソースで、ＢはＡが取り得る状態である。define文は、図４１の４１１２のように、条件要素を変換名で記述した式に対し、ｆＮという名称を付与するものであり、Ｎ(Ｎ：正の整数)は条件要素番号である。
【０１２５】
条件要素から式への変換のやり方は以下の通りである。条件要素のＡはジョブまたはリソースであるので、その変換名を要素名変換テーブル８０１(図９参照)から取得する。これを式の左辺とする。条件要素のＢはＡの取り得る状態である。Ａがジョブの場合は、変換をする必要がないので、そのまま式の右辺とする。Ａがリソースの場合は、リソース状態名変換テーブル９０１(図１０参照)に基づいて、状態名に対応するリソースプロセスの状態を変換名から取得し、これを式の右辺とする。
【０１２６】
図４０のステップ４００５では、条件要素を構成要素とする論理式を生成し、これをＦと呼称する。これは、図３９の論理式テキストボックス３９１３に設計者が入力した情報に基づく。設計者が入力した論理式は、条件要素の番号(図３９参照)を構成要素とする論理式である。条件要素の番号の前に「ｆ」を付与すると、図４０のステップ４００３で生成したdefine文が定義する式の名称になる。図３９の事後条件の例では、F(論理式)は、「f1 && f2 && f3 && f4」である。
【０１２７】
ステップ４００６では、ステップ４００５で定義したFを用いて、「[]f0->F」という式を出力する。出力結果の例は図４１の４１１３である。ここで、[]は時相論理のオペレータであり、「常に」という意味である。式全体の意味は、「常に以下が成り立つ。ジョブネットが正常終了状態にあるならば、Fである」である。これが、事後条件に対応する検査性質である。
以上が、図４０に示す検証性質生成部１０６による業務要件１２４に格納されている事後条件をSpin(モデル検査エンジン１０３)向けの検査性質１２５に変換する手順である。
【０１２８】
設計者が事後条件の検査を実行する方法の１つに、前記の図３２に示すジョブネット設計画面３１０１がある。ジョブネット設計画面３１０１の上部の事後条件の検証ボタン３１０３を押下することで、モデル検査部１０２は、検査性質１２５に保存されている事後条件に係る検査性質をモデル検査エンジン１０３（Spin）に入力として与え、モデル検査処理を実行させ、事後条件の検査を開始させる。
一方、設計者が状態遷移整合性の検証ボタン３１０２を押下すると、モデル検査部１０２は、検査性質１２５に保存されている状態遷移整合性に係る検査性質をモデル検査エンジン１０３（Spin）に入力として与え、モデル検査処理を実行させる。
【０１２９】
こうして、モデル検査エンジン１０３（Spin）が出力する事後条件の検査結果、状態遷移整合性の検査結果等から設計者に提示すべき情報を抽出し、検査結果１２２(図１参照)として出力する。
図４２に、図４１の検査性質の検証を、第２処理フロー例３７０１(図３７参照)、リソース構造モデル例３０１(図４参照)、リソース状態遷移モデル例４０１(図５参照)、第２ジョブ作用テーブル例３８０１(図３８参照)から検査用モデル生成部１０１が生成した検査用モデル１２０に対して行った場合に出力される検査結果４２０１を示す。
【０１３０】
図３７に示す第２処理フロー例３７０１は、上記の事後条件(図３９に示す昼用ＡＰ・昼用ＤＢは停止状態かつ夜用ＡＰはリクエスト対応状態かつ夜用ＤＢは稼動状態)を満たしていないため、検査結果４２０１はその反例となる情報である。図４２の４２１３の２行目の  Day_DB_state=DB_Running  が事後条件を満たしていない。
図４３に、図４２の検査結果４２０１から処理フロー状態生成部１０４(図１参照)が生成する処理フロー状態４３０１を示す。処理フロー状態生生成部１０４の詳細は前記した通りである。
図４３の４３１３の２行目が「昼用DB==稼働状態」となっていることから昼用ＤＢが停止状態となっておらず稼動状態であることが分る。
【０１３１】
これは、第２処理フロー例３７０１(図３７参照)が正常終了した時点で、昼用ＤＢが稼働状態にある実行パスが存在することを示している。設計者は、この検査結果を目視することにより、第２処理フロー例３７０１(図３の処理フロー例２０１を修正したもの)を修正する必要があることが分る。
上記第２実施形態によれば、ジョブネットが、設計者が入力した事後条件を満たさない場合にその反例を処理フロー状態４３０１(図４３参照)に自動的に出力し、設計者によるジョブネット設計作業を支援することができる。
【０１３２】
＜＜第３実施形態＞＞
次に、本発明の第３実施形態として、実施形態で説明する処理フロー１１１(処理フロー例２０１(図３参照))が満たすべき条件の業務要件、すなわち、状態遷移整合性(第１実施形態で説明)、事後条件(第２実施形態で説明)、不変条件のうちの不変条件について、説明する。
第３実施形態では、設計者による不変条件の記述と、設計支援装置１００による不変条件の検査を説明する。
【０１３３】
図４４に、業務要件を入力することができる業務要件入力画面４４０１を示す。業務要件入力画面４４０１は、事後条件を入力する業務要件入力画面３９０１と同じであるので詳細な説明は省略する。
設計者は、種別プルダウンメニュー４４１１で不変条件を選択することで、不変条件を入力することができる。
業務要件入力画面４４０１で設計者が入力した不変条件の意味は以下の通りである。「常に以下が成り立つ。夜用ＡＰがリクエスト対応状態または稼働状態にあるならば、夜用ＤＢは稼働状態にある」。これは、ＡＰが稼働している間は、そのＡＰが使用するＤＢも稼働していなければ、障害の原因となってしまうからである。
【０１３４】
＜検査性質生成部１０６が、業務要件１２４の不変条件を検査性質に変換する手順＞
次に、図１に示す検査性質生成部１０６が、業務要件１２４に格納されている不変条件を検査性質１２５に変換する手順を、図４５に示すフローチャートと図４６に示す検査性質１２５の出力例を用いて説明する。
なお、図４５は、検査性質生成部１０６による不変条件の検査性質を生成するためのフローチャートを示す図であり、図４６は、図４５に示す検査性質生成部１０６による不変条件の検査性質を生成するための検査性質１２５の出力例を示す図である。
【０１３５】
図４５に示すフローチャートは、図４０のフローチャートとほぼ同じであるので詳細な説明は省略する。図４５のフローチャートと図４０のフローチャートとの相違点は、ジョブネットの状態に関する式を生成しない点(図４０の４００１参照)と、最終的な検証式が「常にF」という意味の[]Fの形式である(図４５の４５０６参照)ことである。
図４７は、図４６に示す検査性質４６０１(１２５)の検査を行った際に、モデル検査部１０２(図１参照)が出力する検査結果４７０１を示している。第２処理フロー例３７０１(図３７参照)は上記の不変条件を満たしていないため、図４７の検査結果４７０１はその反例となる情報である。
【０１３６】
図４８に、検査結果４７０１(図４７参照)(１２２)から処理フロー状態生成部１０４(図１参照)が生成する処理フロー状態４８０１(１２３)を示す。処理フロー状態生成部１０４の詳細は前記した通りである。
設計者は、この検査結果４７０１(図４７参照)を目視することにより、第２処理フロー例３７０１を実行すると、不変条件が満たされない実行パスがあることがわかる。さらに処理フロー状態４８０１(図４８参照)を見ることで、ジョブＧＡ(Ｆ)が正常終了した時点で夜用ＡＰが稼働状態にあるにも拘らず、夜用ＤＢが停止状態にあることがわかる。
上記第３実施形態によれば、ジョブネットが、設計者が入力した不変条件を満たさない場合にその反例を処理フロー状態４８０１(図４８参照)に自動的に出力し、設計者によるジョブネット設計作業を支援することができる。
【０１３７】
＜＜第４実施形態＞＞
次に、本発明の第４実施形態について、図４９を用いて説明する。
なお、図４９は、本実施形態である設計支援装置４９００の概略を示した図である。
第４実施形態は、第１〜第３実施形態と異なり、図４９に示すように、設計支援装置４９００におけるモデル検査部４９０２が複数のモデル検査エンジン４９０３Ａと４９０３Ｂを使用したものである。
図４９では２つのモデル検査エンジン４９０３Ａ、４９０３Ｂのみを示しているが、３つ以上のモデル検査エンジンを使用してもよい。モデル検査エンジンとしては、第一の形態で使用したSpinやＳＭＶなどが考えられる。
第４実施形態においては、設計者は、設計支援装置４９００が使用すべきモデル検査エンジンを選択することができる。
【０１３８】
モデル検査エンジンを選択する手段は、複数のモデル検査エンジン４９０３Ａと４９０３Ｂを画面に表示し、それぞれのモデル検査エンジン４９０３Ａ、４９０３Ｂに対応する選択チェックボックスを表示し、設計者が選択チェックボックスにチェックを入れることにより、該選択情報が設計支援装置４９００に入力される。そして、入力された選択情報によりモデル検査部４９０２がモデル検査エンジン４９０３Ａ、４９０３Ｂのうちの少なくとも何れかを選択することにより実現することができる。その他、モデル検査エンジンを３つ以上の場合も同様に実現できる。
ところで、検査用モデル生成、検査性質生成、処理フロー状態生成の処理はモデル検査エンジンの入出力の形式に依存する。これらの依存性の情報、すなわち、検査用モデル生成方法情報と検査性質生成方法情報と処理フロー状態抽出方法情報は、モデル検査エンジン依存情報４９０９に保存されている。
【０１３９】
設計支援装置４９００においては、検査用モデル生成部４９０１と、検査性質生成部４９０６と、処理フロー状態生成部４９０４は、モデル検査エンジン依存情報４９０９を参照し、検査用モデル４９２０の生成、検査性質４９２５の生成、処理フロー状態４９２３の生成を行う。
モデル検査エンジン依存情報の例は、第１実施形態から第３実施形態を説明するために用いたフローチャート(図１１、図４０、図４５等)で示されている処理手順情報である。
これらは、モデル検査エンジンがSpinである場合の処理手順を示したものであり、図４９に示すモデル検査エンジン４９０３ＡがＳＭＶである場合には、モデル検査エンジン依存情報４９０９が持つＳＭＶ向けの処理手順情報を用いて処理を行う。
上記第４実施形態によれば、設計者は複数のモデル検証エンジンの使用法に習熟する必要なしに、ジョブネットの検証を複数のモデル検証エンジンを用いて行うことができる。
【０１４０】
＜＜作用効果＞＞
第１〜第４実施形態の設計支援装置によれば、処理フローの設計情報から処理フローを検査するための検査用モデルを生成することができる。また、業務要件を、処理フローが満たすべき性質として表現し、それを検査用モデルが満たすべき検査性質に変換することができる。
また、検査用モデルが満たすべき検査性質を満たしているか否かを検査することで、処理フローのふるまいが業務要件を満たしているか否かを検査することができる。
【０１４１】
なお、前記実施形態では、業務要件として、状態遷移整合性、事後条件、不変条件等を例示して説明したが、これら以外のものを業務要件として定義して用いてもよいし、或いは、状態遷移整合性、事後条件、不変条件のうちの少なくとも１つを適用する構成としてもよいし、業務要件の適用は適宜選択できる。
【符号の説明】
【０１４２】
１００  設計支援装置
１０１  検査用モデル生成部
１０２  モデル検査部
１０４  処理フロー状態生成部(処理フロー状態抽出部)
１０５  業務要件記述支援部(変換部)
１０６  検査性質生成部
１１１  処理フロー
１１２  リソース構造モデル(リソース構造情報)
１１３  リソース状態遷移モデル(リソース状態遷移情報)
１１４  ジョブ作用情報
１２０  検査用モデル
１２１  モデル関連情報
１２５  検査性質(検査性質情報)
１２３  処理フロー状態
３９０１  業務要件入力画面(入力部)
４４０１  業務要件入力画面(入力部)
４９００  設計支援装置
４９０１  検査用モデル生成部
４９０２  モデル検査部
４９０２Ａ  モデル検査エンジンＡ(モデル検査エンジン)
４９０２Ｂ  モデル検査エンジンＢ(モデル検査エンジン)
４９０４  処理フロー状態生成部(処理フロー状態抽出部)
４９０６  検査性質生成部
４９０９  モデル検査エンジン依存情報(検査用モデル生成方法情報、検査性質生成方法情報、処理フロー状態抽出方法情報)
４９２０  検査用モデル
４９２３  処理フロー状態
４９２５  検査性質
【図１】
2010198240.tif 000003
【図２】
2010198240.tif 000004
【図３】
2010198240.tif 000005
【図４】
2010198240.tif 000006
【図５】
2010198240.tif 000007
【図６】
2010198240.tif 000008
【図７】
2010198240.tif 000009
【図８】
2010198240.tif 000010
【図９】
2010198240.tif 000011
【図１０】
2010198240.tif 000012
【図１１】
2010198240.tif 000013
【図１２】
2010198240.tif 000014
【図１３】
2010198240.tif 000015
【図１４】
2010198240.tif 000016
【図１５】
2010198240.tif 000017
【図１６】
2010198240.tif 000018
【図１７】
2010198240.tif 000019
【図１８】
2010198240.tif 000020
【図１９】
2010198240.tif 000021
【図２０】
2010198240.tif 000022
【図２１】
2010198240.tif 000023
【図２２】
2010198240.tif 000024
【図２３】
2010198240.tif 000025
【図２４】
2010198240.tif 000026
【図２５】
2010198240.tif 000027
【図２６】
2010198240.tif 000028
【図２７】
2010198240.tif 000029
【図２８】
2010198240.tif 000030
【図２９】
2010198240.tif 000031
【図３０】
2010198240.tif 000032
【図３１】
2010198240.tif 000033
【図３２】
2010198240.tif 000034
【図３３】
2010198240.tif 000035
【図３４】
2010198240.tif 000036
【図３５】
2010198240.tif 000037
【図３６】
2010198240.tif 000038
【図３７】
2010198240.tif 000039
【図３８】
2010198240.tif 000040
【図３９】
2010198240.tif 000041
【図４０】
2010198240.tif 000042
【図４１】
2010198240.tif 000043
【図４２】
2010198240.tif 000044
【図４３】
2010198240.tif 000045
【図４４】
2010198240.tif 000046
【図４５】
2010198240.tif 000047
【図４６】
2010198240.tif 000048
【図４７】
2010198240.tif 000049
【図４８】
2010198240.tif 000050
【図４９】
2010198240.tif 000051