(57)【要約】【課題】効率の良い仕様変更時の再検証を支援することができるようにする。【解決手段】ソフトウェアの仕様を検証する仕様検証支援装置であって、仕様を表す設計情報を記憶する設計情報格納部と、仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、検証コードにおいて用いられる設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、コード生成設定情報に基づいて特定される検証対象設計情報を設計情報から抽出し、抽出した検証対象設計情報を検証ベースコードに適用して検証コードを生成する検証コード生成処理部と、検証コードを実行した検証結果、検証対象設計情報を特定するための参照情報、及び検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成する検証エビデンス生成処理部と、を備える。【選択図】  図１
2014164677.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアの仕様を検証する仕様検証支援装置であって、
前記仕様を表す設計情報を記憶する設計情報格納部と、
前記仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、
前記検証コードにおいて用いられる前記設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、
前記コード生成設定情報に基づいて特定される前記検証対象設計情報を前記設計情報から抽出し、抽出した前記検証対象設計情報を前記検証ベースコードに適用して前記検証コードを生成する検証コード生成処理部と、
前記検証コードを実行した検証結果、前記検証対象設計情報を特定するための参照情報、及び前記検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成する検証エビデンス生成処理部と、
を備えることを特徴とする仕様検証支援装置。
【請求項２】
請求項１に記載の仕様検証支援装置であって、
前記検証エビデンスに含まれる前記参照情報により特定される前記検証対象設計情報を前記設計情報から抽出し、前記抽出した検証対象設計情報の内容と、前記検証エビデンスに含まれている前記内容情報が表す内容とを比較して検証の要否を判定する検証結果確認処理部をさらに備えること、
を特徴とする仕様検証支援装置。
【請求項３】
請求項２に記載の仕様検証支援装置であって、
前記検証確認結果処理部は、前記検証エビデンスに含まれる前記検証結果に応じて検証の要否を判定し、検証不要と判定した場合にのみ、前記抽出した検証対象設計情報の内容と前記検証エビデンスに含まれている前記内容情報が表す内容とを比較してさらに検証の要否を判定すること、
を特徴とする仕様検証支援装置。
【請求項４】
請求項１乃至３のいずれか１項に記載の仕様検証支援装置であって、
前記検証エビデンス生成処理部は、前記検証対象設計情報を所定のハッシュ関数に与えて前記内容情報を算出すること、
を特徴とする仕様検証支援装置。
【請求項５】
請求項１乃至４のいずれか１項に記載の仕様検証支援装置であって、
前記検証ベースコードに追加する処理を所定方式で記述したコードである検証部品コードを生成するためのひな形である検証部品コード生成情報を記憶する検証部品コード生成情報格納部をさらに備え、
前記検証コード生成処理部は、前記検証対象設計情報を前記所定方式で記述した検証データコードを生成し、前記検証部品コード生成情報及び前記検証対象設計情報に基づいて前記検証部品コードを生成し、前記検証データコード及び前記検証部品コードを前記検証ベースコードに適用して前記検証コードを生成すること、
を特徴とする仕様検証支援装置。
【請求項６】
ソフトウェアの仕様を検証する方法であって、
前記仕様を表す設計情報を記憶する設計情報格納部と、
前記仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、
前記検証コードにおいて用いられる前記設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、
を備えるコンピュータが、
前記コード生成設定情報に基づいて特定される前記検証対象設計情報を前記設計情報から抽出し、抽出した前記検証対象設計情報を前記検証ベースコードに適用して前記検証コードを生成するステップと、
前記検証コードを実行した検証結果、前記検証対象設計情報を特定するための参照情報、及び前記検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成するステップと、
を実行することを特徴とする仕様検証支援方法。
【請求項７】
ソフトウェアの仕様を検証するためのプログラムであって、
前記仕様を表す設計情報を記憶する設計情報格納部と、
前記仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、
前記検証コードにおいて用いられる前記設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、
を備えるコンピュータに、
前記コード生成設定情報に基づいて特定される前記検証対象設計情報を前記設計情報から抽出し、抽出した前記検証対象設計情報を前記検証ベースコードに適用して前記検証コードを生成するステップと、
前記検証コードを実行した検証結果、前記検証対象設計情報を特定するための参照情報、及び前記検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成するステップと、
を実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェア開発を支援する技術に関し、特に、ソフトウェア仕様を検証する技術に関する。
【背景技術】
【０００２】
ソフトウェア開発では、顧客からの要望等に基づき、開発したソフトウェアが意図した通りの動作するよう、設計・実装することが求められる。そのため、設計段階での仕様の検証、或いは、実装したソフトウェア上での動作確認（テスト）によって、期待通りに動作するか、を確認することが重要となる。
【０００３】
設計段階での検証には、例えば、ソフトウェアの振る舞いを特殊な仕様記述言語によって記述することで、ソフトウェアが意図しない動作をしないことを、検証するためのモデル検証技術が知られている。例えば、「Ｐｒｏｍｅｌａ」はモデル検査技術のための記述言語のひとつであり、Ｐｒｏｍｅｌａ言語で書かれたモデルを検査するツールとして「ＳＰＩＮ」が知られている（非特許文献１）。また、ソフトウェアの設計情報から、仕様検証のための仕様記述言語に自動変換することで、設計情報の仕様検証を容易にする方法が知られている（特許文献１）。
【０００４】
検証を行った後、例えばソフトウェアに不具合が見つかった場合や顧客要求が変更になった場合には、仕様が修正されることになり、その修正後の仕様についての再検証が必要となる。しかしながら、仕様修正のたびに、すべての項目に対して再検証を行うと、仕様修正に関わる再検証のコストが大きくなってしまう。この問題に対し、特許文献２では、修正後の仕様と修正前の仕様とを比較し、変更された仕様項目から遷移グラフを辿って状態探索を行い、修正後の仕様に関するテストケースを生成することで、仕様修正時のソフトウェアの検証を効率化する方法が提案されている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２０１１−１８０６３２号公報
【特許文献２】特開２００９−２５２１６９号公報
【非特許文献】
【０００６】
【非特許文献１】Gerard Holzmann、“The SPIN Model Checker: Primer and Reference Manual”、Addison-Wesley, 2004.
【発明の概要】
【発明が解決しようとする課題】
【０００７】
検証しようとするシステムの振る舞いに対しての要件によっては、システムの機能やシナリオに変更があったとしても再検証を行う必要のない場合がある。例えば、鉄道の運行を管理するシステムにおいて、Ａ駅に設計変更があったとしても、Ｂ駅に対し、列車が駅外に進出することの検証を行う必要の無い場合がある。  
しかしながら、特許文献２に記載の方法では、仕様の変更箇所に関するテストケースが必ず作成されることになるため、本来不要な検証についても再検証されてしまうことがある。
【０００８】
本発明は、このような背景を鑑みてなされたものであり、効率の良い仕様変更時の再検証を支援することのできる、仕様検証支援装置、仕様検証支援方法及びプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００９】
上記課題を解決するための本発明のうち主たる発明は、ソフトウェアの仕様を検証する仕様検証支援装置であって、前記仕様を表す設計情報を記憶する設計情報格納部と、前記仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、前記検証コードにおいて用いられる前記設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、前記コード生成設定情報に基づいて特定される前記検証対象設計情報を前記設計情報から抽出し、抽出した前記検証対象設計情報を前記検証ベースコードに適用して前記検証コードを生成する検証コード生成処理部と、前記検証コードを実行した検証結果、前記検証対象設計情報を特定するための参照情報、及び前記検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成する検証エビデンス生成処理部と、を備えることとする。
【００１０】
また、本発明の他の態様は、ソフトウェアの仕様を検証する方法であって、前記仕様を表す設計情報を記憶する設計情報格納部と、前記仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、前記検証コードにおいて用いられる前記設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、を備えるコンピュータが、前記コード生成設定情報に基づいて特定される前記検証対象設計情報を前記設計情報から抽出し、抽出した前記検証対象設計情報を前記検証ベースコードに適用して前記検証コードを生成するステップと、前記検証コードを実行した検証結果、前記検証対象設計情報を特定するための参照情報、及び前記検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成するステップと、を実行することとする。
【００１１】
また、本発明の他の態様は、ソフトウェアの仕様を検証するためのプログラムであって、前記仕様を表す設計情報を記憶する設計情報格納部と、前記仕様の検証を行うプログラムである検証コードを生成するためのひな形である検証ベースコードを記憶する検証ベースコード格納部と、前記検証コードにおいて用いられる前記設計情報である検証対象設計情報を特定するためのコード生成設定情報を記憶するコード生成設定情報格納部と、を備えるコンピュータに、前記コード生成設定情報に基づいて特定される前記検証対象設計情報を前記設計情報から抽出し、抽出した前記検証対象設計情報を前記検証ベースコードに適用して前記検証コードを生成するステップと、前記検証コードを実行した検証結果、前記検証対象設計情報を特定するための参照情報、及び前記検証対象設計情報の内容を表す内容情報を含む検証エビデンスを生成するステップと、を実行させることとする。
【００１２】
その他本願が開示する課題やその解決方法については、発明の実施形態の欄及び図面により明らかにされる。
【発明の効果】
【００１３】
本発明によれば、効率の良い仕様変更時の再検証を支援することが可能となる。
【図面の簡単な説明】
【００１４】
【図１】本実施形態に係る検証支援装置の構成を示すブロック図である。
【図２】本実施形態に係る検証支援装置のハードウェア構成の一例を示す図である。
【図３】本実施例における設計情報の一例を示す図である。
【図４】本実施例におけるコード生成設定情報の一例を示す図である。
【図５】本実施例における検証処理の処理フローを示す図である。
【図６】本実施例における検証コード生成処理の概要を示す図である。
【図７】本実施例における検証ベースコードの一例を示す図である。
【図８】本実施例における検証部品コード生成情報の一例を示す図である。
【図９】本実施例における検証コードの一例を示す図である。
【図１０】本実施例における検証エビデンス生成処理の処理フローを示す図である。
【図１１】本実施例における検証エビデンスの一例を示す図である。
【図１２】本実施例における検証結果確認処理の処理フローを示す図である。
【図１３】本実施例における検証支援装置の画面イメージの一例を示す図である。
【発明を実施するための形態】
【００１５】
図１は、本実施形態の検証支援装置１００の構成図である。図１に示した通り、検証支援装置１００は、入力部１０１、入出力制御部１０２、表示部１０３、検証結果確認処理部１０４、検証エビデンス生成処理部１０５、検証結果分析処理部１０６、検証コード生成処理部１０７、検証支援処理部１０８、及び検証処理部１０９の各処理部を備える。
【００１６】
また、検証支援装置１００は、検証エビデンス格納部１１０、検証結果格納部１１１、検証コード格納部１１２、設計情報格納部１１７、コード生成設定情報格納部１１６、検証部品コード生成情報格納部１１５、検証ベースコード格納部１１４、及び検証用設定情報格納部１１３から構成される。
【００１７】
ここで、入力部１０１は、キーボードやマウスなどの入力装置２０４を介して、ユーザから情報の入力を受け付けるための処理部であり、表示部１０３はディスプレイ等の表示装置２０３を介して、ユーザに画面を提供するための処理部である。
【００１８】
入出力制御部１０２は、入力部１０１が受け付けた情報を受け取り、検証支援部１０８への入力結果を通知し、検証支援装処理部１０８によって生成される画面イメージを表示部１０３に出力するための処理を行う。
【００１９】
検証支援部１０３は、仕様検証、或いは、検証結果を表示するためのＧＵＩ（Ｇｒａｐｈｉｃａｌ  Ｕｓｅｒ  Ｉｎｔｅｒｆａｃｅ）を提供し、入力部１０１が受け付けたユーザ入力に従い、検証コード生成処理部１０７、検証処理部１０９、検証結果分析処理部１０６、検証エビデンス生成処理部１０５の各処理部を制御する。
【００２０】
検証コード処理部１０７は、仕様検証を行うプログラムである検証コード６０５を生成する。本実施形態では一例として、検証コード６０５は、モデル検査用仕様記述言語Ｐｒｏｍｅｌａにより記述されることを想定するが、Ｐｒｏｍｅｌａに限らず任意の仕様記述言語により記述することができる。検証コード生成処理部１０７による検証コード６０５の生成処理については後述する。
【００２１】
検証処理部１０９は、検証コード６０５を用いた検証を行い、その検証結果を生成する。本実施形態では一例として、検証処理部１０９には、Ｐｒｏｍｅｌａの検証ツールとしてＳＰＩＮを用いることを想定する。なお、ＳＰＩＮ以外の検証ツールを使うようにしてもよい。
【００２２】
検証結果分析処理部１０６は、検証処理部１０９が生成した検証結果を分析することで検証の成功、失敗又は未了の判定を行う。なお、検証結果分析処理部１０６は、例えば、ＳＰＩＮによる検証結果に含まれる終了ステータスを参照することにより検証処理が成功若しくは失敗したこと、又は途中で終了したことを判定することができる。
【００２３】
検証エビデンス生成処理部１０５は、当該検証の概要を表す検証エビデンスを生成する。検証エビデンスには、検証処理部１０９が生成した検証結果と、検証コード６０５の実行時に用いられる設計情報（以下、検証対象設計情報と呼ぶ。）の内容と、検証対象設計情報を特定するための情報（以下、検証対象設計情報参照情報という。）とが含まれる。本実施形態では、検証エビデンスに含める検証対象設計情報の内容として、所定のハッシュ関数に検証対象設計情報を与えたハッシュ値を用いるものとする。
【００２４】
検証結果確認処理部１０４は、検証エビデンスを用いて、さらなる検証の要否の確認処理を行う。検証結果確認処理部１０４による検証要否の確認処理については後述する。
【００２５】
次に各格納部に格納される情報について説明する。  
設計情報格納部１１７には、ソフトウェア開発のための設計情報６００が格納される。設計情報６００の例は後述するが、任意のデータ形式とすることができる。
【００２６】
検証ベースコード格納部１１４には、検証コード６０５のひな形である検証ベースコード６０３が格納（記憶）される。検証コード６０５は、検証しようとするシステムの振る舞いに対しての要件（例えば、列車が必ず駅外に進出することを検証する輸送性の要件や、支障のある軌道回路に列車が進入しないことを検証する安全性の要件などがある。以下、検証要件という。）ごとに、検証ベースコード６０３が格納される。
【００２７】
検証部品コード生成情報格納部１１５には、検証コード６０５に埋め込む処理を所定の言語（本実施形態ではＰｒｏｍｅｌａを想定する。）で記述したコード（以下、検証部品コードという。）を生成するための検証部品コード生成情報６０１が格納（記憶）される。
【００２８】
コード生成設定情報格納部１１６には、設計情報６００内の検証対象設計情報を特定するための情報であるコード生成設定情報４００が格納（記憶）される。コード生成設定情報格納部１１６は、検証の要件ごとに、１つまたは複数のコード生成設定情報４００を格納する。
【００２９】
検証用設定情報格納部１１３には、検証処理部１０９を実行する際に必要となる設定情報が格納（記憶）される。例えば、検証コード６０５にモデル検査用仕様記述言語Ｐｒｏｍｅｌａを用い、検証処理にＰｒｏｍｅｌａの検証ツールであるＳＰＩＮを用いる場合には、ＳＰＩＮを実行するための実行手順（スクリプト）や実行時のオプション情報などが格納される。
【００３０】
検証コード格納部１１２には、検証コード生成処理部１０７から出力される検証コード６０５が格納（記憶）される。検証処理部１０９は、上記検証用設定情報格納部１１３に格納されたスクリプト及びオプション情報などに基づいて、検証コード格納部１１２に格納された検証コード６０５実行することにより、検証要件に応じた設計情報６００の検証を行うことになる。
【００３１】
検証結果格納部１１１には、検証処理部１０９から出力される検証結果が格納（記憶）される。
【００３２】
検証エビデンス格納部１１０には、検証エビデンス生成処理部１０５から出力される検証エビデンスが格納（記憶）される。
【００３３】
図２は、図１に示した検証支援装置１００を実現するハードウェア構成の一例を示している。  
図２の構成例では、検証支援装置１００は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｏｒ  Ｕｎｉｔ）２０１、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）２０２、入力装置２０４、表示装置２０３、及び外部記憶装置２１０がインターフェイス２０５を介して接続された、一般的な構成を有するコンピュータ（電子計算機）である。
【００３４】
入力装置２０４は、例えば、キーボードやマウスなどであり、表示装置２０３は、表示用ディスプレイ、外部記憶装置２１０は、ＨＤＤ（Ｈａｒｄ  Ｄｉｓｋ  Ｄｒｉｖｅ）などである。
【００３５】
ＣＰＵ２０１は、ＲＡＭ２０２上にロードしたプログラムを実行することで、図１に示す入出力制御部１０２、検証支援処理部１０８、検証結果確認処理部１０４、検証エビデンス生成処理部１０５、検証結果分析処理部１０６、検証コード生成処理部１０７、及び検証処理部１０９の各処理部をプロセスとして具現化する。
【００３６】
外部記憶装置２１０は、検証結果確認処理部１０４、検証エビデンス生成処理部１０５、検証結果分析処理部１０６、検証コード生成処理部１０７、及び検証処理部１０９の実行プログラムを格納するための記憶領域であり、検証エビデンス格納部１１０、検証結果格納部１１１、検証コード格納部１１２、設計情報格納部１１７、コード生成情報格納部１１６、検証部品コード生成情報格納部１１５、検証ベースコード格納部１１４、及び検証用設定情報格納部１１３の各格納部に相当する。
【００３７】
インターフェイス２０５は、装置内の上記各構成要素間でデータを送受信する内部パスである。
【００３８】
以下、本実施形態に係る実施例について、図３に示す設計情報を用いて説明する。  
図３は、鉄道運行管理システムを開発するための設計情報６００の一例を説明するための図である。鉄道運行管理システムのための設計情報６００において、「閉そく」とは信号機の防護区間であり、信号機の内方区間に設置された第一内方軌道回路から最終内方軌道回路までの線路領域である。二つの閉そく間の関係を「幾何」という。鉄道運行管理システムは、列車の在線位置や設備の状態、運行計画を表すダイヤなどを入力として受け取り、列車が次に進行する線路領域（閉そく）を決定し、信号機への制御要求を出力する。これによって、鉄道運行管理システムは、列車の進路制御を行うことになる。
【００３９】
図３に示す設計情報６００は、線路の形状を表す線路形状３００、線路形状３００に含まれる閉そくを管理する閉そくテーブル３２０、及び幾何を管理する幾何テーブル３２１を含む。なお、図３では、線路の形状が視覚的に図示されているが、線路形状３００は線路の配置及び分岐、線路の属するエリア（駅、区間など）、信号機の設置箇所などを管理する情報であればよく、線路形状３００に基づいて図３の形状が表示可能であるものとする。
【００４０】
閉そくテーブル３２０には、各閉そくの識別子である閉そくＩＤ３０４、閉そくが所属するエリアを表す所属３０５、閉そくを定義する関連設備３０５、各閉そくに関わる信号機を制御する際に必要となるロジック３０７、及び、ロジック３０７を実行する場合に参照する条件値３０８（ロジック３０７に与えるパラメータ）から構成される。信号機と第一内方軌道回路から最終内方軌道回路までの軌道回路とにより閉そくが定義される、本実施例では、関連設備３０５には、１つの信号機と、１つまたは複数の軌道回路とが含まれるものとする。図３の例では、閉そくと線路形状との対応を図式化している。
【００４１】
幾何テーブル３２１には、幾何の識別子である幾何ＩＤ３０９、二つの閉そく間の関係の種類（例えば、閉そくが平行している関係や、閉そくが向かい合っている関係などを示す。）を表す種別３１０、当該二つの閉そくの一方を示す閉そくＩＤ１（３１２）、当該二つの閉そくの他方を示す閉そくＩＤ２（３１３）、幾何に対して割り付けられたロジック３１３、及びロジック３１３を実行する場合に参照する条件値３１４（ロジック３１３に与えるパラメータ）が含まれる。
【００４２】
閉そくテーブル３２０に割り付けられたロジック３０７、及び幾何テーブル３２１に割り付けられたロジック３１３は、例えば、閉そくに進入する列車に対し、当該閉そくに進入してもよいかどうかを判断するための制御ロジックである。一つの幾何、または、閉そくに対し、制御ロジックは複数設定することができる。
【００４３】
運行管理システムは、列車の在線列車、運行計画を表すダイヤ情報、閉そくテーブル３２０に管理されている閉そくの関連設備などに基づいて、列車が進入する閉そくを決定し、決定した閉そくに割り当てられたロジック３０７、及び当該閉そくと関連する幾何に割り当てられたロジック３１３を実行して、当該閉そくに進入してよいかどうかを判断し、その結果を基に信号機への制御要求を決定する。
【００４４】
そのため、設計情報６００に含まれる、閉そくや幾何のデータ設計、各閉そくに割り当てられるロジック３０７及び条件値３０８、並びに、各幾何に割り当てられる３１３及び条件値３１４は、列車を計画通り運行させるための要素である。これら設計情報６００の不備や、割り当てられたロジック３０７及び３１３に誤りがある場合には、例えば在線列車が駅外に進出できなくなったり、競合する信号機に対して誤った制御要求を出力したりする等、意図した進路制御ができなくなる可能性があることを意味する。そこで、設計情報６００の検証が必要となる。
【００４５】
なお、本実施例では、図３に示す設計情報６００を用いて説明を行うが、設計情報６００の内容及び形式は図３に示すもの限定されるものではない。設計情報６００には、図３に示すもの以外の情報を含んでもよい。例えば、信号機や軌道回路を、設備一覧として別のテーブルに管理してもよい。また、例えば、割当てられたロジック３０７内の各ロジックの設計情報をフローチャート等として記述し、検証部品コード生成処理部６１１において、検証部品コードを設計情報６００から生成できるようにしてもよい。
【００４６】
図４は、本実施例におけるコード生成設定情報４００の一例を表す図である。  
コード生成設計情報４００は、検証要件の識別子である要件ＩＤ、検証要件の名称を表す要件４０２、検証の概要を表す備考４０３、検証対象となるロジック４０４及びデータ４０５、並びに、検証対象設計情報の検証範囲を特定する単位となる単位４０６から構成される。ユーザから指定された検証要件及び検証範囲に対応するコード生成設計情報４００に基づいて、設計情報６００から検証対象となる検証対象設計情報が抽出され、またコード生成設計情報４００に含まれるデータ４０５から、検証コード６０５で用いられるデータが特定されて検証ベースコード６０３に組み入れられ、これにより検証コード６０５が生成される。
【００４７】
図５は、本実施例における検証処理の処理フローを示す図である。  
検証処理が開始すると（ステップ５００）、ユーザから検証要件の選択を入力部１０１から受け付け、選択された検証要件のそれぞれに対し、ステップ５０２〜ステップ５０９を繰り返す（ステップ５０１）。また、ユーザから検証範囲の選択を入力部１０１から受け付け、選択された検証範囲のそれぞれに対し、ステップ５０３〜ステップ５０８を繰り返す（ステップ５０２）。
【００４８】
検証結果確認処理部１０４は、検証要件及び検証範囲に対応する検証エビデンスを検証エビデンス格納部１１０から読み出し、読み出した検証エビデンスを用いて、さらなる検証が必要かどうかを確認する、検証結果の確認処理（図１２）を行う（ステップ５０３）。
【００４９】
ステップ５０３の検証結果確認処理の結果が「検証未済」であれば、ステップ５０５に進む。それ以外の場合にはステップ５０９に進む。
【００５０】
検証コード生成処理部１０７は、検証コード６０５の生成処理（図６）を行い、生成した検証コード６０５を検証コード格納部１１２に格納する（ステップ５０５）。検証処理部１０９は、ステップ５０５で生成された検証コード６０５を用いて検証処理を行い、検証結果を検証結果格納部１１１に格納する（ステップ５０６）。検証結果分析処理部１０６は、ステップ５０６で生成された検証結果を分析し、検証の成功、失敗、未了の判定を行う（ステップ５０７）。なお、検証結果分析処理部１０６は、一般的な手法を用いて検証結果を分析することができる。
【００５１】
検証エビデンス生成処理部１０５は、ステップ５０７による分析結果を用いて、検証エビデンスの生成処理（図１０）を行い、生成した検証エビデンスを検証エビデンス格納部１１０に格納する（ステップ５０８）。
【００５２】
ユーザに選択された検証範囲がまだあればステップ５０２に戻る（ステップ５０９）。そうでなければ、ステップ５０８に進む。また、ユーザに選択された検証要件がまだあればステップ５０１に戻る（ステップ５１０）。そうでなければステップ５１１に進み、処理を終了する。
【００５３】
図５に示したように、検証対象設計情報の検証にあたっては、検証コード生成処理（ステップ５０５）の前に検証エビデンスを用いた検証結果の確認処理（ステップ５０３）が行われるので、選択された検証要件及び検証範囲については既に検証済みと判定された場合、すなわち、検証が不要な場合には、ステップ５０５からステップ５０８の検証処理を行う必要がなくなる。これにより、不要な検証処理を省略することが可能となる。したがって、膨大な設計情報６００を検証する場合にも、効率的に検証処理を行うことができる。
【００５４】
次に、ステップ５０５の検証コード生成処理の概要について説明する。  
図６は、ステップ５０５の検証コード生成処理の概要を表す図である。なお、設計情報６００は、図３の線路形状３００、閉そくテーブル３２０及び幾何テーブル３２１を表すデータであるものとし、検証コード６０５には、モデル検査用仕様記述言語Ｐｒｏｍｅｌａを用いるものとする。検証コード生成処理部１０７は、検証データコード生成処理部６１０、検証部品コード生成処理部６１１、及び検証コード構成処理部６１２を含む。
【００５５】
検証データコード生成処理部６１０は、ユーザから選択された検証要件及び検証範囲に対応するコード生成設定情報４００をコード生成設定情報格納部１１６から読み出し、読み出したコード生成設定情報４００に含まれるデータ４０５に指定されているデータを、検証対象設計情報として設計情報６００から抽出する。そして、検証データコード生成処理部６１０は、抽出した検証対象設計情報をＰｒｏｍｅｌａ言語で記述したコード（以下、検証データコードという。）を生成する。
【００５６】
検証対象設計情報の抽出は下記の手順によって行えばよい。まず、コード生成設計情報４００から、選択された検証要件を示す要件ＩＤに対応する、ロジック４０４及びデータ４０５を特定する。例えば、要件ＩＤが「１」である「輸送性」の要件が選択された場合には、ロジック４０４から進路選択が抽出されるとともに、データ４０５から閉そく（関連設備）及び幾何（種別、閉そくＩＤ１、閉そくＩＤ２）が抽出される。
【００５７】
次に、選択された検証範囲に対応する設計情報６００の内、前記抽出したロジック及びデータに該当するものを抽出する。なお、ここで入力される検証範囲は、コード生成設定情報４００の単位４０６である。
【００５８】
要件ＩＤが「１」である「輸送性」の単位４０６は「駅」であるため、検証範囲は駅単位となる。ここで、検証範囲として「駅Ａ」が与えられた場合には、閉そくテーブル３２０から、「駅Ａ」に属する閉そくを抽出し、幾何テーブル３２１から、前記抽出した閉そくを閉そくＩＤ１（３１１）または閉そくＩＤ２（３１２）が示しているもの含む幾何を抽出する。例えば、「輸送性」及び「駅Ａ」に対応する検証対象設計情報として、図３の設計情報６００の例では、閉そくＩＤが「Ｂ１」「Ｂ２」及び「Ｂ３」の閉そくが抽出される。さらにロジック（進路選択）、データ（閉そく（関連設備）、幾何（種別、閉そくＩＤ１、閉そくＩＤ２））から、閉そくＩＤが「Ｂ１」「Ｂ２」及び「Ｂ３」の閉そく内の関連設備（信号機、起動回路）、ロジック３０７、条件３０８、及び幾何が抽出される。
【００５９】
なお、上記では単位４０６が「駅」の場合に、特定の駅から検証対象設計情報を特定する方法を示したが、単位４０６は駅に限らなくてもよい。例えば、単位４０６として、「駅１から駅２内に含まれる全駅」、或いは、「二つの閉そくをつなぐ全閉そく」等を単位４０６に指定してもよい。この場合、単位４０６を条件として、条件を満たす設備情報６００を検索するようにすればよい。例えば、「駅１から駅２内に含まれる全駅」であれば、ユーザから二つの駅（例えば、駅Ａ、駅Ｃ）を入力とし受け取り、その二つの駅の間に存在する全駅を探索することができる。そして、得られた駅に含まれる設計情報６００の中から、ロジック４０４、データ４０５に該当する設計情報を特定し、検証対象設計情報とすればよい。
【００６０】
以上により抽出した検証対象設計情報が検証データコード６０２として記述される。例えば、図６に示す検証データコード６０２では、図３の閉そくテーブル３２０に含まれる閉そくＩＤが「Ｂ２」である閉そく（Ｂｌｏｃｋ）を「０」で表し、信号機（ｓｉｇｎａｌ）Ａを「０」で表し、信号機Ａと２つの軌道回路とが関連しているものとして、「Ｂｌｏｃｋ［０］．ｓｉｇｎａｌ＝０；Ｂｌｏｃｋ［０］．ｌｅｎｇｔｈ＝２；」というように記述されている。
【００６１】
また、検証部品コード生成処理部６１１は、検証部品コード生成情報６０１、コード生成設定情報４００、及び検証対象設計情報に基づいて検証部品コード６０４を生成する。検証部品コード生成情報６０１には、進路選択や競合判断、設備状態チェック等、予め検証コード６０４に埋め込むための判断ロジックのコードを格納しておき、コード生成設定情報４００から抽出した検証要件に対応するロジック４０４を検証部品コード生成情報６０１の判断ロジックから抽出して検証部品コード６０４を生成することができる。例えば、要件ＩＤが「１」である「輸送性」の要件が選択された場合には、検証部品コード生成情報６０１内に記述された判断ロジックから、「進路選択」に該当するコードを抽出して検証部品コード６０４を生成する。また、例えば、各ロジックの設計情報がフローチャート等で記述されている場合には、検証部品コード生成処理部６１１において、検証部品コードを設計情報６００から生成できるようにしてもよい。
【００６２】
検証コード構成処理６１２は、検証部品コード６０４および検証用データコード６０２を検証ベースコード６０３に組み込んで検証コード６０５を生成する。
【００６３】
図７、図８、図９に、検証ベースコード６０３、検証部品コード生成６０４、及び生成される検証コード６０５の一例を示す。
【００６４】
図７は、検証ベースコード６０３の一例である。前述のとおり検証ベースコード６０３は検証コード６０５のひな形となるコードであり、検証データコード６０２を埋め込むための標識である検証用データコード埋め込み部（図７では、２つの検証用データコード埋め込み部７０１及び７０２が示されている。）と、検証部品コード６０４を埋め込むための標識である検証部品コード埋め込み部（図７では、３つの検証部品コード埋め込み部７０５、７０６及び７０６が示されている。）を含む。
【００６５】
検証ベースコード６０３の検証データコード埋め込み部は、「＠ｄａｔａ」から始まるステートメントで記述され、検証要件を表すＲｅｑＩＤ、及び検証データコード６０２を埋め込む場所を識別するＰｉｅｃｅＩｄの各属性を有する。検証コード構成処理部６１２は、検証ベースコード６０３内の「＠ｄａｔａ」ステートメントを探索し、ＲｅｑＩＤが検証要件に一致する場合、ＰｉｅｃｅＩｄに対応する検証データコードで当該ステートメントを置換することにより、検証データコード６０を検証ベースコード６０３に埋め込む。
【００６６】
なお、図６−９の例では、検証データコード生成処理部６１０は、検証対象設計情報に含まれる信号機に係るデータの個数をカウントして「＃ｄｅｆｉｎｅ  Ｎ＿ＳＩＧＮＡＬ  個数」という検証データコード６０２を作成し、これをＰｉｅｃｅＩｄが「１」の「＠ｄａｔａ」ステートメントと置換し、上述のように閉そくについて生成した「Ｂｌｏｃｋ［０］．ｓｉｇｎａｌ＝０・・・」で表される検証データコード６０２を、ＰｉｅｃｅＩｄが「２」の「＠ｄａｔａ」ステートメントと置換しているが、どのＰｉｅｃｅＩｄの「＠ｄａｔａ」ステートメントについてどの検証データコード６０２を置換するかは予め設定されているものとする。
【００６７】
同様に、検証部品コード埋め込み部は、「＠ｃｏｄｅ」から始まるステートメントで記述されており、検証要件を表すＲｅｑＩｄ、及び検証部品コード６０４を埋め込む場所を識別するＰｉｅｃｅＩｄの各属性を有する。検証部品コード生成情報６０１にはＰｉｅｃｅＩｄが指定されており、検証部品コード６０４は検証要件及びＰｉｅｃｅＩｄごとに生成されることになる。検証コード構成処理６１２は、検証ベースコード６０３内の「＠ｃｏｄｅ」ステートメントを探索し、ＲｅｑＩｄが検証要件に一致する場合、ＰｉｅｃｅＩｄに対応する検証部品コード６０４で当該ステートメントを置換することにより、検証部品コード６０４を検証ベースコード６０３に埋めこむ。
【００６８】
図８は、検証部品コード生成情報６０１の構成を、ＸＭＬ（ｅＸｔｅｎｓｉｂｌｅ  Ｍａｒｃｋｕｐ  Ｌａｎｇｕａｇｅ）を用いて記述した一例を示す図である。
【００６９】
検証部品コード生成情報６０１は、全体を管理するためのＣｏｄｅＰｉｅｃｅＧｅｎｅｒａｔｅＩｎｆｏ要素８００から構成され、ＣｏｄｅＰｉｅｃｅＧｅｎｅｒａｔｅＩｎｆｏ要素８００には、検証要件ごとの検証部品コード生成情報を管理するためのＣｈｅｃｋＲｕｌｅ要素８０１が含まれる。
【００７０】
ＣｈｅｃｋＲｕｌｅ要素８０１は、対応する検証要件を示す要件ＩＤを格納するためのＩｄ属性を有する。また、ＣｈｅｃｋＲｕｌｅ要素８０１は、その子要素として、検証ベースコード６０３内の検証部品コード埋め込み部を特定するためのＰｉｅｃｅ要素、埋め込む検証部品コードの概要を説明するためのＣｏｍｍｅｎｔ要素８０３、埋め込む検証部品コードを記述するためのＣｏｄｅ要素８０４を有する。
【００７１】
Ｃｏｄｅ要素８０４のＴｙｐｅ属性に「ｃｏｄｅ」が指定された場合には、Ｃｏｄｅ要素８０４の内容には、検証ベースコード６０３に埋め込むためのコードそのものが記述される。この場合、Ｃｏｄｅ要素８０４の内容がそのまま「＠ｃｏｄｅ」ステートメントと置換されることになる。
【００７２】
Ｃｏｄｅ要素８０４のＴｙｐｅ属性に「ｐｒｏｇｒａｍ」が指定された場合、設計情報６００から検証部品コード６０４を動的に生成するためのルーチンがＩｄ属性に指定される。この場合、検証部品コード生成処理部６１１は、Ｃｏｄｅ要素８０４のＩｄ属性に指定されたルーチンに検証対象設計情報を与えて実行し、その実行結果を「＠ｃｏｄｅ」ステートメントと置換する。
【００７３】
図９は、図７に示した検証ベースコード６０３より生成される検証コード６０５の一例である。
【００７４】
図９に示した検証ベース６０５は、図７の検証ベースコード内の検証データコード埋め込み部７０１、検証コード埋め込み部７０５、検証データコード埋め込み部７０２、及び検証コード埋め込み部７０６が、それぞれ、検証データコード埋め込み結果９０１、検証部品コード埋め込み結果９０５、検証データコード埋め込み結果９０２、検証部品コード埋め込み結果９０６に置換されたものである。
【００７５】
次に検証エビデンス生成処理（ステップ５０８）の処理について、図１０及び図１１を用いて説明する。
【００７６】
図１０は、検証エビデンス生成処理の処理フローを示す図である。  
検証エビデンス生成処理が開始すると（ステップ１０００）、検証エビデンス生成処理部１０５は、設計情報６００から検証対象設計情報を抽出する（ステップ１００１）。ここでの抽出処理は、上述した検証データコード生成処理部６１０、及び検証部品コード生成処理部６１１により行われる設計情報６００から検証対象設計情報を抽出する処理と同じ処理である。
【００７７】
検証エビデンス生成処理部１０５は、ステップ１００１において抽出した検証対象設計情報のハッシュ値を計算する（ステップ１００２）。検証エビデンス生成処理部１０５は、抽出した検証対象設計情報を示す検証対象設計情報参照情報、ステップ１００２で計算したハッシュ値及び検証結果を記述した検証エビデンスを生成し（ステップ１００３）、処理を終了する（ステップ１００４）。
【００７８】
図１１は、検証エビデンス生成処理によって生成される検証エビデンス６０５を格納する検証エビデンス格納情報１１００を、ＸＭＬを用いて記述した一例を示す図である。
【００７９】
図１１に示す通り、検証エビデンス格納情報１１００は、ＶｅｒｉｆｉｃａｔｉｏｎＥｖｉｄｅｎｃｅ要素１１０１から構成され、個々の検証エビデンスは、ＣｈｅｃｋＲｕｌｅ要素１１０３内に格納される。
【００８０】
ＣｈｅｃｋＲｕｌｅ要素１１０３は、検証エビデンスに対応する検証要素を示す要件ＩＤを格納するＩＤ属性を持ち、さらに検証対象設計情報ごとに検証エビデンスを管理するためのＴａｒｇｅｔＤａｔａ要素１１０３を含む。ＴａｒｇｅｔＤａｔａ要素１１０３は、検証対象設計情報を特定するための検証対象設計情報参照情報を格納するＲｅｆｅｒｅｎｃｅ要素１１０４と、検証結果及びハッシュ値を格納するためのＲｅｓｕｌｔ要素１１０５を含む。
【００８１】
図１１の例におけるＲｅｆｅｒｅｎｃｅ要素１１０４には、検証対象設計情報を特定するため、Ｓｔａｔｉｏｎ要素を記述し、ｓｔａｔｉｏｎＮａｍｅ属性内に検証対象設計情報に係る駅名称を指定している。
【００８２】
Ｒｅｓｕｌｔ要素１１０５内のｐａｓｓ属性には、ステップ５０７において検証結果分析処理部１０６が取得した、検証処理部１０９による検証コード６０５を用いた検証処理の検証結果を格納する。例えば、検証結果が成功の場合には、「成功」、失敗の場合には「失敗」を記載する。また、検証処理がメモリ不足や一定時間経過しても検証結果が得られなかった等、検証が途中終了していた場合には、「未了」を記述する。
【００８３】
Ｒｅｓｕｌｔ要素１１０５の子要素であるＴｉｍｅＳｔａｍｐ要素及びＨａｓｈＶａｌｕｅ要素には、それぞれ検証エビデンスを生成した日時及び検証対象設計情報のハッシュ値を格納する。
【００８４】
次に、上述した検証エビデンスを用いて、検証対象設計情報に対する検証結果を確認する処理について説明する（ステップ５０３）。
【００８５】
図１２は、検証エビデンス格納情報を元に検証結果を確認する処理の処理フローを表している。
【００８６】
検証結果の確認処理が開始すると（ステップ１２００）、検証結果確認処理部１０４は、検証エビデンス格納情報１１００から、選択された検証要件に対応する検証エビデンス１２０１を読み出す（ステップ１２０１）。検証結果確認処理部１０４は、図１１の検証エビデンス格納情報１１００内のＣｈｅｃｋＲｕｌｅ要素内のｉｄ属性が、選択された検証要件を示す要件ＩＤと一致するものがあるかを探索する。さらに検証結果確認処理部１０４は、ＴａｒｇｅｔＤａｔａ要素１１０４内のＲｅｆｅｒｅｎｃｅＤａｔａ要素が存在するかどうかを確認する。上記探索において、検証要件に対応する検証エビデンスが存在しない、又は検証対象設計情報参照情報が存在しない場合には（ステップ１２０２：Ｎｏ）、検証エビデンスが生成されていない（又は、検証対象設計情報が未検証）であるとして、検証未済を出力（ステップ１２１０）し、処理を終了する（ステップ１２１２）。
【００８７】
次に検証結果確認処理部１０４は、設計情報６００から検証対象設計情報を抽出する（ステップ１２０３）。ここでの抽出処理は、検証エビデンス生成処理における図１０のステップ１００１と同じ処理である。検証結果確認処理部１０４は、検証対象設計情報が存在しない場合は（ステップ１２０４：Ｙｅｓ）、検証対象なしを出力して（ステップ１２１１）、処理を終了する（１２１２）。そうでない場合は（ステップ１２０４：Ｎｏ）、検証結果確認処理部１０４は、検証対象設計情報を連結してハッシュ値の計算を行う（ステップ１２０５）。ここで、ハッシュ値の計算処理は、検証エビデンス生成処理における図１０のステップ１００２と同じ処理である。
【００８８】
検証結果確認処理部１０４は、計算したハッシュ値と検証エビデンス内のハッシュ値とを比較する（ステップ１２０６）。検証対象設計情報に変更がなければ、ステップ１２０５で計算されるハッシュ値と検証エビデンス内のハッシュ値（図１０のステップ１００２での計算結果）とは一致した値となる。したがって、この比較処理によって、検証要件に対応する検証対象設計情報に変更がないかどうかを確認することが可能となる。
【００８９】
計算したハッシュ値と検証エビデンス内のハッシュ値とが一致しなければ（ステップ１２０６：Ｎｏ）、ステップ１２１０に進み、検証未済を出力する。そうでなければ（ステップ１２０６：Ｙｅｓ）、検証結果確認処理部１０４は、検証エビデンス内の検証結果を確認にする（ステップ１２０７）。これは、検証対象設計情報に変更がなかった場合に、前回の検証結果が検証成功か否かを確認するための処理である。検証結果確認処理部１０４は、検証エビデンスに含まれる検証結果が「成功」であれば（ステップ１２０８：Ｙｅｓ）、検証済みを出力して（ステップ１２０９）、処理を終了する（ステップ１２１２）。検証結果が「成功」でない場合には（ステップ１２０８：Ｎｏ）、検証結果確認処理部１０４は、検証未済を出力して（ステップ１２１０）、処理を終了する（ステップ１２１２）。
【００９０】
このようにして、検証結果確認処理部１０４からの出力を参照することにより、検証コードの生成処理（ステップ５０５、図６の処理）、及び検証処理部１０９による検証処理（ステップ５０６）の実行の必要可否を判定することができる。したがって、不要な検証処理を回避することが可能となり、設計情報修正時の再検証コストを軽減することができる。
【００９１】
なお、ステップ１２０７及びステップ１２０８は、ステップ１２０５の前に実行し、検証成功の結果となっている検証エビデンスに対してのみ、ステップ１２０５、ステップ１２０６を実行するようにしてもよい。
【００９２】
また、ステップ１２０２、ステップ１２０６における判定結果がＮｏであった場合に、「検証未済」を出力するのではなく、「検証エビデンスが存在しない」、「検証対象データ不一致」といった情報を出力してもよい。同様に、ステップ１２１０において、単に検証未済を出力するのではなく、「検証失敗」、「検証未了」など、検証結果をそのまま出力するようにしてもよい。
【００９３】
なお、本実施例では、ハッシュ値を用いて検証エビデンスを生成する方法を記載したが、ハッシュ値に代えて検証対象設計情報の要約値を表す他の値を用いてもよい。例えば、ハッシュ値の代わりに、検証者の電子署名値を用いてもよい。その場合には、ステップ１００２におけるハッシュ値の計算は、検証支援装置１００の利用者による電子署名の署名生成処理となり、ステップ１２０５、ステップ１２０６における検証対象設計情報と検証対象エビデンス内のハッシュ値の比較は、電子署名の署名検証処理となる。この場合、検証支援装置１００には、電子署名生成のための秘密鍵を格納するための電子署名用秘密鍵格納装置が、また上記署名検証処理のため、電子署名用公開鍵格納装置が必要となる。なお、電子署名用秘密鍵と電子署名用公開鍵は、変更後の設計情報を検証するユーザが、変更前の設計情報の作成者と同一とは限らないため、電子署名用秘密鍵格納装置と電子署名用公開鍵格納装置に格納される電子署名用秘密鍵、電子署名用公開鍵は、必ずしも対になる電子署名用秘密鍵、電子署名用公開鍵でなくてもよい。
【００９４】
また、本実施例では、検証対象設計情報（を連結したもの）からハッシュ値を計算しているが、検証対象設計情報に検証結果や検証時間を含めた上でハッシュ値を計算するようにしてもよい。
【００９５】
図１４は、本実施例における検証支援装置１００の画面イメージの一例（検証支援画面１３００）を表している。検証支援画面１３００は、検証支援部１０３によって生成され、入出力制御部１０２を介して、表示部１０３に出力され、表示装置２０３に表示される。また、入力部１０１により、ユーザ入力を受け付け、設計情報６００の検証や検証結果の確認処理を行う。
【００９６】
図１４に示した通り、検証支援画面１３００は、設計情報を読込むためのファイルメニュー１３０１、設計情報に対し、検証要件を選択するための検証メニュー１３０２、及び検証支援装置１００の利用方法等を表示するヘルプメニュー１３１０の各メニューを含んで構成される。
【００９７】
また、検証支援画面１３００は、設計情報６００の内、線路形状３００を表示するための形状設計上表表示部１３１０、閉そくテーブル３２０、幾何テーブル３２１を表示するテーブル設計情報表示部１３１１、及び検証要件に対し、各検証範囲の検証結果、検証する範囲を選択するための検証結果表示部１３１２を備える。
【００９８】
検証支援装置１００のユーザは、ファイルメニュー１３０１から設計情報６００の格納されたファイルを指定して、設計情報６００を読み込ませる。次に、ユーザは、検証メニュー１３０２から、検証要件を選択する。この時、形状設計情報表示部１３１０には、検証範囲と対応する線路形状３００、及びテーブル設計情報１３１１には、対応する閉そくテーブル３２０、または、幾何テーブル３２１が表示される。また、設計情報６００内に含まれる検証範囲とその検証結果が、検証結果表示部１３１２を表示される。
【００９９】
ユーザは、検証結果表示部１３１２内に表示された検証範囲のチェック欄から検証範囲を選択する。次に、選択した検証範囲に対して、検証処理を行う場合には、検証ボタン１３２０を選択する。検証結果を確認する場合には、検証確認ボタン１３２１を選択し、検証確認処理を行う。
【０１００】
なお、本実施例において、コード生成設定情報４００内に検証要件間の依存関係や、優先順位を設定するようにしてもよい。この場合、図５の検証処理は、優先順位の高い、または、依存元の検証要件について、ステップ５０３からステップ５０８の処理を行い、優先順位の高い、或いは、依存元の検証要件の検証に失敗、或いは、検証結果の確認結果が検証未済の場合には、以降の検証要件及び検証範囲の検証処理（ステップ５０５からステップ５０８）は、無条件で実行するようにしてもよい。
【０１０１】
また、本実施例では、検証コード６０５にモデル検査用仕様記述言語Ｐｒｏｍｅｌａを用い、検証部品コード生成情報６０１、検証エビデンス格納情報１１００にＸＭＬを用いて説明を行ったが、これらの記述方法は、本実施例に限る必要はない。例えば、前述のとおり、モデル検査用仕様記述言語Ｐｒｏｍｅｌａ以外のモデル検査用仕様記述言語を用いてもよい。また、検証部品コード生成情報６０１、検証エビデンス格納情報１１００は、ＸＭＬ以外の記述を用いてもよく、図８及び図１１に示す構成に限らなくてもよい。
【０１０２】
以上説明したように、本実施例に係る検証支援装置１００によれば、検証要件ごとの検証ベースコード６０３から自動生成された検証コード６０５を用いて設計情報６００の検証を自動的に行うことができる。したがって、ソフトウェア仕様の検証を効率良く行うことができる。
【０１０３】
また、本実施例に係る検証支援装置１００によれば、検証要件及び検証範囲ごとに検証コード６０５を生成することで分割検証を行うことが可能となる。したがって、１回の検証処理に係る処理負荷を低減し、検証処理を効率的に行うことができる。
【０１０４】
また、本実施例に係る検証支援装置１００によれば、検証コード６０５を用いた検証の結果と、検証コード６０５に用いられた検証対象設計情報を示す検証対象設計情報参照情報と、検証対象設計情報のハッシュ値とを設定した検証エビデンスを作成することができる。したがって、検証エビデンスを参照することにより、検証の要否を判定することができる。
【０１０５】
検証エビデンスには前回の検証結果が含まれているので、検証結果に応じた検証の要否を容易かつ迅速に判定することができる。本実施形態の検証支援装置１００では、検証結果が「成功」の場合には「検査済」を出力するので、ユーザは再検査が不要であることを把握することが可能となり、不要な再検査を行わないようにして、効率良く検証を行うことができる。
【０１０６】
また、検証エビデンスには検証対象設計情報参照情報が含まれているので、検証処理に用いる検証対象設計情報が設計情報６００に存在しているかどうかを確認することができる。本実施形態の検証支援装置１００では、検証対象設計情報参照情報により特定される検証対象設計情報が設計情報６００に存在しない場合（例えば、削除された場合など）には「検証対象なし」を出力するので、ユーザは再検証が必要である旨を容易に把握することができる。また、検証の対象となる設計情報６００に大きな変更があるような場合には、検証内容自体も変更する必要があるが、本実施形態の検証支援装置１００によれば、検証対象設計情報が存在しない場合には「検証対象なし」を出力することができるので、ユーザは検証内容に変更が必要であることを容易に確認することもできる。
【０１０７】
また、検証エビデンスには検証対象設計情報の内容（を示すハッシュ値）が含まれているので、検証時に使用した検証対象設計情報の内容がどのようなものであったのかを容易に把握することができる。現状の設計情報６００から抽出した検証対象設計情報の内容とを比較することにより、検証後に検証対象設計情報に変更があったかどうかを容易に把握することができる。したがって、検証対象設計情報の内容に変更がなければ検証を行わないようにすることが可能となり、不要な再検証を行わないようにして、効率の良い検証を行うことができる。本実施例の検証支援装置１００では、検証エビデンスに含まれるハッシュ値と、検証対象設計情報参照情報により特定される検証対象設計情報から算出したハッシュ値とを比較して、これが一致しない場合には「検証未済」を出力することができる。したがって、ユーザは検証対象設計情報の内容に変更があったことを容易に把握することが可能となり、これに伴い再検証が必要である旨を容易に判断することができる。
【０１０８】
このように、本実施例の検証支援装置１００からの出力に応じて、検証対象設計情報に変更がなく、前回の検証結果が検証成功である場合には、再検証を行わないようにすることができる。これにより、設計情報６００を修正した場合においても、検証を行う必要のない検証要件については検証を省略することが可能となり、効率的良く検証を行うことができる。
【０１０９】
また、本明細書の記載により、少なくとも次のことが明らかにされる。  
すなわち、本発明の仕様検証支援装置であって、前記検証エビデンスに含まれる前記参照情報により特定される前記検証対象設計情報を前記設計情報から抽出し、前記抽出した検証対象設計情報の内容と、前記検証エビデンスに含まれている前記内容情報が表す内容とを比較して検証の要否を判定する検証結果確認処理部をさらに備えること、を特徴とする仕様検証支援装置。これによれば、検証後に検証対象設計情報に変更があったかどうかに応じて検証の要否を判断することができるので、検証対象設計情報の内容に変更がない場合には検証不要として、不要な再検証を行わないようにして、効率の良い検証を行うことができる。
【０１１０】
また、本発明の仕様検証支援装置であって、前記検証確認結果処理部は、前記検証エビデンスに含まれる前記検証結果に応じて検証の要否を判定し、検証不要と判定した場合にのみ、前記抽出した検証対象設計情報の内容と前記検証エビデンスに含まれている前記内容情報が表す内容とを比較してさらに検証の要否を判定すること、を特徴とする仕様検証支援装置。これによれば、前回の検証に成功していない場合には直ちに再検証が必要と判断するとともに、前回の検証に成功していたとしても、検証対象設計情報の内容に変更があるか否かにより再検証の要否をさらに判断することができる。したがって、再検証の要否を効率良く判断しつつ、検証が必要な場合には確実に再検証を行うことが可能となる。
【０１１１】
また、本発明の仕様検証支援装置であって、前記検証エビデンス生成処理部は、前記検証対象設計情報を所定のハッシュ関数に与えて前記内容情報を算出すること、を特徴とする仕様検証支援装置。これによれば、検証対象設計情報の内容の全てを検証エビデンスに残すことなく、検証対象設計情報に変更があったか否かを判断するために必要な情報は残すようにすることができる。したがって、検証エビデンスの蓄積に必要な記憶領域を圧縮することを可能としつつ、効率的な検証を行うことができる。
【０１１２】
また、本発明の仕様検証支援装置であって、前記検証ベースコードに追加する処理を所定方式で記述したコードである検証部品コードを生成するためのひな形である検証部品コード生成情報を記憶する検証部品コード生成情報格納部をさらに備え、前記検証コード生成処理部は、前記検証対象設計情報を前記所定方式で記述した検証データコードを生成し、前記検証部品コード生成情報及び前記検証対象設計情報に基づいて前記検証部品コードを生成し、前記検証データコード及び前記検証部品コードを前記検証ベースコードに適用して前記検証コードを生成すること、を特徴とする仕様検証支援装置。これによれば、実行すべき検証ロジックなどを記載した検証部品コードを検証コードに動的に組み入れることができる。したがって、検証に必要な検証対象設計情報を検証データコードとして検証コードの中に記述するとともに、検証に必要なロジックを検証対象設計情報に応じて動的に生成することができる。これにより、検証コードを自動生成する自由度を広げることができる。
【０１１３】
また、本実施例の検証支援装置１００によれば、分割検証された検証コード６０５それぞれについて検証エビデンスを生成することができる。したがって、細かい単位で前記検証エビデンスを用いた再検証の要否を判定することが可能となる。よって、設計変更時においても、設計変更箇所が偏在しているような場合には、不要な再検証を回避することが可能となり、設計情報修正時における再検証にかかるコストを低減することができる。
【０１１４】
以上、本実施形態について説明したが、上記実施形態は本発明の理解を容易にするためのものであり、本発明を限定して解釈するためのものではない。本発明は、その趣旨を逸脱することなく、変更、改良され得ると共に、本発明にはその等価物も含まれる。
【符号の説明】
【０１１５】
１００  検証支援装置
１０１  入力部
１０２  入出力制御部
１０３  表示部
１０４  検証結果確認処理部
１０５  検証エビデンス生成処理部
１０６  検証結果分析処理部
１０７  検証コード生成処理部
１０８  検証支援処理部
１０９  検証処理部
１１０  検証エビデンス格納部
１１１  検証結果格納部
１１２  検証コード格納部
１１３  検証用設定情報格納部
１１４  検証ベースコード格納部
１１５  検証部品コード生成情報格納部
１１６  コード生成設定情報格納部
１１７  設計情報格納部
２００  電子計算機
２０１  ＣＰＵ
２０２  ＲＡＭ
２０３  表示装置
２０４  入力装置
２０５  インターフェイス
２１０  外部記憶装置
４００  コード生成設定情報
６００  設計情報
６０１  検証部品コード生成情報
６０２  検証用データコード
６０３  検証ベースコード
６０４  検証部品コード
６０５  検証コード
６１０  検証データコード生成処理部
６１１  検証部品コード生成処理部
６１２  検証コード構成処理部
１１００  検証エビデンス格納情報
１１０１  検証エビデンス
【図１】
2014164677.tif 000003
【図２】
2014164677.tif 000004
【図３】
2014164677.tif 000005
【図４】
2014164677.tif 000006
【図５】
2014164677.tif 000007
【図６】
2014164677.tif 000008
【図７】
2014164677.tif 000009
【図８】
2014164677.tif 000010
【図９】
2014164677.tif 000011
【図１０】
2014164677.tif 000012
【図１１】
2014164677.tif 000013
【図１２】
2014164677.tif 000014
【図１３】
2014164677.tif 000015