(57)【特許請求の範囲】
【請求項１】
モデル検査を実行するコンピュータが、
前記モデル検査の検査対象プログラムで用いるデータ項目各々について入力データ項目であるか出力データ項目であるかが定義されている定義テーブルを参照して、前記検査対象プログラムを実行する際に用いる検査条件の記述から入力データ項目と出力データ項目を抽出して、抽出した入力データ項目を生成対象項目として特定し、
前記検査条件の記述から抽出した前記出力データ項目に対応する前記検査対象プログラムの実行環境に記録されているデータを取得して、取得したデータに対応する前記出力データ項目のデータとして用いる形式に変換して出力データを生成し、
前記検査条件と前記出力データを、ＳＭＴソルバプログラムに入力するデータの形式に変換して生成条件を生成し、
前記生成条件を入力してＳＭＴソルバプログラムを実行し、前記生成条件を満たすデータを求め、該データから前記生成対象項目に対応するデータを抽出し、
抽出したデータを前記生成対象項目の入力として検査対象プログラムの実行環境に入力する、
ことを実行するデータ生成方法。
【請求項２】
モデル検査の検査対象プログラムで用いるデータ項目各々について入力データ項目であるか出力データ項目であるかが定義されている定義テーブルを参照して、前記検査対象プログラムを実行する際に用いる検査条件の記述から入力データ項目と出力データ項目を抽出して、抽出した入力データ項目を生成対象項目として特定する検査条件特定部と、
前記検査条件の記述から抽出した前記出力データ項目に対応する前記検査対象プログラムの実行環境に記録されているデータを取得して、取得したデータに対応する前記出力データ項目のデータとして用いる形式に変換して出力データを生成する出力データ取得部と、
前記検査条件と前記出力データを、ＳＭＴソルバプログラムに入力するデータの形式に変換して生成条件を生成する検査条件変換部と、
前記生成条件を入力してＳＭＴソルバプログラムを実行し、前記生成条件を満たすデータを求め、該データから前記生成対象項目に対応するデータを抽出するＳＭＴソルバ実行部と、
抽出したデータを前記生成対象項目の入力として検査対象プログラムの実行環境に入力させる生成データ通知部と、
を備えることを特徴とするデータ生成装置。
【請求項３】
モデル検査を実行させるコンピュータに、
前記モデル検査の検査対象プログラムで用いるデータ項目各々について入力データ項目であるか出力データ項目であるかが定義されている定義テーブルを参照して、前記検査対象プログラムを実行する際に用いる検査条件の記述から入力データ項目と出力データ項目を抽出して、抽出した入力データ項目を生成対象項目として特定する処理と、
前記検査条件の記述から抽出した前記出力データ項目に対応する前記検査対象プログラムの実行環境に記録されているデータを取得して、取得したデータに対応する前記出力データ項目のデータとして用いる形式に変換して出力データを生成する処理と、
前記検査条件と前記出力データを、ＳＭＴソルバプログラムに入力するデータの形式に変換して生成条件を生成する処理と、
前記生成条件を入力してＳＭＴソルバプログラムを実行し、前記生成条件を満たすデータを求め、該データから前記生成対象項目に対応するデータを抽出する処理と、
抽出したデータを前記生成対象項目の入力として検査対象プログラムの実行環境に入力させる処理と、
を実行させることを特徴とするデータ生成プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査に用いるテストデータを生成する技術に関する。
【背景技術】
【０００２】
従来のモデル検査は、まず擬似システムに予め作成したテストデータを、ドライバを用いて入力する処理を行う。ここで、擬似システムとは、検査対象のシステムの振る舞いを、該システムの設計書や仕様書などに基づいて専用言語などを用いて作成されるプログラムである。また、擬似システムである検査対象プログラムは、検査対象プログラムを動かすドライバとデータベースやネットワークなどの外部環境を抽象化するためのスタブなどと接続されている。ドライバは、検査対象プログラムを様々な実行順序で複数回、連続的に呼び出して、ユーザの操作を模倣したテストデータを引数として検査対象プログラムに渡す。
【０００３】
次にモデル検査では、該テストデータを用いて検査対象プログラムを実行する処理をして、該テストデータを用いた検査対象プログラムの実行結果が、プロパティに記録されている該テストデータに対応する検査条件を満たしているか否かを、判定する処理を行う。
【０００４】
そして、上記説明した処理を終了すると、現在の検査対象プログラムの状態に対するテストデータを、ドライバを用いて検査対象プログラムに入力する処理を再度行い、検査対象プログラムを実行して実行結果が、検査条件を満たしているか否かを判定する。
【０００５】
このように、モデル検査では設計書や仕様書などに基づき、検査対象プログラムの取りうる状態遷移の各状態が取りうる全ての組み合わせに対してテストデータを入力して、繰り返し実行する。
【０００６】
ところが、全ての組み合わせに対して網羅的にモデル検査を実施すには、検査対象プログラムのあらゆる動作を想定したテストデータを予め作成し、作成したテストデータを入力できるドライバが必要である。すなわち、検査対象プログラムのユーザ操作イベントおよびユーザ操作イベントの引数となるテストデータについて、仕様上可能な組み合わせを再現できるようにしなければならない。
【０００７】
例えば、Java PathFinderに代表されるモデル検査では、検査対象プログラムに入力するテストデータは検査対象プログラムの動作結果に依存して決定されるため、検査対象プログラムを動作させる前に具体的な値が決定できない。例えば、商品の注文を複数回連続して行える商品注文システムにおいて、注文できる数量が在庫数を超える場合は購入できないという仕様がある場合について考える。従来のドライバによるテストデータの生成では、在庫数量に対して具体的な値を設定して、ケースごとに在庫数量＜購入数量を満たす購入数量を求めている。在庫数量が１００個であれば、購入数量を１０１個とすることが考えられる。
【０００８】
しかし、購入によって在庫数量が変わると、１回目に購入できる数量と２回目に購入できる数量が異なる。そのため、２回目に購入できる数量を求めるには、１回目に購入した結果の在庫数量を算出する必要があり、在庫数量も算出に関するすべての仕様を判断できる形で記述する必要がある。例えば、１回目に購入数量＝９０個で購入したら、在庫数量は在庫数量（１００個）−購入数量（９０個）＝１０個になるので、次の購入時の境界値は１０個になる。しかし、在庫数量１０個を求めるには「在庫数量−数量が次の在庫数量になる」という仕様が記述されなければならないが、通常そのような仕様までドライバは対応していない。
【０００９】
また、前述の境界値により作成したデータを、２回目以降の購入でも使うと次のような問題が発生する。１回目に在庫数１００個のときに購入数量１００個で商品を購入した場合、在庫数量の境界値は０個になる。しかし、１回目と同じデータを用いると、在庫が無いにもかかわらず、在庫数量＜購入数量、在庫数量＝購入数量、在庫数量＞購入数量の場合について検査を実行しなくてはならない。例えば、購入数量が１０１個、１００個、９０個の３パターンについても検査を実行する。また、在庫数１００個のときに購入数量９０個で商品を購入した場合、在庫数量の境界値は１０個になるが、１回目と同じデータを用いていると在庫数量が１０個で同じように３パターンについて実行しなくてはならない。また、在庫数量が１０個以下の場合については検査をしないことになる。しかし、通常そのような仕様をすべて網羅するドライバは現実的でないため、２回目以降も１回目の境界値を使って検査をしている。
【００１０】
なお、テストデータを生成する技術として、テスト実行中に通過しなかったルートを検出し、ソースプログラムを解析し、当該ルートを通るような入力パラメータ値を生成する技術が知られている。この技術では、プログラムのテスト実行中にコードカバレッジを測定し、テスト実行後、カバレッジ結果を解析して未実行ルートを特定し、その直前の分岐条件から未実行ルートを実行させるための条件を抽出する。その条件と関連するテスト実行中に計測した変数の変移情報から、未実行ルートを通す入力データを特定する。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２０００−３４７９００号公報
【発明の概要】
【発明が解決しようとする課題】
【００１２】
本発明は上記のような実情に鑑みてなされたものであり、モデル検査で用いるテストデータを動的に生成するデータ生成方法、モデル検査装置およびデータ生成プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１３】
実施の態様のひとつであるモデル検査においてテストデータを動的に生成するデータ生成方法（ドライバ）は、モデル検査を実行するコンピュータが、上記モデル検査の検査対象プログラムで用いるデータ項目各々について入力データ項目であるか出力データ項目であるかが定義されている定義テーブルを参照する。そして、上記検査対象プログラムを実行する際に用いる検査条件の記述から入力データ項目と出力データ項目を抽出して、抽出した入力データ項目を生成対象項目として特定する。
【００１４】
次に、上記検査条件の記述から抽出した上記出力データ項目に対応する上記検査対象プログラムの実行環境に記録されているデータを取得して、取得したデータに対応する上記出力データ項目のデータとして用いる形式に変換して出力データを生成する。
【００１５】
次に、上記検査条件と前記出力データを、ＳＭＴソルバプログラムに入力するデータの形式に変換して生成条件を生成する。
次に、上記生成条件を入力してＳＭＴソルバプログラムを実行し、上記記生成条件を満たすデータを求め、該データから上記生成対象項目に対応するデータを抽出し、抽出したデータを前記生成対象項目の入力として検査対象プログラムの実行環境に入力させる。
【発明の効果】
【００１６】
実施の態様によれば、モデル検査で用いるテストデータを動的に生成することにより、検査精度と実行効率を向上させることができるという効果を奏する。
【図面の簡単な説明】
【００１７】
【図１】実施形態１のモデル検査システムの一実施例を示すブロック図である。
【図２】実施形態１のモデル検査システムの動作の一実施例を示すフロー図である。
【図３】検査対象プログラムの取りうる状態遷移の各状態の一実施例を示す状態遷移図である。
【図４】ドライバの一実施例を示すブロック図である。
【図５】入出力装置の画面から商品ＩＤと発注数を入力して在庫数が足りていれば注文を受け付けるプログラムの表示画面、画面項目定義テーブル、ＤＢ項目定義テーブル、商品テーブルの一実施例を示す図である。
【図６】検査条件特定部の動作の一実施例を示すフロー図である。
【図７】検査条件テーブルの一実施例を示す図である。
【図８】検査条件からデータ項目を抽出する動作の一実施例を示す図である。
【図９】第１の生成条件テーブルの一実施例を示す図である。
【図１０】出力データ取得部の動作の一実施例を示すフロー図である。
【図１１】ＤＢ／画面出力データテーブルの一実施例を示す図である。
【図１２】検査条件変換部の動作の一実施例を示すフロー図である。
【図１３】変換ルールテーブルと第２の生成条件テーブルの一実施例を示す図である。
【図１４】第２の生成条件テーブルの一実施例を示す図である。
【図１５】ＳＭＴソルバ実行部の動作の一実施例を示すフロー図である。
【図１６】ＳＭＴソルバ実行部の実行結果の一実施例を示す図である。
【図１７】生成データ通知部の動作の一実施例を示すフロー図である。
【図１８】生成データ通知部の動作の概要の一実施例を示す図である。
【図１９】実施形態２のコンピュータのハードウェア構成の一実施例を示す図である。
【発明を実施するための形態】
【００１８】
以下図面に基づいて、実施形態１について詳細を説明する。
図１は、モデル検査システムの一実施例を示すブロック図である。図１のモデル検査システムは、モデル検査部１、ドライバ２、検査対象プログラム実行環境３、プロパティ４などを有している。モデル検査部１、ドライバ２、検査対象プログラム実行環境３の機能を実現する方法として、Central Processing Unit（ＣＰＵ）を用いることが考えられる。また、プログラマブルなデバイス（Field Programmable Gate Array（ＦＰＧＡ）、Programmable Logic Device（ＰＬＤ）など）を用いることが考えられる。なお、モデル検査部１の機能と、ドライバ２および検査対象プログラム実行環境３の機能を、分けて実現してもよい。また、モデル検査部１、ドライバ２、検査対象プログラム実行環境３、プロパティ４のプログラムやデータなどは、例えばRead Only Memory（ＲＯＭ）、Random Access Memory（ＲＡＭ）などのメモリやハードディスクなどの記録部に記録することが考えられる。また、記録部にはパラメータ値、変数値などのデータを記録してもよいし、実行時のワークエリアとして用いてもよい。なお、モデル検査部１、ドライバ２、検査対象プログラム実行環境３、プロパティ４のプログラムやデータなどは、同一のメモリやハードディスクなどに記録しなくてもよい。
【００１９】
モデル検査部１は、検査対象プログラム実行環境３とドライバ２とプロパティ４を用いてモデル検査を実行し、実行結果がプロパティ４に記録されている後述する機能仕様に記載されている条件が満たされているかを判定する。
【００２０】
ドライバ２は、モデル検査に用いる動的なテストデータを生成する。
検査対象プログラム実行環境３は、該検査対象のシステムの設計書や仕様書などに基づいて検査対象のシステムの振る舞いを専用言語などにより作成した後述する検査対象プログラム５、データベーススタブ６、ネットスタブ７を有している。検査対象プログラム５は、検査対象のシステムの振る舞いを設計書や仕様書などに基づいて作成したプログラムであり、検査対象プログラムを動かすドライバ２とデータベース６やネットワーク７などの外部環境を抽象化するためのスタブなどと接続されている。データベーススタブ６はデータベースの記録内容と動作などを模倣したスタブであり、ネットスタブ７はネットワークと接続された装置と装置とのやり取りなどを模倣したスタブである。
【００２１】
プロパティ４には、仕様書や設計書などに記載された機能仕様が、「Ａ（条件部）ならばＢ（帰結部）」（Ａ−＞Ｂ）の形式で示され、記録されている。仕様書や設計書などに記載されている機能仕様は、例えば、「購入時に入力した購入数量が在庫数量以内ならば購入可能」である。また、「在庫数量−購入数量が１０未満ならば警告を出力」「購入数量に０未満が入力されたならばエラー」「購入数量×単価が１００００円を超えたならば金額オーバー」などである。「購入時に入力した購入数量が在庫数量以内ならば購入可能」に対応する内容であれば、条件部に「在庫数量−購入数量ａｎｄ購入数量＞０」が記録され、帰結部に「メッセージ＝「ｎｕｌｌ」ａｎｄ在庫数量（ａｆｔｅｒ）＝在庫数−購入数量」が記録されている。ここで、ａｎｄは複数の条件を同時に満たす場合を示す記号である。また、帰結部の「メッセージ＝・・・」は、後述する出力部の画面にメッセージや計算結果などを表示する関数である。例えば、メッセージ=「表示内容１」ａｎｄ「表示内容２」と記載すると、「表示内容１」と「表示内容２」が出力部に表示される。また、「在庫数量−購入数量が１０未満ならば警告を出力」に対応する内容であれば、条件部に「０≦在庫数量−購入数量＜１０ａｎｄ購入数量＞０」が記録される。また、帰結部に「メッセージ＝「警告」ａｎｄ在庫数量（ａｆｔｅｒ）＝在庫数量−購入数量」が記録されている。また、「購入数量に０未満ならばエラー」に対応する内容であれば、条件部に「購入数量≦０」が記録され、帰結部に「メッセージ=「購入数量エラー」」が記録されている。また、「購入数量×単価が１００００円を超えたならば金額オーバー」に対応する内容であれば、条件部に「単価×購入数量≧１００００」が記録され、帰結部に「メッセージ＝「金額オーバー」」が記録されている。
なお、上記プロパティ４の記載形式は上記形式に限定されるものではない。
【００２２】
モデル検査システムの動作について説明する。
図２は、モデル検査システムの動作の一実施例を示すフロー図である。ステップＳ１では、モデル検査部１が現在の状態において検査可能な検査条件の選択肢を列挙する。例えば、設計書や仕様書などに基づき作成した検査対象プログラム５の取りうる状態遷移の各状態が、図３に示すような組み合わせである場合について説明する。また、図３の状態１（丸形１）〜状態１０（丸形１０）・・・は状態遷移の各状態を示している。図３の状態１は初期状態を示し、状態１からは状態２、３などに状態遷移する。状態２からは状態４、６、７に状態遷移する。状態３からは状態１０に状態遷移する。状態４からは状態５に状態遷移する。状態７からは状態８、９に状態遷移する。ここで、現在の状態が状態１であれば、状態２、３などの検査条件を列挙する。同じように、現在の状態が状態２であれば状態４、６、７の検査条件を列挙する。検査条件は、プロパティ４に記録されている状態各々に対応する機能仕様の条件部である。また、図３に示した状態各々の遷移については、予め作成して記録部に記録されている。
【００２３】
ステップＳ２では、モデル検査部１が検査条件から１つを特定する。例えば、現在の状態が図３の状態２であれば状態４、６、７の検査条件を列挙されているので、状態４、６、７の検査条件を選択する。選択の方法は、プロパティ４に記録されている検査条件を順に選択する方法が考えられる。しかし、選択の方法は上記に限定されるものではない。
【００２４】
ステップＳ３では、モデル検査部１が特定した検査条件をドライバ２に入力する。そして、ドライバ２は後述する動的なテストデータを生成して、検査対象プログラム実行環境３に該テストデータを入力する。次に、検査対象プログラム実行環境３により実行され、モデル検査部１に実行結果が出力される。
【００２５】
ステップＳ４ではモデル検査部１が実行結果を検査する。例えば、実行結果とプロパティ４の状態各々に対応する機能仕様の帰結部の記載を比較して、実行結果が帰結部の記載内容を満たしていればステップＳ５で合格と判定してステップＳ７（Ｙｅｓ）に移行する。実行結果が帰結部の記載内容を満たしていないときは、ステップＳ５で不合格と判定してステップＳ６（Ｎｏ）に移行する。ステップＳ６で不合格である場合には、モデル検査を停止してもよいし、他の状態に遷移してモデル検査を継続してもよい。
【００２６】
ステップＳ７では、モデル検査部１が合格した後に遷移した現在の状態を検査対象プログラム実行環境３の実行結果を参照して抽出する。例えば、図３の状態４の状態において検査に合格したのであれば、状態５の状態がモデル検査部１により抽出される。
【００２７】
ステップＳ８では、モデル検査部１が既に検査実行済みの状態であるか否かを判定し、検査実行済みの状態であればステップＳ１０（Ｙｅｓ）に移行し、まだ検査が実行されていない状態であればステップＳ９（Ｎｏ）に移行する。例えば、ステップＳ７において図３の状態７の状態において検査に合格し状態８の状態が抽出され場合に、状態８の状態が既に検査実行済みであれば、１つ前の状態である状態７に状態を戻すためにステップＳ１０に移行する。状態８の状態がまだ検査が実行されていないのであれば、状態８より先に検査をする状態があるかを判定するためにステップＳ９に移行する。
【００２８】
ステップＳ９では、モデル検査部１が現在の状態より先に検査をする状態があるか否かを判定し、現在の状態より先に検査をする状態がない場合は終了状態と判定してステップＳ１０（Ｙｅｓ）に移行する。現在の状態より先に検査をする状態がある場合は終了状態でないと判定してステップＳ１（Ｎｏ）に移行する。例えば、図３の状態８の状態が既に検査実行済みであれば、１つ前の状態である状態７に状態を戻し、状態８の状態がまだ検査が実行されていないのであれば、状態８の状態のモデル検査を実行するためにステップＳ１に移行する。
【００２９】
ステップＳ１０では、モデル検査部１が現在の状態を１つ前の状態に戻す。例えば、図３の状態８の状態が既に検査実行済みであれば、１つ前の状態である状態７に状態を戻す。
【００３０】
ステップＳ１１では、モデル検査部１がステップＳ１で列挙した全ての状態の検査条件各々を実行したか否かを判定して、列挙した全ての検査条件を実行した場合にはステップＳ１２（Ｙｅｓ）に移行する。まだ実行していない検査条件がある場合にはステップＳ２（Ｎｏ）に移行する。
【００３１】
ステップＳ１２でモデル検査部１は、現在の条件が初期状態であるか否かを判定して、初期状態であればモデル検査を終了し、初期状態でない場合にはステップＳ１０（Ｎｏ）に移行する。例えば、図３の状態１の初期状態で、かつ全ての状態についてモデル検査が終了していればモデル検査を終了する。また、状態２の場合であればステップＳ１０に移行して１つ前の状態である状態１（初期状態）に状態を戻す。
【００３２】
ドライバ２について説明する。
図４は、ドライバ２の一実施例を示すブロック図である。図４のドライバ２は、検査条件特定部２０１、出力データ取得部２０２、検査条件変換部２０３、Satisability Modulo Theories（ＳＭＴ）ソルバ実行部２０４、生成データ通知部２０５を有している。ドライバ２は、後述する検査条件テーブル２０６、画面項目定義テーブル２０７、ＤＢ項目定義テーブル２０８、変換ルールテーブル２１１を有している。また、第１の生成条件テーブル２０９、ＤＢ／画面出力データテーブル２１０、第２の生成条件テーブル２１２、生成データテーブル２１４を有している。ただし、上記各テーブルはドライバ２以外に記録しておいてもよい。また、ドライバ２は、ＳＭＴソルバ実行部２０４が実行するＳＭＴソルバのプログラムを有している。
【００３３】
検査条件特定部２０１は、定義テーブルを参照して検査対象プログラムを実行する際に用いる検査条件の記述から入力データ項目と出力データ項目を抽出して、該入力データ項目を生成対象項目と特定する。定義テーブルは、モデル検査の検査対象プログラムで用いるデータ項目各々について入力データ項目であるか出力データ項目であるかが定義されているテーブルである。また定義テーブルは、例えば、画面項目定義テーブル２０７、ＤＢ項目定義テーブル２０８などである。図５と図６を用いて、検査条件特定部２０１の説明をする。
【００３４】
図５は、入出力装置の画面から商品ＩＤと発注数を入力して在庫数が足りていれば注文を受け付けるプログラムの表示画面、画面項目定義テーブル、ＤＢ項目定義テーブル、商品テーブルを示す図である。上記プログラムが実行されると、図５に示すような画面５１が表示され、担当者を識別する担当者ＩＤ、画面５１に商品を識別するＩＤを入力する入力範囲５２と、該商品の発注数を入力する入力範囲５３が表示される。また、図５に示す画面５１には、利用者が注文を決定したことを通知する注文ボタン５４が表示される。図５の例では担当者ＩＤとして１０００が記録されている。
【００３５】
上記画面５１から入出力されるデータの定義は、画面項目定義テーブル５５に記録されている。画面項目定義テーブル５５は「画面項目名」「入出力区分」「型」を有している。「画面項目名」には入出力されるデータを識別する識別子が記録され、図５の例では「担当者ＩＤ」「商品ＩＤ」「発注数」が記録されている。「入出力区分」には画面から入力される入力データであるか、画面に表示される出力データであるかを区分けする「入力」「出力」が、「画面項目名」各々に関連付けられて記録されている。「型」には、「画面項目名」各々に関連付けられて入出力されるデータの型が記録されている。型は、例えば、Ｃ言語などで用いられているようなデータの型を定義する型であってもよい。なお、図５の例では、全ての型が整数であることを示す「ｉｎｔ」が記録されている。
【００３６】
図５のＤＢ項目定義テーブル５６は、データベーススタブ６で用いるデータが記録されており、「テーブル名」「ＤＢ項目名」「型」を有している。「テーブル名」にはデータベーススタブ６で用いるテーブルを識別する「テーブル名」が記録されている。図５の例では「商品テーブル」が記録されている。「ＤＢ項目名」にはテーブル各々で用いるデータを識別する識別子が記録され、図５の例では「担当者ＩＤ」「商品ＩＤ」「在庫数」が記録されている。「型」には、「ＤＢ項目名」各々に関連付けられて入出力されるデータの型が記録されている。型は、例えば、Ｃ言語などで用いられているような型であってもよい。なお、図５の例では、全ての型が整数であることを示す「ｉｎｔ」が記録されている。商品テーブル５７は、検査対象プログラム実行環境３のデータベーススタブ６に記録され、「担当者ＩＤ」「商品ＩＤ」「在庫数」を有し、「担当者ＩＤ」には担当者を識別する識別子「１０００」「１０００」「１０１０」「１０２０」が記録されている。「商品ＩＤ」には商品を識別するための識別子「１」「２」「３」「４」が記録されている。「在庫数」には現在の商品の在庫数量を示す「１０」「２００」「１０００」「５０」が記録されている。
【００３７】
検査条件特定部２０１について説明する。
図６は、検査条件特定部２０１の動作の一実施例を示すフロー図である。
ステップＳ６１では、検査条件特定部２０１が検査条件テーブル２０６の検査条件からデータ項目を一つ特定する。例えば、モデル検査部１が図７に示す検査条件テーブル２０６の項番各々に関連付けられている検査条件を用いてモデル検査を実行する。ここで、検査条件テーブル２０６は「項番」「検査条件」を有している。「項番」は、検査条件を識別するための識別子である。本例では、「Ｐ１」「Ｐ２」「Ｐ３」・・・が記録されている。「検査条件」は、既に説明したプロパティ４に記録されている機能仕様の条件部に対応する記述が「項番」に関連付けられて記録されている。本例では、「Ｐ１」に関連付けて「画面．発注数＜＝０」が記録されている。画面５１の入力範囲５３に利用者により入力された発注数が０以下の場合を示している。また、「Ｐ２」に関連付けて「画面．発注数＞０ ａｎｄ （ｎｕｍＯｆ（ｆｉｌｔｅｒ（ｒｅｃ ｉｎ 商品テーブル，ｒｅｃ．担当者ＩＤ＝＝画面．担当者ＩＤ ａｎｄ ｒｅｃ．商品ＩＤ＝＝画面．商品ＩＤ ａｎｄ ｒｅｃ．在庫数＞＝画面．発注数））＝＝１）」が記録されている。ここで、ｒｅｃはテーブル内のあるレコードを表している。上記検査条件は、画面５１の入力範囲５３に利用者により入力された発注数が０より大きく。且つ、商品テーブル内の担当者ＩＤと画面５１上の担当者ＩＤが同じで、商品テーブル内の商品ＩＤと画面５１の入力範囲５２に利用者により入力された商品ＩＤが同じである。さらに、商品テーブル内の在庫数が画面５１の入力範囲５３に利用者により入力された発注数以上の場合を示している。つまり、注文が成功する場合を示している。また、「Ｐ３」に関連付けて「画面．発注数＞０ ａｎｄ （ｎｕｍＯｆ（ｆｉｌｔｅｒ（ｒｅｃ ｉｎ 商品テーブル，ｒｅｃ．担当者ＩＤ＝＝画面．担当者ＩＤ ａｎｄ ｒｅｃ．商品ＩＤ＝＝画面．商品ＩＤ ａｎｄ ｒｅｃ．在庫数＜画面．発注数））＝＝１）」が記録されている。ここで、ｒｅｃはテーブル内のあるレコードを表している。上記検査条件は、画面５１の入力範囲５３に利用者により入力された発注数が０より大きい。且つ、商品テーブル内の担当者ＩＤと画面５１上の担当者ＩＤが同じで、商品テーブル内の商品ＩＤと画面５１の入力範囲５２に利用者により入力された商品ＩＤが同じである。さらに、商品テーブル内の在庫数が画面５１の入力範囲５３に利用者により入力された発注数より少ない場合を示している。つまり、在庫数が足りなり場合を示している。
【００３８】
モデル検査部１が、図７に示す検査条件テーブル２０６の「項番」の「Ｐ２」に関連付けられている検査条件を取得した場合であれば、まずＰ２に対応する検査条件からデータ項目を抽出する。次に、Ｐ２に対応する検査条件は、第１の生成条件テーブル２０９に検査条件として記録される。
【００３９】
次にデータ項目の抽出は、例えば、Ｐ２に対応する検査条件の記載内容から、画面項目定義テーブル５５の「画面項目名」、ＤＢ項目定義テーブル５６の「テーブル名」「ＤＢ項目名」に記載されているデータと一致するデータ項目を抽出する。本例では、図８の８１に示すようにデータ項目「画面．発注数」「商品テーブル．担当者ＩＤ」「画面．担当者ＩＤ」「商品テーブル．商品ＩＤ」「画面．商品ＩＤ」「商品テーブル.在庫数」を抽出する。そして、抽出したデータ項目の中から一つのデータ項目を特定する。
【００４０】
第１の生成条件テーブル２０９は、検査条件の記述から抽出された入力データ項目と出力データ項目を分けて記録する。例えば、図９に第１の生成条件テーブル９１に示すように「検査条件」「画面出力項目」「ＤＢ項目」「生成対象項目」を有している。図９の例では、第１の生成条件テーブル９１の「検査条件」にＰ２に関連付けられた検査条件の内容が記録されている。「画面出力項目」「ＤＢ項目」には出力データ項目が記録され、「生成対象項目」には入力データ項目が記録される。
【００４１】
ステップＳ６２では、検査条件特定部２０１が特定したデータ項目がＤＢ項目か否かを、ＤＢ項目定義テーブル２０８を参照して判定をして、ステップＳ６３においてデータ項目がＤＢ項目である場合にステップＳ６４（Ｙｅｓ）に移行する。ＤＢ項目でない場合にはステップＳ６５（Ｎｏ）に移行する。例えば、商品テーブル５７のデータ項目であればＤＢ項目であるので「商品テーブル．担当者ＩＤ」「商品テーブル．商品ＩＤ」「商品テーブル．在庫数」をＤＢ項目に振り分ける。「画面．」などの記述があるデータ項目であれば、画面項目であると判定する。例えば、「画面．発注数」「画面．担当者ＩＤ」「画面．発注数」を画面項目である。
【００４２】
ステップＳ６４では、検査条件特定部２０１が第１の生成条件テーブル２０９の出力データ項目にＤＢ項目であるデータ項目を記録してステップＳ６９に移行する。例えば、第１の生成条件テーブル９１ではＤＢ項目であるデータ項目を記録する「ＤＢ項目」に、データ項目を記録する。本例では、第１の生成条件テーブル９１の「ＤＢ項目」に「商品テーブル．担当者ＩＤ」「商品テーブル．商品ＩＤ」「商品テーブル．在庫数」が記録されている。
【００４３】
ステップＳ６５では、検査条件特定部２０１が画面項目定義テーブル２０７を参照して振り分けられたデータ項目が画面出力項目か判定する。ステップＳ６６では、検査条件特定部２０１が画面出力項目である場合にステップＳ６７（Ｙｅｓ）に移行し、画面出力項目でない場合にはステップＳ６８（Ｎｏ）に移行する。例えば、図５の画面項目定義テーブル５５の「入出力区分」を参照して、データ項目が「出力」である場合にはステップＳ６７（Ｙｅｓ）に移行する。データ項目が「入力」である場合にはステップＳ６８（Ｎｏ）に移行する。
【００４４】
ステップＳ６７では、検査条件特定部２０１が第１の生成条件テーブル２０９の画面出力項目（出力データ項目）にデータ項目を記録してステップＳ６９に移行する。本例では、図９の第１の生成条件テーブル９１の「画面出力項目」に「画面．担当者ＩＤ」が記録される。
【００４５】
ステップＳ６８では、検査条件特定部２０１が第１の生成条件テーブル２０９の生成対象項目（入力データ項目）にデータ項目を記録する。本例では、図９の第１の生成条件テーブル９１の「生成対象項目」に「画面．発注数」「画面．発注数」が記録される。
【００４６】
ステップＳ６９では、検査条件特定部２０１が全てのデータ項目を処理したか否かを判定し、全てのデータ項目を振り分けていれば出力データ取得部２０２の処理に移行し、まだ振り分けられていないデータ項目がある場合にはステップＳ６１に移行する。
【００４７】
出力データ取得部２０２について説明する。
出力データ取得部２０２は、検査対象プログラムの実行環境に記録されている検査条件の記述から抽出した出力データ項目に対応するデータを取得して、取得したデータを前記出力データ項目で用いることを示す形式に変換することにより出力データを生成する。例えば、第１の生成条件テーブル２０９の画面出力項目、ＤＢ項目などの出力データ項目に記録されているデータ項目に対応するデータを検査対象プログラム実行環境３にアクセスして取得して、ＤＢ／画面出力データテーブル２１０に記録する。
【００４８】
図１０は、出力データ取得部２０２の動作の一実施例を示すフロー図である。
例えば、検査対象プログラム実行環境３に前述した入出力装置の画面から商品ＩＤと発注数を入力して在庫数が足りていれば注文を受け付けるプログラムがある場合について説明する。現在の状態が図９に示す第１の生成条件テーブル９１の状態であるとする。また、図１１に示すように現在の検査対象プログラム実行環境３の画面の状態が画面５１に示す状態で、データベーススタブ６に記録されているテーブルの状態が商品テーブル５７に示す状態であるとする。
【００４９】
ステップＳ１０１では、出力データ取得部２０２が第１の生成条件テーブル９１の「ＤＢ項目」を参照して、データ項目を特定する。次に、ステップＳ１０２で出力データ取得部２０２は、「ＤＢ項目」のデータ項目に関連するデータを、検査対象プログラム実行環境３から取得する。本例では、出力データ取得部２０２は第１の生成条件テーブル９１の「ＤＢ項目」に記録されているデータ項目各々がすべて商品テーブル５７に関連付けられているので、商品テーブル５７に関連するデータを取得する。
【００５０】
ステップＳ１０３では、出力データ取得部２０２が取得したデータを出力データ項目が用いることを示す形式に変換しＤＢ／画面出力データテーブル２１０に記録する。例えば、出力データ取得部２０２が取得したデータが商品テーブル５７の場合であれば、図１１の「ＤＢデータ」に示したデータが記録される。本例では「ＤＢデータ」に、商品テーブル５７の１行目に対応する「商品テーブル［０］．担当者ＩＤ＝１０００，商品テーブル［０］．商品ＩＤ＝１，商品テーブル［０］．在庫数＝１０」が記録されている。また、「ＤＢデータ」に、商品テーブル５７の２行目に対応する「商品テーブル［１］．担当者ＩＤ＝１０００，商品テーブル［１］．商品ＩＤ＝２，商品テーブル［１］．在庫数＝２００」が記録されている。また、「ＤＢデータ」に、商品テーブル５７の３行目に対応する「商品テーブル［２］．担当者ＩＤ＝１０１０，商品テーブル［２］．商品ＩＤ＝３，商品テーブル［２］．在庫数＝１０００」が記録されている。また、「ＤＢデータ」に、商品テーブル５７の４行目に対応する「商品テーブル［３］．担当者ＩＤ＝１０２０，商品テーブル［３］．商品ＩＤ＝４，商品テーブル［３］．在庫数＝５０」が記録されている。
【００５１】
ステップＳ１０４では、出力データ取得部２０２がＤＢ／画面出力データテーブル１１１の行数を表すレコード数に行数を記録する。本例では、商品テーブル５７の行数が４なので、ＤＢ／画面出力データテーブル１１１の「ＤＢレコード数」に「４」が記録される。ただし、「ＤＢレコード数」はなくてもよい。
【００５２】
ステップＳ１０５では、出力データ取得部２０２が第１の生成条件テーブル９１の「画面出力項目」を参照して、データ項目を特定する。次に、ステップＳ１０６で出力データ取得部２０２は、画面出力項目のデータ項目に関連するデータを、検査対象プログラム実行環境３から取得する。例えば、出力データ取得部２０２は第１の生成条件テーブル９１の「画面出力項目」に記録されているデータ項目が画面．担当者ＩＤに関連付けられているので、検査対象プログラム実行環境３の画面．担当者ＩＤに関連するデータを取得する。
【００５３】
ステップＳ１０７では、出力データ取得部２０２が取得したデータを出力データ項目が用いることを示す形式に変換しＤＢ／画面出力データテーブル２１０に記録する。本例では、画面．担当者ＩＤに関連するデータ「画面．担当者ＩＤ＝１０００」が図１１の「画面出力データ」に記録される。
【００５４】
検査条件変換部２０３について説明する。
検査条件変換部２０３は、検査条件と出力データをＳＭＴソルバプログラムへ入力するデータの形式に変換して生成条件を生成する。検査条件変換部２０３は、例えば、検査条件を変換ルールテーブル２１１とＤＢ／画面出力データテーブル２１０を用いて変換する。
【００５５】
図１２は、検査条件変換部２０３の動作の一実施例を示すフロー図である。
ステップＳ１２１では、検査条件変換部２０３がＤＢ／画面出力データテーブル２１０から各テーブルのレコード数を取得する。例えば、図１１のＤＢ／画面出力データテーブル１１１の場合であれば、「ＤＢレコード数」から「４」を取得する。また、「ＤＢレコード数」がない場合には「ＤＢデータ」を用いて行数を求めてもよい。本例では、商品テーブル５７しかないが、データベーススタブ６などで用いるテーブルが複数ある場合にはテーブル各々のレコード数を取得する。
【００５６】
ステップＳ１２２では、検査条件変換部２０３が第１の生成条件テーブル２０９に記録されている検査条件と、変換ルールテーブル２１１の変換前パターン各々を比較して、形式が一致する変換前パターンを特定する。そして、特定した変換前パターンを用いて検査条件に含まれる変数を抽出する。例えば、図９の「検査条件」の記載内容の形式と図１３の変換ルールテーブル１３１に記録されている変換前パターン各々の形式を比較する。図１３の例では、変換ルールテーブル１３１の「変換前パターン」の「ｎｕｍＯｆ（ｆｉｌｔｅｒ（ｒｅｃ ｉｎ ％ＤＢテーブル％，％条件式％））＝＝１」の形式と一致しているので、特定した変換前パターンを用いて検査条件に含まれる変数を抽出する。「変換前パターン」の％で囲われた文字列「％ＤＢテーブル％」「％条件式％」に対応する検査条件の変数「商品テーブル」「ｒｅｃ．担当者ＩＤ＝＝画面．担当者ＩＤ ａｎｄ ｒｅｃ．商品ＩＤ＝＝画面．商品ＩＤ ａｎｄ ｒｅｃ．在庫数＞＝画面．発注数」を抽出する。
【００５７】
ステップＳ１２３では、検査条件変換部２０３が変換ルールテーブル２１１の変換後パターンに、抽出した変数とレコード数を代入して検査条件を変換して、第２の生成条件テーブル２１２に記録する。例えば、図１３の変換ルールテーブル１３１のステップＳ１２２で特定した変換前パターンに関連付けられている変換後パターン「Ｆｏｒ ｉ ＝ ０ ｔｏ ％ＤＢテーブル％．ＤＢレコード数｛％条件式％｝ ｏｒ 接続」を用いて、生成条件を生成する。変換後パターンは、検査条件をＳＭＴソルバの入力データに変換するための関数であり、生成条件はＳＭＴソルバの入力データに用いられるデータである。本例では、図１３の生成条件１３２に示す形式のデータに変換する。「Ｆｏｒ ｉ ＝ ０ ｔｏ ％ＤＢテーブル％．ＤＢレコード数」は、「％ＤＢテーブル％」が示す「商品テーブル」の各レコードを示す［０］〜［３］を示している。また、「％条件式％」は商品テーブルのレコードが［０］のとき「商品テーブル［０］．担当者ＩＤ ＝＝ 画面．担当者ＩＤ ａｎｄ 商品テーブル［０］．商品ＩＤ ＝＝ 画面．商品ＩＤ ａｎｄ 商品テーブル［０］．在庫数＞＝画面．発注数」になる。また、商品テーブルのレコードが［１］のとき「商品テーブル［１］．担当者ＩＤ ＝＝ 画面．担当者ＩＤ ａｎｄ 商品テーブル［１］．商品ＩＤ ＝＝ 画面．商品ＩＤ ａｎｄ 商品テーブル［１］．在庫数＞＝画面．発注数」になる。また、商品テーブルのレコードが［２］のとき「商品テーブル［２］．担当者ＩＤ ＝＝ 画面．担当者ＩＤ ａｎｄ 商品テーブル［２］．商品ＩＤ ＝＝ 画面．商品ＩＤ ａｎｄ 商品テーブル［２］．在庫数＞＝画面．発注数」になる。また、商品テーブルのレコードが［３］のとき「商品テーブル［３］．担当者ＩＤ ＝＝ 画面．担当者ＩＤ ａｎｄ 商品テーブル［３］．商品ＩＤ ＝＝ 画面．商品ＩＤ ａｎｄ 商品テーブル［３］．在庫数＞＝画面．発注数」になる。そして、「ｏｒ 接続」は上記４つの「％条件式％」に対応する記述を論理和「ｏｒ」で結合することを示している。ただし、本例の変換後パターンの関数は実際に用いるＳＭＴソルバの入力データの形式に変換できる関数であればよく、上記変換後パターンに限定されるものではない。
【００５８】
ステップＳ１２４では、検査条件変換部２０３が検査条件に対して全て変換処理をしたかを判定して、全ての変換処理をした場合にはステップＳ１２５（Ｙｅｓ）に移行し、すべての変換処理をしていない場合にはステップＳ１２２（Ｎｏ）に移行する。例えば、検査条件が複数の変換前パターンの形式を有している場合に、全ての変換前パターンに対して変換処理をしたか否かを判定する。
【００５９】
ステップＳ１２５では、検査条件変換部２０３がＤＢ／画面出力データテーブル２１０の画面出力データを取得して条件式に変換して、第２の生成条件テーブル２１２に記録する。例えば、図１１のＤＢ／画面出力データテーブル１１１から「画面出力データ」に記録されている「画面．担当者＝１０００」を取得して、図１４に示すように「ａｎｄ 画面．担当者＝１０００」に変換して、変換後生成条件に追加して記録する。ただし、本例の変換は実際に用いるＳＭＴソルバの入力データの形式に変換できる関数であればよく、上記変換に限定されるものではない。
【００６０】
ステップＳ１２６では、検査条件変換部２０３がＤＢ／画面出力データテーブル２１０のＤＢデータを取得して条件式に変換、第２の生成条件テーブル２１２に記録する。例えば、図１１のＤＢ／画面出力データテーブル１１１から「ＤＢデータ」に記録されているデータを取得して、図１４に示すように「ａｎｄ 商品テーブル［０］．担当者ＩＤ＝１０００ ａｎｄ 商品テーブル［０］．商品ＩＤ＝１ ａｎｄ 商品テーブル［０］．在庫数=１０ ａｎｄ ・・・・」に変換して、変換後生成条件に追加して記録する。ただし、本例の変換は実際に用いるＳＭＴソルバの入力データの形式に変換できる関数であればよく、上記変換に限定されるものではない。
【００６１】
ＳＭＴソルバ実行部２０４について説明する。
ＳＭＴソルバ実行部２０４は、検査条件変換部２０３で生成した第２の生成条件テーブル２１２に記録した生成条件を入力としてＳＭＴソルバプログラム２１３を実行して、生成条件を満たすデータを得る。次に、ＳＭＴソルバ実行部２０４は、第１の生成条件テーブル２０９の生成対象項目から画面入力データを抽出し、生成データテーブル２１４に記録する。ＳＭＴソルバとは、ＤＰＬＬ（Ｔ）アルゴリズム（「Decision Procedures: An Algorithmic Point of View」、Daniel Kroening他、ISBN:978-3540741046の１１章参照）等を用いて入力された制約の充足可能性を判定するものである。ここで、ＤＰＬＬ（Ｔ）とは、命題論理用の充足可能性判定アルゴリズムであるＤＰＬＬアルゴリズムを述語論理に拡張したものである。ＤＰＬＬは、Davis-Putnam-Logemann-Lovelandを示し、Ｔは理論（Theory）の略で、理論とは述語論理のサブセットを指す。例えば、「ｘ＝ｙかつｙ＝１かつｘ！＝２」といった自然数の等価関係（＝）のみから構成される論理式のクラスは理論の一つである。また、ＳＭＴソルバでは、まず入力された制約の論理的な最小単位である原子論理式に対応する命題論理式を新たに与える。続いて、当該制約の各原子論理式を対応する命題論理式で変換した論理式が充足可能であるように、ＳＭＴソルバは各命題論理式に対して真偽値を与えていく。そして、原子論理式の真偽値が対応する各命題論理式の真偽値と一致するように、当該原子論理式に出現するインスタンス（変数）の具体的な充足値を得ようと試みる。実際に各インスタンスの具体的な充足値を得ることができた場合、ＳＭＴソルバは入力された制約を充足可能と判定し、得た充足値を充足解として出力する。充足値を得ることができなかった場合、ＳＭＴソルバは入力された制約を充足不能と判定する。この処理により、ＳＭＴソルバは変換後制約を入力として受け取り、変換後制約充足解を出力する。
【００６２】
図１５は、ＳＭＴソルバ実行部２０４の動作の一実施例を示すフロー図である。
ステップＳ１５１では、ＳＭＴソルバ実行部２０４が第２の生成条件テーブル２１２の生成条件を取得して実行する。そして、ＳＭＴソルバ実行部２０４は実行結果を取得する。例えば、ＳＭＴソルバ実行部２０４は、生成条件１４１を入力してＳＭＴソルバプログラム２１３を実行して、実行結果を取得する。図１６の実行結果１６１にＳＭＴソルバプログラムの実行結果の一実施例を示す。
【００６３】
ステップＳ１５２では、ＳＭＴソルバ実行部２０４が第１の生成条件テーブル２０９に記録されている生成対象項目のデータ項目を取得する。例えば、第１の生成条件テーブル９１のデータ項目「画面．発注数」「画面．商品ＩＤ」を取得する。図１６に生成対象項目１６２を示す。
【００６４】
ステップＳ１５３では、ＳＭＴソルバ実行部２０４が実行結果から生成対象項目で用いる生成データを抽出して、生成データテーブル２１４に記録する。例えば、図１６に実行結果１６１の「画面．発注数=１０」「画面．商品ＩＤ＝１」を抽出して生成データテーブル１６３に記録する。
【００６５】
生成データ通知部２０５について説明する。
生成データ通知部２０５は、生成データテーブル２１４の生成データを用いて検査対象プログラムを実行するために、生成データテーブル２１４の生成データを検査対象プログラム実行環境３に入力する。
【００６６】
図１７は、生成データ通知部２０５の動作の一実施例を示すフロー図である。
ステップＳ１７１では、生成データ通知部２０５が生成データテーブル２１４から生成データを取得する。次に、ステップＳ１７２で生成データ通知部２０５は、生成データをテストデータとして検査対象プログラムに入力する。図１８の場合であれば、生成データテーブル１６３の生成データである画面.発注数＝１０、画面.商品ＩＤ＝１を、テストデータとして検査対象プログラムへ入力する。その後、モデル検査部１は、現在の検査対象プログラムの実行をし、実行が終了するとモデル検査完了か否かの判定を行い、モデル検査を続行する場合、次の検査条件の特定を行う。
【００６７】
実施形態１のドライバによれば、生成対象項目に含まれる複数のデータ項目で用いる値によりテストデータを決定する必要がある場合に、変換後生成条件を満たす生成データを作成してテストデータとして検査対象プログラム実行環境に入力する。すなわち、動的にテストデータを検査対象プログラム実行環境に入力することができるため、従来のように無駄なテストデータを検査対象プログラム実行環境に入力して実行することを抑制できるので、モデル検査の実行効率を向上させることができる。また、動的にテストデータを生成するため、従来検査できなかった検査条件についても検査をすることができるため、モデル検査の精度を向上させることができる。また、検査対象プログラムに入力するテストデータが、検査対象プログラムの動作結果に依存して決定されるため、検査対象プログラムを動作させる前に具体的な値が決定できる。また、検査できなかった検査条件が検知された場合には、従来のようにその検査条件に対するドライバを生成してコンパイルし直す必要がないため、モデル検査を実施する準備作業を削減できる。
【００６８】
実施形態２について説明する。
実施形態２は、実施形態１を、コンピュータを用いて実現する場合について説明する。
図１９は、実施形態２のコンピュータのハードウェア構成の一実施例を示す図である。コンピュータのハードウェア１９００は、ＣＰＵ１９０１、記録部１９０２、記録媒体読取装置１９０３、入出力インタフェース１９０４（入出力Ｉ／Ｆ）、通信インタフェース１９０５（通信Ｉ／Ｆ）などを備えている。また、上記各構成部はバス１９０６によってそれぞれ接続されている。
【００６９】
ＣＰＵ１９０１は、記録部１９０２に記録されている上記説明した各処理を実行する。
記録部１９０２には、ＣＰＵ１９０１が実行するプログラムやデータが記録されている。また、ワークエリアなどとして使用される。例えば、ＲＯＭ、ＲＡＭ、ハードディスクドライブなどである。
【００７０】
記録媒体読取装置１９０３は、ＣＰＵ１９０１の制御に従って記録媒体１９０７に対するデータのリード／ライトを制御する。そして、記録媒体１９０７に記録媒体読取装置１９０３の制御で書き込まれたデータを記録させたり、記録媒体１９０７に記憶されたデータを読み取らせたりする。また、着脱可能な記録媒体１９０７は、コンピュータで読み取り可能なｎｏｎ−ｔｒａｎｓｉｔｏｒｙ（非一時的）な記録媒体として、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記録装置には、ハードディスク装置（ＨＤＤ）などがある。光ディスクには、Digital Versatile Disc（ＤＶＤ）、ＤＶＤ−ＲＡＭ、Compact Disc Read Only Memory（ＣＤ−ＲＯＭ）、ＣＤ−Ｒ(Recordable)／ＲＷ（ReWritable）などがある。光磁気記録媒体には、Magneto-Optical disk（ＭＯ）などがある。なお、記録部１９０２もnon-transitory（非一時的）な記録媒体に含まれる。
【００７１】
入出力インタフェース１９０４には、入出力装置１９０８が接続され、利用者が入力した情報を受信し、バス１９０６を介してＣＰＵ１９０１に送信する。また、ＣＰＵ１９０１からの命令に従ってディスプレイの画面上に操作情報などを表示する。入出力装置１９０８は、例えば、タッチパネルなどが考えられる。
【００７２】
通信インタフェース１９０５は、必要に応じ、他のコンピュータとの間のLocal Area Network（ＬＡＮ）接続やインターネット接続や無線接続を行うためのインタフェースである。また、他の装置に接続され、外部装置からのデータの入出力を制御する。
【００７３】
このようなハードウェア構成を有するコンピュータを用いることによって、上記説明した各種処理機能が実現される。その場合システムが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体１９０７に記録しておくことができる。なお、上記各種処理機能は、実施形態１で説明したフロー図などである。
【００７４】
プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭなどの記録媒体１９０７が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【００７５】
プログラムを実行するコンピュータは、例えば、記録媒体１９０７に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記録部１９０２に格納する。そして、コンピュータは、自己の記録部１９０２からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、記録媒体１９０７から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。
【００７６】
また、本発明は、上記実施の形態に限定されるものでなく、本発明の要旨を逸脱しない範囲内で種々の改良、変更が可能である。なお、各実施例は処理に矛盾の無い限りにおいて、互いに組み合わせても構わない。
【符号の説明】
【００７７】
１  モデル検査部
２  ドライバ
３  検査対象プログラム実行環境
４  プロパティ
５  検査対象プログラム
６  データベーススタブ
７  ネットスタブ
２０１  検査条件特定部
２０２  出力データ取得部
２０３  検査条件変換部
２０４  ＳＭＴソルバ実行部
２０５  生成データ通知部
２０６  検査条件テーブル
２０７、５５  画面項目定義テーブル
２０８、５６  ＤＢ項目定義テーブル
２０９、９１  第１の生成条件テーブル
２１０、１１１  ＤＢ／画面出力データテーブル
２１１、１３１  変換ルールテーブル
２１２、１３２、１４１  第２の生成条件テーブル
２１３  ＳＭＴソルバプログラム
２１４、１６３  生成データテーブル
５１  画面
５２、５３  入力範囲
５４  注文ボタン
５７  商品テーブル
１６１  実行結果
１６２  生成対象項目
１９００  ハードウェア
１９０１  ＣＰＵ
１９０２  記録部
１９０３  記録媒体読取装置
１９０４  入出力インタフェース（入出力Ｉ／Ｆ）
１９０５  通信インタフェース（通信Ｉ／Ｆ）
１９０６  バス
１９０７  記録媒体
１９０８  入出力装置
【図１】
0005471971.tif 000002
【図２】
0005471971.tif 000003
【図３】
0005471971.tif 000004
【図４】
0005471971.tif 000005
【図５】
0005471971.tif 000006
【図６】
0005471971.tif 000007
【図７】
0005471971.tif 000008
【図８】
0005471971.tif 000009
【図９】
0005471971.tif 000010
【図１０】
0005471971.tif 000011
【図１１】
0005471971.tif 000012
【図１２】
0005471971.tif 000013
【図１３】
0005471971.tif 000014
【図１４】
0005471971.tif 000015
【図１５】
0005471971.tif 000016
【図１６】
0005471971.tif 000017
【図１７】
0005471971.tif 000018
【図１８】
0005471971.tif 000019
【図１９】
0005471971.tif 000020