"検証要件に基づくソフトウェアの検証を支援するソフトウェア検証支援装置であって、ソフトウェアから機能モデルを生成する機能モデル生成手段と、前記機能モデル生成手段で生成した機能モデルに基づいて検証要件を生成する検証要件生成手段と、を備えることを特徴とするソフトウェア検証支援装置。前記検証要件生成手段は、機能モデルから検証対象のパターンとマッチングする機能要素を抽出し、当該抽出した機能要素に基づいて検証要件を生成することを特徴とする請求項1に記載のソフトウェア検証支援装置。前記検証要件生成手段は、機能モデルをスナップショットに分解し、当該分解したスナップショットに基づいて検証要件を生成することを特徴とする請求項1に記載のソフトウェア検証支援装置。前記検証要件生成手段で生成した検証要件からソフトウェアに入力するテストを生成するテスト生成手段を備えることを特徴とする請求項1~請求項3のいずれか1項に記載するソフトウェア検証支援装置。前記各生成手段で生成されるものを表示する表示手段を備えることを特徴とする請求項1~請求項4のいずれか1項に記載するソフトウェア検証支援装置。検証要件に基づくソフトウェアの検証を支援するソフトウェア検証支援方法であって、ソフトウェアから機能モデルを生成する機能モデル生成ステップと、前記機能モデル生成ステップで生成した機能モデルに基づいて検証要件を生成する検証要件生成ステップと、を含むことを特徴とするソフトウェア検証支援方法。検証要件に基づくソフトウェアの検証を支援するためのソフトウェア検証支援プログラムであって、コンピュータに、ソフトウェアから機能モデルを生成する機能モデル生成機能と、前記機能モデル生成機能で生成した機能モデルに基づいて検証要件を生成する検証要件生成機能と、を実現させることを特徴とするソフトウェア検証支援プログラム。ソフトウェアは、計算負荷低減や関連の無い機能をひとつのプログラムにまとめるなど、実装上の理由で必ずしも各機能を人が理解し易い形で記述されていない。また、ある一つのシステムのソフトウェアが、異なる複数の言語で記述されている場合もある。このような理由などからソフトウェアから各機能を読み解くのは難しく、スキルを要する作業である。そのため、人が検証要件を決定する場合、人によって検証要件の品質がばらつく。また、ソフトウェアの構造のみに基づいて検証要件を決定する場合、検証で網羅すべき基準がソフトウェアの構造に基づいたものになるため、検証すべき機能を網羅した検証要件を抽出できない。その結果、検証モレが生じる。また、上記の特許文献1の検証支援は検証対象がハードウェアの回路であり、レジスタの状態変化に着目して検証要件を抽出しているので、ソフトウェアの検証要件の抽出には適用できない。そこで、本発明は、検証モレを抑制したソフトウェアの検証を可能とするソフトウェア検証支援装置、ソフトウェア検証支援方法及びソフトウェア検証支援プログラムを提供することを課題とする。本発明に係るソフトウェア検証支援装置は、検証要件に基づくソフトウェアの検証を支援するソフトウェア検証支援装置であって、ソフトウェアから機能モデルを生成する機能モデル生成手段と、機能モデル生成手段で生成した機能モデルに基づいて検証要件を生成する検証要件生成手段とを備えることを特徴とする。このソフトウェア検証支援装置では、機能モデル生成手段によって検証対象のソフトウェアから機能モデルを生成する。機能モデルは、ソフトウェアの機能を網羅したモデルであり、ソフトウェアの検証すべきある一面ポイントを抽出してモデル化したものである。また、機能モデルは、人に目に見える形で示すことができ、人がソフトウェアの機能を容易に読み解けるようにモデル化したものである。このような機能モデルを生成すると、ソフトウェア検証支援装置では、検証要件生成手段によってその機能モデルに基づいて検証要件を生成する。このように、ソフトウェア検証支援装置は、ソフトウェアから機能モデルを生成して、機能モデルから検証要件を生成することにより、機能モデルから検証すべき機能を網羅した検証要件を簡単かつ自動で生成でき、その検証要件に基づいてソフトウェアを検証することによって検証モレを抑制することができる。また、ソフトウェアが異なる複数の言語で記述されている場合でも、そのソフトウェアを機能モデルで統一的に扱うことができ、機能モデルから検証要件を簡単に生成できる。なお、検証対象のソフトウェアの記述言語としては、様々な言語が適用可能であり、例えば、C言語等の手続き型言語、Simulinkなどのモデリング言語がある。機能モデルとしては、例えば、制御フローであればデータフローグラフDataflowgraphモデル、制御モードの切り替えであれば状態遷移モデル、タイミングの問題であればTimedAutomataがある。本発明の上記ソフトウェア検証支援装置では、検証要件生成手段は、機能モデルから検証対象のパターンとマッチングする機能要素を抽出し、当該抽出した機能要素に基づいて検証要件を生成する構成としてもよい。このソフトウェア検証支援装置では、機能モデルから検証対象のパターンすなわち、検証したい機能のパターンにマッチングする機能要素を抽出して検証要件を生成することにより、機能モデルから検証すべき機能を網羅した検証要件を簡単かつ高精度に抽出できる。本発明の上記ソフトウェア検証支援装置では、検証要件生成手段は、機能モデルをスナップショットに分解し、当該分解したスナップショットに基づいて検証要件を生成する構成としてもよい。このソフトウェア検証支援装置では、機能モデルをスナップショットに分解して検証要件を生成することにより、機能モデルから検証すべき機能を網羅した検証要件を簡単かつ高精度に抽出できる。本発明の上記ソフトウェア検証支援装置では、検証要件生成手段で生成した検証要件からソフトウェアに入力するテストを生成するテスト生成手段を備える構成としてもよい。このソフトウェア検証支援装置では、検証要件からテストを自動生成し、このテストを入力してソフトウェアを検証することにより、検証すべき機能を効率的に検証することができる。本発明の上記ソフトウェア検証支援装置では、各生成手段で生成されるものを表示する表示手段を備える構成としてもよい。表示手段で表示するものとしては、例えば、機能モデル、検証要件、検証対象パターン、分解されたスナップショット、検証要件に応じたテストがある。このソフトウェア検証支援装置では、各生成手段で生成したものを表示することにより、検証を行う人に機能モデルや検証要件などを明示することができ、人がソフトウェアの機能構成や検証すべき要件などを容易に認識できる。本発明に係るソフトウェア検証支援方法は、検証要件に基づくソフトウェアの検証を支援するソフトウェア検証支援方法であって、ソフトウェアから機能モデルを生成する機能モデル生成ステップと、機能モデル生成ステップで生成した機能モデルに基づいて検証要件を生成する検証要件生成ステップとを含むことを特徴とする。このソフトウェア検証支援方法によれば、各ステップの処理を行うことにより、上記ソフトウェア検証支援装置の作用及び効果を奏する。本発明に係るソフトウェア検証支援プログラムは、検証要件に基づくソフトウェアの検証を支援するためのソフトウェア検証支援プログラムであって、コンピュータに、ソフトウェアから機能モデルを生成する機能モデル生成機能と、機能モデル生成機能で生成した機能モデルに基づいて検証要件を生成する検証要件生成機能とを実現させることを特徴とする。このソフトウェア検証支援プログラムによれば、このプログラムをコンピュータに実行させることによって、上記ソフトウェア検証支援装置の作用及び効果を奏する。本発明によれば、ソフトウェアから機能モデルを生成して、機能モデルから検証要件を生成することにより、機能モデルから検証すべき機能を網羅した検証要件を簡単かつ自動で生成でき、その検証要件に基づいてソフトウェアを検証することによって検証モレを抑制することができる。以下、図面を参照して、本発明に係るソフトウェア検証支援装置、ソフトウェア検証支援方法及びソフトウェア検証支援プログラムの実施の形態を説明する。なお、各図において同一又は相当する要素については同一の符号を付し、重複する説明を省略する。本実施の形態では、本発明を、任意のシステムを制御する制御ソフトウェアを検証する制御ソフトウェア検証装置に適用する。本実施の形態に係る制御ソフトウェア検証装置は、検証対象の制御ソフトウェアが入力されると、制御ソフトウェアの検証要件を自動で生成し、その検証要件に応じて制御ソフトウェアを検証する。本実施の形態には、2つの形態があり、第1の実施の形態が基本の形態であり、第2の実施の形態が基本の形態に加えて制御ソフトウェアに入力するテストを自動生成する機能も有する形態である。本実施の形態に係る制御ソフトウェア検証装置は、制御ソフトウェアの検証だけを行う専用装置でもよいし、あるいは、汎用コンピュータで制御ソフトウェア検証用のアプリケーションを実行することによって構成されてもよい。なお、検証対象のソフトウェアは、単一の言語で記述されてものでもよいし、あるいは、異なる複数の言語で記述されたものでもよい。記述言語としては、様々な言語が適用可能であり、例えば、C言語などの手続き型言語、Simulinkなどのデータフロー型のモデリング言語がある。まず、図1を参照して、本実施の形態に係る制御ソフトウェア検証装置の概要について説明する。図1は、本実施の形態に係る制御ソフトウェア検証装置の概念図である。図1では、実線で接続する構成が制御ソフトウェア検証装置の最大の構成であり、破線で接続する各構成各組み合わせが制御ソフトウェア検証装置の最小の構成である。まず、制御ソフトウェア検証装置では、検証対象の制御ソフトウェアから機能モデルを生成する。機能モデルは、制御ソフトウェアの機能を網羅したモデルであり、制御ソフトウェアの検証すべきある一面ポイントを抽出してモデル化したものである。また、機能モデルは、人の目に見える形で示すことができ、人が制御ソフトウェアの機能を容易に読み解けるようにモデル化したものである。このように機能モデルという形で人に明示することができるので、人が機能モデルを見て検証すべき機能が網羅されているかが容易に判る。制御ソフトウェアを実現している制御機能は様々な側面を持つので、機能モデルとしては、その制御機能の各側面に応じたものでモデル化され、例えば、制御フローであればデータフローグラフモデルDFGモデル、制御モードの切り替えであれば状態遷移モデル、タイミングの問題であればTimedAutomataがある。なお、本実施の形態では、データフローグラフモデルの場合を例にして説明する。次に、制御ソフトウェア検証装置では、機能モデルから検証要件を生成する。検証要件は、制御ソフトウェアにおいて検証すべき機能の要件である。この検証要件の生成手法には、パターンマッチングとスナップショット分解の2つの手法がある。パターンマッチング手法では、機能モデルから検証パターンとマッチングする機能要素を抽出し、その抽出した機能要素に基づいて検証要件を生成する。検証パターンは、機能モデルの中で検証したい機能のパターンであり、人によって決められる。スナップショット分解手法では、機能モデルをスナップショットに分解し、その分解したスナップショットに基づいて検証要件を生成する。機能モデルのスナップショットは、機能モデルの中で特定の瞬間タイミングで成立しているパターンであり、機能モデルの中で可能な全てのパターンでもよいしあるいは一部のパターンでもよい。一部のスナップショットだけを用いる場合、制御機能の重要性などから、人によって決められる。次に、制御ソフトウェア検証装置では、生成した検証要件に応じて制御ソフトウェアを検証する。ここでは、検査パスを決定するために、カバレッジモニタやテスト自動生成を利用する。カバレッジモニタでは、カバレッジ基準として制御ソフトウェアの検証すべき機能をどの程度網羅しているかを明示するために生成された検証要件をモニタに表示する。テスト自動生成では、生成された検証要件から制御ソフトウェアのテスト入力をモデル検査器を用いて自動生成する。そして、この生成されたテスト入力を制御ソフトウェアに入力して検証を行う。なお、検証については、通常は専用の装置や汎用コンピュータによって行うが、検証要件に基づいて人が行ってもよい。図2を参照して、第1の実施の形態に係る制御ソフトウェア検証装置1について説明する。図2は、第1の実施の形態に係る制御ソフトウェア検証装置の構成図である。制御ソフトウェア検証装置1は、検証対象の制御ソフトウェアSが入力されると、制御ソフトウェアSからデータフローグラフ機能モデルMを生成し、データフローグラフから検証要件を生成し、制御ソフトウェアSに対して検証要件に応じた検証を行い、検証結果Rを出力する。そのために、制御ソフトウェア検証装置1は、機能モデル生成手段10、検証要件生成手段11、検証手段12を備えている。入力される制御ソフトウェアSは、任意の言語によって記述され、ソフトウェアモデルSMやプログラムSPとして構成される。また、制御ソフトウェアSは、単一の言語で記述されたものでもよいし、あるいは、複数の異なる言語で記述されたものでもよい。例えば、図3には、ある制御について、単一のC言語で記述されたCコードプログラムSP1の一例を示している。このCコードプログラムSP1では、変数t以外は全てグローバル変数である。また、図5には、図3と同じ制御について2つの言語で記述された場合の一例を示しており、図bに前半部がSimulinkで記述されたSimulinkモデルSM2と図cに後半部がC言語で記述されたCコードプログラムSP2を示している。機能モデル生成手段10では、制御ソフトウェアSが入力されると、制御ソフトウェアSから機能モデルMとしてデータフローグラフを生成する。制御ソフトウェアSは上記したように部分的に異なる言語で記述されることもあるが、データフローグラフという機能モデルを定義することにより、記述言語にかかわらず、入力から出力へのデータフローとその切り替えという制御機能の一面を抽出することができる。データフローグラフは、プログラムの演算や分岐をノード、変数をエッジで表現されたグラフとしてモデリングされたものである。この生成されたデータフローグラフ機能モデルMは、モニタ表示手段に表示され、検証対象の人が視覚的に確認できる。データフローグラフの生成は、従来の手法を適用する。例えば、手続き型のプログラムの場合、プログラムの構文を解析し、そのプログラムの構文解析結果に基づいてプログラムのコントロールフローグラフControlflowgraphを生成し、コントロールフローグラフを用いてグローバル変数についての到達定義を算出し、各ノードの到達定義集合を用いて出力変数から到達定義を逆順に追跡し、その追跡結果に基づいて出力変数を出力とするデータフローグラフを生成する。図4には、図3に示すCコードプログラムSP1のデータフローグラフDFG1を示している。データフローグラフは、演算が四角形で表され、セレクタが菱形で表され、入出力ポートが楕円で表され、参照する変数が矢印エッジに付加され、参照する定数値が矢印の末端に付加される。このデータフローグラフDFG1は、goutを出力変数とするものである。したがって、データフローグラフDFG1では、goutに関連する演算フローだけが理解し易い形で抽出されている。また、図5に示すSimulinkモデルSM2とCコードプログラムSP2で構成される制御ソフトウェアについても、図4と同様のデータフローグラフDFG1となる。図5aに示すように、このデータフローグラフDFG1のうち、破線で区切られる左上部分がSimulinkモデルSM2に対応する部分DFG1Mであり、右下部分がCコードプログラムSP2に対応する部分DFG1Pである。検証要件生成手段11では、機能モデルMとしてデータフローグラフが生成されると、そのデータフローグラフから検証要件Cを生成する。検証要件の生成手法としては、上記したようにパターンマッチングによる手法とスナップショット分解による手法があり、いずれか一方の手法を用いるか、あるいは、2つの手法を組み合わせて用いる。まず、パターンマッチングについて説明する。まず、データフローグラフの中から検証パターンにマッチングする部分機能要素を抽出する。検証パターンは、検証が必要とされるパターン分岐、演算等であり、局所的なパターンを持つ機能要素に相当する。検証パターンは、検証する人が予め決めて、制御ソフトウェア検証装置1に予め登録されているものでもよいし、あるいは、検証する人がモニタ表示されるデータフローグラフを見て選択されるものでもよい。検証パターンを容易に決めるために、制御ソフトウェア検証装置1内にデータベースを構築し、そのデータベースに定型的な検証パターンを登録しておき、データベースから検証パターンを選択できるようにするとよい。図6には、検証パターンの例として、図aに検証パターンIP1と図bに検証パターンIP2を示している。このような検証パターンを、モニタに表示してもよい。図7には、図4に示すデータフローグラフDFG1において図6aに示す検証パターンIP1にマッチングする部分IP1’と図6bに示す検証パターンIP2にマッチングする部分IP2’を示している。このようなデータフローグラフにおいて検証パターンにマッチングする部分を強調してモニタに表示してもよい。次に、制御ソフトウェアSから、データフローグラフにおいて検証パターンにマッチングする部分機能要素に相当する部分を抽出し、その制御ソフトウェアSにおいて検証パターンに相当する部分から検証要件Cを生成する。このように人の目に見える形で判り易くモデル化されているデータフローグラフ機能モデルMから抽出される検証パターンにマッチングする部分を利用することにより、検証要件Cを容易に生成でき、検証モレを抑制できる。図8には、CコードプログラムSP1において、図7で示される検証パターンIP1にマッチングする部分機能要素IP1’と検証パターンIP2にマッチングする部分機能要素IP2’に相当する各行を示しており、機能要素IP1’に相当する行が5-7行であり、機能要素IP2’に相当する部分が17-18行である。この例の場合、CコードプログラムSP1の5-7行と17-18行をカバーする検証を実行することが検証要件Cとなり、5-7行のパスの成立条件はP==TRUEandR==TRUEであり、17-18行のパスの成立条件はQ==TRUEである。生成された検証要件Cは、モニタに表示され、検証対象の人が視覚的に確認できる。次に、スナップショット分解について説明する。図9の例で、スナップショット分解の概要を説明する。データフローDFは、処理Aの出力変数e1と処理Bの出力変数e2がセレクタSL1で切り替えられ、セレクタSL1の出力変数が処理Cに入力され、処理Cの出力変数e3と処理Dの出力変数e4がセレクタSL2で切り替えられて出力される。ここで、各セレクタSL1,SL2で切り替えられるデータフローに対し、セレクタSL1,SL2毎にエッジを一つずつ選択するとすなわち、スナップショット分解、入力から出力まで切り替えの無いデータフロースナップショットが得られる。スナップショットSS1は、セレクタSL1で処理Aの出力変数e1が選択されかつセレクタSL2で処理Cの出力変数e3が選択されたデータフローである。スナップショットSS2は、セレクタSL1で処理Bの出力変数e2が選択されかつセレクタSL2で処理Cの出力変数e3が選択されたデータフローである。スナップショットSS3は、セレクタSL2で処理Dの出力変数e4が選択されたデータフローである。制御機能の観点からこれらスナップショットはある瞬間に成立している機能制御モードと考えることができ、制御機能全体はこれらの制御モードを適宜切り替えることで実現されていると考えることができる。したがって、このようなスナップショットはデータフローにおける各機能を構成要素に分解したものとして考えることができ、機能要素に応じて検証を行うことによりモレの無い検証ができる。そこで、まず、データフローグラフに含まれるセレクタ毎にエッジを一つずつ選択し、入力から出力まで切り替えの無いスナップショットデータフローグラフを生成する。ここでは、全てのセレクタについての全ての切り替えの組み合わせを構成した場合の全てのパターンについてのスナップショットデータフローグラフを生成してもよいし、あるいは、一部のパターンについてのスナップショットデータフローグラフを生成してもよい。一部のパターンの場合には、検証する人が、生成するパターンを制御モードの重要性に応じて決めるようにするとよい。例えば、検証する人がインタラクティブに、モニタに表示されるデータフローグラフを見ながらデータフローグラフの中で切り替えられるエッジ等を選択できるようにするとよい。生成されたスナップショットデータフローグラフは、モニタに表示され、検証対象の人が視覚的に確認できる。図10には、図4に示すデータフローグラフDFG1をスナップショット分解した例を示しており、3つのセレクタGSL1、GSL2,GSL3について各エッジの切り替えの全ての組み合わせを考えることで、4つのスナップショットデータフローグラフSSDFG1,SSDFG2,SSDFG3,SSDFG4が得られる。図aに示すスナップショットデータフローグラフSSDFG1は、セレクタGSL3で定数値0のエッジが選択された場合である。図bに示すスナップショットデータフローグラフSSDFG2は、セレクタGSL1で変数x=0のエッジが選択された場合である。図cに示すスナップショットデータフローグラフSSDFG3は、セレクタGSL1で変数x=ginのエッジが選択された場合である。図dに示すスナップショットデータフローグラフSSDFG4は、セレクタGSL2で変数x=ginのエッジが選択された場合である。次に、スナップショットデータフローグラフに相当する部分を制御ソフトウェアSから抽出し、その制御ソフトウェアSにおいてスナップショットデータフローグラフに相当する部分から検証要件Cを生成する。このように人の目に見える形で判り易く各機能要素に分解されたスナップショットデータフローグラフを利用することにより、検証要件を容易に抽出でき、検証モレも抑制できる。図11には、CコードプログラムSP1において、図10dに示されるスナップショットデータフローグラフSSDFG4に相当する行を示しており、四角形で囲んだ2、4、11-12、16、20行である。この例の場合、このパスの成立条件はP==FALSEandQ==FALSEであり、これが検証要件Cとなる。生成されたこの検証要件Cは、モニタに表示され、検証対象の人が視覚的に確認できる。検証手段12では、検証要件Cが生成されると、検証要件Cに応じて制御ソフトウェアSを検証し、検証結果Rを出力する。ここでは、生成された検証要件Cをガバレッジ基準として適用し、検証を行う。検証方法としては、従来の様々な方法を適用でき、例えば、検証要件Cすなわち、機能要素に応じて、実機試験、HILSHardwareIntheLoopSimulatorやSILSSoftwareIntheLoopSimulatorなどの閉ループシミュレーション、ユニットテストなどの制御ソフトウェアSの一部分を切り出したテスト、モデル検査がある。出力される検証結果Rは、モニタに表示され、検証対象の人が視覚的に確認できる。図12aには検証手段12の構成の一例として、実機検証試験における内部状態の監視システムを示している。この検証手段12Aは、制御対象12aを制御装置12bで制御する実機システムに対して、試験条件入力装置12cと内部状態監視装置12dを備える。例えば、検証対象の制御ソフトウェアSが自動車のエンジンを制御するためのソフトウェアの場合、制御対象12aはエンジンであり、制御装置12bはエンジンを制御するためのECUElectronicControlUnitである。制御装置12bには、検証対象の制御ソフトウェアSの実行ファイルが組み込まれる。試験条件入力装置12cは、検証要件C毎に、検証要件Cを満たすための試験条件テスト入力を入力するための装置である。内部状態監視装置12dは、試験条件を入力後、制御装置12bによって制御対象12aを制御しているときに、制御装置12bのRAM値などを監視することによって内部状態を監視する装置である。このように内部状態を監視することによって、検証要件Cが網羅された試験となっているか、検証要件C毎に制御ソフトウェアSが検証要件Cを満たすように正常に動作しているかなどを検証する。この内部状態は、モニタに表示され、検証対象の人が視覚的に確認できる。図12bには検証手段12の構成の他の例として、HILS試験における内部状態の監視システムを示している。この検証手段12Bは、制御対象モデル演算装置12eを制御装置12bで制御するシミュレーションシステムに対して、試験条件入力装置12cと内部状態監視装置12dを備える。制御対象モデル演算装置12eは、制御対象の動作をシミュレートするシミュレータである。このように、検証手段12Bでは、検証手段12Aと比較すると実機の代わりにシミュレータ制御対象モデル演算装置12eを用いて検証を行う。内部状態を監視する方法としては、様々な方法がある。その一例として、図13を参照して、検証対象のプログラムSPに監視すべき情報を組み込む方法について説明する。まず、検証対象プログラムSPに監視コードを埋め込み、監視コード付プログラムCSPを作成する。図14には、図4に示すCコードプログラムSP1に、図10dに示されるスナップショットデータフローグラフSSDFG4から生成された検証要件Cであるパス成立条件P==FALSEandQ==FALSEが成立したことを検証するために必要な監視コードWC1,WC2,WC3,WC4,WC5,WC6,WC7を埋め込んだ監視コード付プログラムCSP1を示している。そして、その監視コード付プログラムCSPをクロスコンパイルして実行ファイルEFを作成し、その実行ファイルEFを制御装置12bに転送して、制御装置12bに組み込む。これによって、図12に示すような試験環境において、制御装置12bに組み込まれた検証対象プログラムSPが検証要件Cを満たすように動作しているか否かを監視することが可能となる。なお、上記のような実機やシミュレータを用いた検証について説明したが、制御ソフトウェアSのユニットテストなどでも、同様に、検証要件Cをガバレッジ基準として適用した検証を行うことができる。この制御ソフトウェア検証装置1によれば、制御ソフトウェアSの機能構成を網羅しかつ視覚的に把握し易い機能モデルMを生成し、機能モデルMから検証要件Cを生成することにより、機能モデルMから検証すべき機能を網羅した検証要件Cを簡単かつ自動で生成でき、その検証要件Cに基づいて制御ソフトウェアSを検証することによって検証モレを抑制することができる。また、制御ソフトウェアSが異なる複数の言語で記述されている場合でも、その制御ソフトウェアSを機能モデルMで統一的に扱うことができるので、機能モデルMから検証要件Cを簡単に生成できる。また、機能モデルMを用いて検証要件Cを生成することにより、人のスキルに依存しないで検証要件Cを生成して検証を行うことができる。また、制御ソフトウェア検証装置1によれば、機能モデルMから検証要件Cを生成するためにパターンマッチングやスナップショット分解を用いることにより、機能モデルMから検証すべき機能を網羅した検証要件Cを簡単かつ高精度に抽出できる。また、制御ソフトウェア検証装置1によれば、各生成手段10,11,12で生成したものをモニタ表示することにより、検証を行う人に機能モデルMや検証要件Cなどを明示することができ、人が制御ソフトウェアSの機能構成や検証すべき要件などを容易に理解できる。図15を参照して、第2の実施の形態に係る制御ソフトウェア検証装置2について説明する。図15は、第2の実施の形態に係る制御ソフトウェア検証装置の構成図である。制御ソフトウェア検証装置2は、第1の実施の形態に係る制御ソフトウェア検証装置1と比較すると、検証要件Cからテスト入力テストベクタTを自動で生成して検証を行う点が異なる。そのために、制御ソフトウェア検証装置2は、機能モデル生成手段20、検証要件生成手段21、検証手段22及びテスト入力生成手段23を備えている。なお、機能モデル生成手段20、検証要件生成手段21、検証手段22は、第1の実施の形態に係る機能モデル生成手段10、検証要件生成手段11、検証手段12と同様のものなので、説明を省略する。テスト入力生成手段23では、検証要件Cが生成されると、検証要件Cを満たすテスト入力Tを自動的に生成する。この生成手法としては、従来の手法を適用でき、例えば、ランダムテスト生成、モデル検査器を利用した手法がある。生成されたテスト入力Tは、モニタに表示され、検証対象の人が視覚的に確認できる。一例として、図16を参照して、モデル検査器を利用したテスト入力の生成について説明する。ここでは、図4に示すCコードプログラムSP1について、図10dに示されるスナップショットデータフローグラフSSDFG4から生成された検証要件Cのパス成立条件P==FALSEandQ==FALSEを成立させるためのテスト入力Tを生成する場合について説明する。まず、図16に示すように、CコードプログラムSP1に、パス成立条件P==FALSEandQ==FALSEを否定するような論理式を満たすべきプロパティP1及びその論理式に関連して必要な各コードTC1,TC2,TC3,TC4,TC5,TC6を埋め込み、プロパティ付プログラムPSP1を作成する。そして、このプロパティ付プログラムPSP1をモデル検査器にかけ、論理式の条件が成立しない入力の判例として検証要件Cのパス成立条件P==FALSEandQ==FALSEを満たすテスト入力Tを生成する。なお、C言語で記述されたプログラムの場合、CBMCというモデル検査ツールを適用できる。なお、このように生成されたテスト入力Tを用いて検証手段22で検証を行う場合、主に、制御ソフトウェアSのユニットテストなどが対象となり、制御ソフトウェアS単体の検証を行う。制御ソフトウェア検証装置2は、第1の実施の形態に係る制御ソフトウェア検証装置1と同様の効果を有する上に、以下の効果も有している。制御ソフトウェア検証装置2によれば、検証要件Cからテスト入力Tを自動生成し、このテスト入力Tを入力して制御ソフトウェアSを検証することにより、検証すべき機能を効率的に検証することができる。以上、本発明に係る実施の形態について説明したが、本発明は上記実施の形態に限定されることなく様々な形態で実施される。例えば、本実施の形態では制御ソフトウェアの検証要件を生成し、その検証要件に基づいて制御ソフトウェアの検証まで行う制御ソフトウェア検証装置に適用したが、ソフトウェアの検証要件やその検証要件に応じたテストを生成するためのソフトウェア検証支援装置に適用してもよい。また、CD-ROMなどの記憶媒体に格納されたプログラムやインタネットなどのネットワークを介して利用可能なプログラムなどに適用し、このようなプログラムをコンピュータ上で実行することによってソフトウェアの検証要件やその検証要件に応じたテストを生成する構成としてもよい。また、本実施の形態では自動車などの制御に用いられる制御ソフトウェアに適用したが、制御以外にも様々なソフトウェアに適用可能である。"