(57)【特許請求の範囲】
【請求項１】
プログラムの動作確認のためのテストデータを生成するデータ生成方法において，
コンピュータが，
検査対象となるプログラムで実行される画面間の遷移を示す画面遷移情報，各画面が備える項目を示す画面項目情報，および，前記プログラムが満たすべき仕様を示すプロパティを読み込む画面情報設定処理ステップと，
前記プロパティが，前記画面遷移情報に示される画面遷移上のどの画面遷移の仕様に該当するか判定し，該当すると判定されたプロパティを画面遷移に関連付けるプロパティ配置処理ステップと，
前記画面遷移に関連付けられたプロパティについて，該プロパティの事前条件が，前記プログラムの画面遷移上の直近イベントでの入力項目に起因するかを判定し，該事前条件が前記直近イベントでの入力項目に起因する場合に，判定を真とする入力判定処理ステップと，
前記プロパティの事前条件が直近イベントでの入力項目ではない場合に，前記プログラムの画面遷移を遡りながらプロパティを取得し，該取得したプロパティに対する入力項目の判定が真となるまでプロパティの収集を繰り返し，取得したプロパティ群を依存プロパティとして抽出するプロパティ収集処理ステップと，
前記依存プロパティの事前条件および事後条件ならびに連結条件を用いて，データ生成のための制約条件を生成するデータ制約生成処理ステップとを
実行することを特徴とするデータ生成方法。
【請求項２】
前記コンピュータが，さらに，
前記画面遷移情報，画面項目情報および前記プロパティをもとに，前記依存プロパティにおいて入力判定を真とするために不足しているプロパティを特定し，補完するプロパティ補完処理ステップを，
実行することを特徴とする請求項１に記載のデータ生成方法。
【請求項３】
前記コンピュータが，さらに，
前記依存プロパティに含まれる重複部分またはデータ推移と無関係なプロパティを除外するプロパティ整理処理ステップを，
実行することを特徴とする請求項１または請求項２に記載のデータ生成方法。
【請求項４】
プログラムの動作確認のためのテストデータを生成するデータ生成処理であって，
コンピュータに，
検査対象となるプログラムで実行される画面間の遷移を示す画面遷移情報，各画面が備える項目を示す画面項目情報，および，前記プログラムが満たすべき仕様を示すプロパティを読み込む画面情報設定処理と，
前記プロパティが，前記画面遷移情報に示される画面遷移上のどの画面遷移の仕様に該当するか判定し，該当すると判定されたプロパティを画面遷移に関連付けるプロパティ配置処理と，
前記画面遷移に関連付けられたプロパティについて，該プロパティの事前条件が，前記プログラムの画面遷移上の直近イベントでの入力項目に起因するかを判定し，該事前条件が前記直近イベントでの入力項目に起因する場合に，判定を真とする入力判定処理と，
前記プロパティの事前条件が直近イベントでの入力項目ではない場合に，前記プログラムの画面遷移を遡りながらプロパティを取得し，該取得したプロパティに対する入力項目の判定が真となるまでプロパティの収集を繰り返し，取得したプロパティ群を依存プロパティとして抽出するプロパティ収集処理と，
前記依存プロパティの事前条件および事後条件ならびに連結条件を用いて，データ生成のための制約条件を生成するデータ制約生成処理とを
実行させるためのデータ生成プログラム。
【請求項５】
プログラムの動作確認のためのテストデータを生成するデータ生成装置において，
検査対象となるプログラムで実行される画面間の遷移を示す画面遷移情報，各画面が備える項目を示す画面項目情報，および，前記プログラムが満たすべき仕様を示すプロパティを読み込む画面情報設定部と，
前記読み込まれた画面遷移情報，画面項目情報およびプロパティを記憶する記憶部と，
前記プロパティが，前記画面遷移情報に示される画面遷移上のどの画面遷移の仕様に該当するか判定し，該当すると判定されたプロパティを画面遷移に関連付けるプロパティ配置部と，
前記画面遷移に関連付けられたプロパティについて，該プロパティの事前条件が，前記プログラムの画面遷移上の直近イベントでの入力項目に起因するかを判定し，該事前条件が前記直近イベントでの入力項目に起因する場合に，判定を真とする入力判定部と，
前記プロパティの事前条件が直近イベントでの入力項目ではない場合に，前記プログラムの画面遷移を遡りながらプロパティを取得し，該取得したプロパティに対する入力項目の判定が真となるまでプロパティの収集を繰り返し，取得したプロパティ群を依存プロパティとして抽出するプロパティ収集部と，
前記依存プロパティの事前条件および事後条件ならびに連結条件を用いて，データ生成のための制約条件を生成するデータ制約生成部とを
備えることを特徴とするデータ生成装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は，ソフトウェアの動作確認テストに関連し，特に，システム仕様を表現したモデルが，システムに要求されるプロパティを満たすか否かを検査するモデル検査において使用されるテストデータを生成する技術に関する。
【背景技術】
【０００２】
ソフトウェアのモデル検査とは，モデルに該当するプログラムが仕様として満たすべき性質（プロパティと呼ぶ）を満足するか否かを，該プログラムを網羅的に実行し，実行時のプログラム状態においてプロパティが成立するかをチェックすることによって検査する手法である。
【０００３】
ここで，モデルとは，開発するシステムの挙動や処理内容の記述であり，記述の詳細度レベルによって種々のモデルがある。例えば，概要設計のレベルでは，ＵＭＬ（Ｕｎｉｆｉｅｄ  Ｍｏｄｅｌｉｎｇ  Ｌａｎｇｕａｇｅ）を用いて，システムが処理する情報の静的構造や処理シーケンスを記述したモデルが利用される。また，開発仕様を厳密に記述する場合には，仕様記述言語を用いて開発仕様をモデルとして記述することも行われている。さらに，開発システムの動的な側面をモデル化する場合には，例えば，Ｐｒｏｍｅｌａ等のモデル記述用の専用言語を用いて状態遷移等を記述することも行われている。Ｐｒｏｍｅｌａで記述されたモデルに対しては，ＳＰＩＮモデルチェッカというツールを用いてモデル検査を実行することができる。
【０００４】
Ｊａｖａ（登録商標）等の実行可能なプログラム言語を用いて記述されたプログラムも，最も記述が詳細なモデルであると見なされる。プログラムをモデルとするモデル検査は，特に，プログラムモデル検査と呼ばれるが，ここでは，以後単にモデル検査と表記する。Ｊａｖａで記述されたプログラムに対するモデル検査ツールには，例えば，ＪＰＦ（Ｊａｖａ  Ｐａｔｈ  Ｆｉｎｄｅｒ）がある。本出願で扱うモデルは，特にＷｅｂアプリケーションのサーバ側の業務ロジックを記述したものである。
【０００５】
一般に，Ｗｅｂアプリケーション・プログラムに対するモデル検査では，観測するプログラム状態として，ブラウザ等に表示される画面状態とサーバ側のデータベースの状態すなわちデータベースに格納されているデータ値とが用いられる。
【０００６】
モデル検査の処理の手順は，まず，検査対象のプログラムに対して画面とデータベースの初期状態を設定し，次いで，ドライバを用いて，プログラムに対して次々にイベントを起こすことによって検査対象プログラムを駆動する。このとき，ドライバは，検査対象プログラムが種々の状態になりうるように，イベントや入力データを網羅的に選択する。そして，イベントを駆動する中で，プログラム状態がプロパティを満たしているかどうかを検査することによって，プロパティ違反（バグ）が発生していないことを確認する。
【０００７】
ここで，イベントとは，画面上の項目にデータを入力してボタンを押下する等のユーザ操作である。また，プロパティは，モデル（プログラム）が満たすべきロジックの性質を記述したものである。具体的には，検査対象のイベントおよび評価対象のイベントに関する事前条件と事後条件を含んだ構成を持ち，事前条件と事後条件は一階述語論理や時相論理等を用いた論理式で記述され，コンピュータ等によって処理可能である。
【０００８】
モデル検査におけるプロパティ検査は，検査対象に対するイベントについて，イベント駆動前のプログラム状態において事前条件が「真」であるとき，イベント駆動後のプログラム状態において事後条件が「真」であることを確認することである。つまり，事前条件が真であると評価されなければ事後条件は評価されず，プログラムの実行中に，事前条件が一度も真とならなかったプロパティは，一度も検査されないことになる。それゆえ，全てのプロパティの事前条件が少なくとも一度は真となるような状態に，ドライバとプログラム初期状態を調整する必要がある。
【０００９】
特に，Ｗｅｂアプリケーションに対するモデル検査では，画面データはドライバに設定され，データベース・データ（ＤＢデータ）はプログラム初期状態として設定される。そのため，プロパティ自体，および，ＤＢデータに関する共通制約を利用して，その事前条件に記述されている制約を真とするような画面データとＤＢデータを生成するという技術が従来から存在する。
【００１０】
また，近年，コンピュータの性能が飛躍的に向上していることを背景として，ＳＡＴ（ＳＡＴｉｓｆｉａｂｉｌｉｔｙ  ｐｒｏｂｌｅｍ）やＳＭＴ（Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｍｏｄｕｌｏ  Ｔｈｅｏｒｉｅｓ）といった論理式の充足可能性問題を解くツール（ソルバ）を利用してプロパティの事前条件の充足解を求めることが検討されている。
【００１１】
なお，本発明者は，ＳＡＴ，ＳＭＴ等の技術を利用して，画面データとＤＢデータを生成する技術を検討している。プロパティの事前条件からデータの満たすべき制約条件を構築し，ＳＭＴソルバを用いてデータ制約条件を満たす具体的なデータ値を生成するものである。ＳＭＴソルバが論理式の充足可能性問題を解くとは，例えば，論理式を入力してデータが満たすべき条件範囲を出力することである。
【先行技術文献】
【特許文献】
【００１２】
【特許文献１】特開２００９−８７３５４号公報
【特許文献２】特開２０１０−１０２６５０号公報
【発明の概要】
【発明が解決しようとする課題】
【００１３】
しかしながら，従来技術では，各々のプロパティの事前条件をデータの制約条件とする充足可能性問題として個別に解き，事前条件を成立させるようなデータを生成させている。すなわち，従来技術では，依存関係，因果関係等のプロパティの前後関係を考慮して，データを生成することができなかった。
【００１４】
そのため，検査対象プログラムの実行経路上において，プロパティが前後関係を持って設定されている場合に，従来技術を用いて生成されたデータを検査対象プログラムに入力して駆動しても，実行経路において後に該当するプロパティの事前条件が真になるとは限らないという問題があった。プロパティの事前条件が真にならなければ，検査対象プログラムが，該プロパティを満たすかどうかを評価したことにならないため，従来技術で生成されたデータは不十分であった。
【００１５】
上述の従来技術の課題への対応として，プロパティの前後関係を単純に考慮しようとしても，以下の理由により困難であった。
【００１６】
（１）  プロパティの前後関係は，プロパティの記述のみからは決定することができない。
【００１７】
（２）  プロパティの記述のみからは，プロパティの事前条件を構成する項目のうち，どの項目が当該イベントで入力されるデータであるのかを判定することができない。
【００１８】
本発明は，上記課題に鑑みてなされたものであり，その目的とするところは，検査対象プログラムの実行経路上において，プロパティが前後関係を持って設定されている場合に，該プロパティの事前条件が真となるようなデータを生成することができる技術を提供することである。
【課題を解決するための手段】
【００１９】
本発明の一態様として開示されるデータ生成方法は，プログラムの動作確認のためのテストデータを生成する方法において，コンピュータが，１）検査対象となるプログラムで実行される画面間の遷移を示す画面遷移情報，各画面が備える項目を示す画面項目情報，および，前記プログラムが満たすべき仕様を示すプロパティを読み込む画面情報設定処理ステップと，２）前記プロパティが，前記画面遷移情報に示される画面遷移上のどの画面遷移の仕様に該当するか判定し，該当すると判定されたプロパティを画面遷移に関連付けるプロパティ配置処理ステップと，３）前記画面遷移に関連付けられたプロパティについて，該プロパティの事前条件が，前記プログラムの画面遷移上の直近イベントでの入力項目に起因するかを判定し，該事前条件が前記直近イベントでの入力項目に起因する場合に，判定を真とする入力判定処理ステップと，４）前記プロパティの事前条件が直近イベントでの入力項目ではない場合に，前記プログラムの画面遷移を遡りながらプロパティを取得し，該取得したプロパティに対する入力項目の判定が真となるまでプロパティの収集を繰り返し，取得したプロパティ群を依存プロパティとして抽出するプロパティ収集処理ステップと，５）前記依存プロパティの事前条件および事後条件ならびに連結条件を用いて，データ生成のための制約条件を生成するデータ制約生成処理ステップとを実行するものである。
【００２０】
また，本発明の別の一態様として開示されるデータ生成プログラムは，コンピュータに，上記の処理方法で実現される各処理を実行させるためのものである。
【００２１】
また，本発明の別の一態様として開示されるデータ生成装置は，上記の処理方法で実現される処理を実行する各処理部を備えるものである。
【発明の効果】
【００２２】
本発明の一態様として開示したデータ生成装置は，検査対象プログラムの実行経路上において，プロパティが前後関係を持って設定されている場合に，該プロパティの事前条件が真となるようなデータを生成することができ，モデル検査のためのデータ生成処理の手間を軽減させることができる。
【図面の簡単な説明】
【００２３】
【図１】本発明の実施形態におけるモデル検査装置の全体の一例を示す図である。
【図２】本発明の実施形態におけるデータ生成装置のブロック構成例を示す図である。
【図３】本発明の実施形態における検査対象のＷｅｂアプリケーションでの画面遷移の例を示す図である。
【図４】表示項目（会員種別）の値により異なる画面遷移が生じる場合の例を示す図である。
【図５】本発明の実施形態におけるデータベース情報の例を示す図である。
【図６】本発明の実施形態におけるプロパティの例を示す図である。
【図７】本発明の実施形態における画面遷移情報の例を示す図である。
【図８】本発明の実施形態における画面項目情報の例を示す図である。
【図９】本発明の実施形態におけるデータ制約生成部の処理フロー例を示す図である。
【図１０】プロパティ配置処理（ステップＳ２）のより詳細な処理フロー例を示す図である。
【図１１】本発明の実施形態におけるプロパティ配置部によってプロパティから抽出される情報をテーブルとして示す図である。
【図１２】本発明の実施形態におけるプロパティ配置部で生成される結果テーブルの例を示す図である。
【図１３】プロパティ配置部の処理結果を，画面遷移上に対応付けて示す図である。
【図１４】プロパティの入力判定処理（ステップＳ３）のより詳細な処理フロー例を示す図である。
【図１５】本発明の実施形態における入力判定部の処理結果例を示す図である。
【図１６】入力判定部の処理結果を，画面遷移に対応付けて示す図である。
【図１７】プロパティ遡及取得処理（ステップＳ４）および依存プロパティ抽出処理（ステップＳ５）のより詳細な処理フロー例を示す図である。
【図１８】本発明の実施形態における依存プロパティ収集部の作業テーブルの例を示す図である。
【図１９】本発明の実施形態における依存プロパティ収集部の出力結果である依存プロパティで・リストの例を示す図である。
【図２０】依存プロパティ収集部の処理結果を，画面遷移に対応付けて示す図である。
【図２１】プロパティ整理処理（ステップＳ７）のより詳細な処理フロー例を示す図である。
【図２２】本発明の実施形態における依存プロパティ整理部の処理結果の例を示す図である。
【図２３】制約条件生成処理（ステップＳ８）のより詳細な処理フロー例を示す図である。
【図２４】データ制約生成部の処理結果の例を示す図である。
【図２５】入力判定が真とならないプロパティの例を示す図である。
【図２６】入力判定が真とならないプロパティの例を示す図である。
【図２７】プロパティ補完処理（ステップＳ６）のより詳細な処理フロー例を示す図である。
【図２８】本発明の実施形態におけるプロパティ補完部の処理結果の例を示す図である。
【発明を実施するための形態】
【００２４】
以下，本発明の一態様として開示されるデータ生成装置を，画面とデータベース（ＤＢ）を利用するプログラムを検査対象としてモデル検査を実施する際に，使用されるテストデータを生成する実施例をもとに説明する。
【００２５】
図１は，データ生成とモデル検査を実行するモデル検査装置の全体の一例を示す図である。
【００２６】
図１に示すモデル検査装置１は，データ生成装置３と検査実行装置５とを備え，入出力装置（図示しない）と接続されている。データ生成装置３が，本発明の一態様として開示される装置である。
【００２７】
データ生成装置３および検査実行装置５は，それぞれ，制御部１０および記憶部２０を備え，入出力装置に接続されている。
【００２８】
モデル検査装置１では，入出力装置から入力および操作によって，データ生成装置３が，モデル検査のためのテストデータ２５を生成し，検査実行装置５が，データ生成装置３で生成されたテストデータ２５を使用して検査対象プログラム２７のモデル検査を実行する。
【００２９】
モデル検査装置１は，コンピュータまたは専用のハードウェアによって実現される。
【００３０】
制御部１０は，データ生成装置３，検査実行装置５以外に，図１には示されていない，入出力装置，外部記録装置などの周辺機器との情報のやり取りを制御する。制御部１０の実現には，ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）やプログラマブルなデバイス（ＦＰＧＡ（Ｆｉｅｌｄ  Ｐｒｏｇｒａｍｍａｂｌｅ  Ｇａｔｅ  Ａｒｒａｙ），ＰＬＤ（Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  Ｄｅｖｉｃｅ）など）を用いることができる。データ生成装置３および検査実行装置５は，ソフトウェア（コンピュータプログラム）としてコンピュータに実装され，実行されるものであってもよい。また，このソフトウェアは，コンピュータで読み取り可能な記録媒体に記録しておくことができる。
【００３１】
記憶部２０は，データ生成装置３および検査実行装置５が使用するデータを記憶する。記憶部２０は，例えばＲＯＭ（Ｒｅａｄ  Ｏｎｌｙ  Ｍｅｍｏｒｙ），ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ），ハードディスクなどのメモリである。記憶部２０は，入出力装置から入力される入力データ，ドライバ，データベーススタブ，ネットワークスタブなどが格納されている。また，記憶部２０は，パラメータ値，変数値などのデータを記録してもよく，ワークエリアとして用いることもできる。
【００３２】
データ生成装置３の記憶部として，記憶部２０は，プロパティ２１，データベース（ＤＢ）情報２２，画面遷移情報２３，および画面項目情報２４を記憶する。
【００３３】
データ生成装置３の処理手段として，制御部１０は，データ制約生成部３１およびデータ生成部３３を有する。
【００３４】
データ制約生成部３１は，記憶部２０に記憶されたプロパティ２１，ＤＢ情報２２，画面遷移情報２３，および画面項目情報２４を用いて，テストデータ２５の生成における制約条件となるデータ制約を生成する。
【００３５】
データ生成部３３は，データ制約生成部３１が生成したデータ制約を満たすテストデータ２５を生成する。
【００３６】
検査実行装置５の記憶部として，記憶部２０は，テストデータ２５，検査対象プログラム２７を記憶する。
【００３７】
検査実行装置５の処理手段として，制御部１０は，ドライバ５１および検査実行部５３を有する。
【００３８】
ドライバ５１は，テストデータ２５を使用して，モデルである検査対象プログラム２７に対するイベントを発生させる。
【００３９】
検査実行部５３は，ドライバ５１によって検査対象プログラム２７を駆動してプログラム状態を遷移させ，遷移したプログラム状態においてプロパティ２１が成立するかどうかを調査する。
【００４０】
なお，図１では，データ生成装置３および検査実行装置５を備えるモデル検査装置１が１つの物理的装置として実施される場合の構成例を示すが，データ生成装置３および検査実行装置５が，それぞれ別個の装置として構成されるようにしてもよい。
【００４１】
図２は，データ生成装置３のブロック構成例を示す図である。
【００４２】
データ生成装置３のデータ制約生成部３１は，画面情報設定部３１１，プロパティ配置部３１２，入力判定部３１３，依存プロパティ収集部３１４，プロパティ補完部３１５，依存プロパティ整理部３１６，および制約生成部３１７を備える。
【００４３】
画面情報設定部３１１は，検査対象プログラム２７の画面遷移情報２３と画面項目情報２４とを取得して設定する。
【００４４】
プロパティ配置部３１２は，プロパティ２１を取得し，プロパティ２１各々が画面遷移上のどの遷移の仕様に該当するか判定し，該当する画面遷移に配置する。
【００４５】
入力判定部３１３は，画面遷移上に配置されたプロパティ２１を順に選択し，選択したプロパティ２１の事前条件が，画面遷移上の直近イベントでの入力項目に起因するか判定する。
【００４６】
依存プロパティ収集部３１４は，プロパティ２１の事前条件が直近イベントの入力項目に起因しないと判定された場合に，画面遷移情報２３をもとに，画面遷移上を遡及して配置されたプロパティ２１を取得し，取得したプロパティ２１の入力判定が真となるまで，画面遷移の遡及とプロパティ取得とを繰り返し，プロパティ列を収集する。あるプロパティから画面遷移を遡って収集されたプロパティ列を，依存プロパティと呼び，依存プロパティの集合を，依存プロパティ・リストと呼ぶ。
【００４７】
プロパティ補完部３１５は，依存プロパティ収集部３１４によって入力判定が真となるプロパティ２１を抽出できなかった場合に，入力判定を真とするために不足しているプロパティを補完する。
【００４８】
依存プロパティ整理部３１６は，依存プロパティ・リストから，重複部分やデータ推移として無関係なプロパティ２１を除外して，依存プロパティ・リストを整理する。
【００４９】
データ制約生成部３１７は，依存プロパティ・リストの事前条件および事後条件ならびに連結条件を利用して，テストデータ２５の生成処理における制約条件（データ制約）を生成する。
【００５０】
データ生成部３３は，データ制約条件保持部３３１およびデータ制約ソルバ３３２を備える。
【００５１】
データ制約条件保持部３３１は，データ制約生成部３１によって生成されたデータ制約を保持する。
【００５２】
データ制約ソルバ３３２は，ＳＭＴソルバ等の既知技術を用いて，データ制約条件保持部２８が保持するデータ制約を満たすテストデータ２５を生成する。
【００５３】
以下に，検査対象がオンラインショッピングのＷｅｂアプリケーション・プログラムである場合の処理を例に，データ生成装置３の処理をより具体的に説明する。
【００５４】
なお，データ生成装置３は，特定のプログラム言語の種別，アプリケーションのアーキテクチャまたはフレームワークなどに限定されるものではない。
【００５５】
図３は，検査対象のＷｅｂアプリケーションでの画面遷移の例を示す図である。
【００５６】
以下の説明で，画面とは，ＨＴＭＬ等で記述されたＷｅｂページ記述（画面プログラム）を，Ｗｅｂブラウザで表示したページを意味する。例えば，Ｊａｖａを利用したＷｅｂアプリケーションでは，画面としてのＷｅｂページは，ＪＳＰ（Ｊａｖａ  Ｓｅｒｖｅｒ  Ｐａｇｅｓ）で記述され，利用時にＳｅｒｖｌｅｔにコンパイルされて実行処理され，処理結果がＨＴＭＬ形式でＷｅｂブラウザに送信されることによって，画面（Ｗｅｂページ）が表示される。
【００５７】
図３に示す例では，オンラインショッピングのＷｅｂアプリケーションの一部として，ログイン画面４１，商品選択画面４２，商品検索画面４３，確認画面４４，支払画面４５，および完了画面４６の画面遷移を示している。
【００５８】
ログイン画面４１は，画面項目として「ＩＤ」４１１および「パスワード」４１２，ならびに操作ボタンとして「ログインボタン」４１３を備える。ＩＤ４１１は，顧客の識別情報の入力項目であり，パスワード４１２は，顧客のパスワードの入力項目である。ログイン画面４１で，ＩＤ４１１とパスワード４１２とに入力があり，ログインボタン４１３が押下されると，商品選択画面４２に遷移する。
【００５９】
商品選択画面４２は，入力項目として「数量」４２１，操作ボタンとして「商品検索ボタン」４２２および「確認ボタン」４２３，ならびに表示項目として「氏名」４２４および「会員種別」４２５を備える。数量４２１は，商品の購入数の入力項目であり，氏名４２４および会員種別４２５は，ログイン画面４１での入力項目に対応した表示項目である。
【００６０】
商品選択画面４２では，ログイン画面４１での入力（ＩＤ，パスワード）にもとづいて，後述する顧客データベース２２１に格納された顧客データを検索し，該当した顧客名と会員種別が，氏名４２４および会員種別４２５にそれぞれ表示される。
【００６１】
商品選択画面４２で，商品検索ボタン４２２が押下されると，商品検索画面４３に遷移し，数量４２１に入力があり，確認ボタン４２３が押下されると，確認画面４４に遷移する。
【００６２】
商品検索画面４３は，操作ボタンとして「商品追加ボタン」４３１を備える。商品追加ボタン４３１が押下されると，図３の画面遷移例では省略した商品検索操作画面に遷移して商品検索操作が行われ，選択された商品の一覧を追加した商品選択画面４２へ遷移する。
【００６３】
確認画面４４は，商品選択画面４２の表示項目の再表示であり，入力項目がなく，操作ボタンとして「戻るボタン」４４１および「支払ボタン」４４２のみを備える。
【００６４】
確認画面４４で，戻るボタン４４１が押下されると，商品選択画面４２へ遷移し，支払ボタン４４２が押下されると，支払画面４５へ遷移する。
【００６５】
支払画面４５は，顧客の氏名および会員種別を含む顧客情報の表示項目，選択された商品の一覧（商品名，価格，数量，割引率，割引額，金額）を含む商品情報の表示項目４５１，ならびに操作ボタンとして「戻るボタン」４５３および「購入確定ボタン」４５２を備える。
【００６６】
支払画面４５で，戻るボタン４５３が押下されると，確認画面４４へ遷移し，購入確定ボタン４５２が押下されると，購入処理が実行されて，完了画面４６に遷移し，購入が完了する。
【００６７】
検査対象のＷｅｂアプリケーションでは，図３に示すように６個の画面間でボタン押下のイベントにより，画面が遷移する仕様となっている。
【００６８】
図４は，確認画面４４および支払画面４５間の遷移において，確認画面４４の会員種別の値（“ゴールド”か“ノーマル”か）の相違により，支払画面４５の表示項目４５１の割引率の値が異なる遷移があることを示す図である。
【００６９】
確認画面４４の表示項目，すなわち，商品選択画面４２の表示項目の会員種別の値が“ゴールド”である場合には，イベントにより支払画面４５ａへ遷移する。支払画面４５ａでは，個人情報の表示項目のうち会員種別４７１の値が“ゴールド”となり，商品情報の表示項目で割引率４７２の値が“０．１”となる。一方，会員種別が“ノーマル”である場合には支払画面４５ｂへ遷移し，支払画面４５ｂでは，会員種別４７３の値が“ノーマル”，割引率４７４の値が“０”となる。
【００７０】
図５は，データベース情報２２の例を示す図である。
【００７１】
オンラインショッピングのＷｅｂアプリケーションでは，データベース情報２２として顧客データベース２２１および商品データベース２２２の情報が使用される。
【００７２】
図５（Ａ）は，顧客データベース２２１の構成例を示す図である。顧客データベース２２１は，ＩＤ，ＰＷ，氏名，種別などの顧客データを格納する。ＩＤは顧客の識別情報，ＰＷは顧客のパスワード，氏名は顧客の名前，種別は会員種別を示す情報である。
【００７３】
図５（Ｂ）は，商品データベース２２２の構成例を示す図である。商品データベース２２２は，商品名，価格，在庫数など取り扱う商品データを格納する。商品名は商品を識別する情報，価格は商品単価，在庫数は在庫する商品数を示す情報である。
【００７４】
なお，図３および図４に示す画面遷移では，図５に示す顧客データベース２２１と商品データベース２２２が使用されるものとする。一例として，ログイン画面４１では，ＩＤ４１１とパスワード４１２の入力にもとづいて，顧客データベース２２１が検索され，該当する顧客データがあればログインが許可され，なければログインが拒否される。また，商品検索画面４３での商品検索は，商品データベース２２２に格納された商品データが検索される。この場合に，商品データベース２２２の商品データが適切に画面に表示される等の仕様をプロパティで記述することができる。
【００７５】
図６は，プロパティの例を示す図である。
【００７６】
図６に示すプロパティ２１は，図３および図４に示す画面遷移があるＷｅｂアプリケーションのプロパティの仕様例である。各プロパティは，外部仕様レベルでのプロパティの記述に，プロパティを識別するプロパティ名が対応付けられている。ここで，外部仕様レベルでのプロパティとは，画面に表示される画面項目の値やデータベースの格納データに関して記述された仕様である。
【００７７】
図６に示すプロパティ記述例において，“⇒（論理包含，導出）”の前の部分を事前条件と，後の部分を事後条件と呼ぶ。このプロパティ記述では，検査対象プログラム２７が事前条件を「真」とする状態にあるとき，遷移後の状態が事後条件を「真」とすることを要求することを示す。
【００７８】
また，“記号＃”は変数を示し，画面やデータベースが変数やフィールドを保持する場合に“保持元＃変数”と記述される。
【００７９】
また，“ＣＯＵＮＴ（ＤＢ名，条件）”は，指定されたデータベースに格納されたテーブルで，条件を満たすレコード個数を取得する関数であるとする。
【００８０】
また，“ＤＢ＃フィールド名．ｗｈｅｒｅ（条件）”は，指定されたデータベースにおいて，条件を満たすレコードの指定フィールドの値を表すとする。
【００８１】
図６に示すプロパティＰ１の記述「（ＣＯＵＮＴ（顧客ＤＢ，（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ）ＡＮＤ（顧客ＤＢ＃ＰＷ＝ログイン画面＃パスワード））＝１）＠ログインボタン押下  ⇒  （商品選択画面＃氏名＝顧客ＤＢ＃名前．ｗｈｅｒｅ（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ））ＡＮＤ（商品選択画面＃会員種別＝顧客ＤＢ＃種別．ｗｈｅｒｅ（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ））」は，
「ログインボタン押下時に，顧客ＤＢに格納されたデータのうち，（（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ）ＡＮＤ（ｐｗ＝ログイン画面＃ＰＷ））の条件を満たすデータの個数が１であるならば，商品選択画面の氏名の値は，顧客ＤＢの（ＩＤ＝ログイン画面＃ＩＤ）を満たすデータの名前フィールドの値と等しく，商品選択画面の会員種別の値は，顧客ＤＢの（ＩＤ＝ログイン画面＃ＩＤ）を満たすデータの会員種別フィールドの値と等しい」ことを意味する。
【００８２】
図７は，画面遷移情報２３の例を示す図である。本実施例では，画面遷移情報２３は，図７（Ａ）に示す画面一覧テーブル２３１および図７（Ｂ）に示す画面遷移テーブル２３２として保持される。
【００８３】
画面一覧テーブル２３１は，検査対象プログラム２７で表示される画面の一覧を示すテーブルであり，各画面について，識別番号および画面名が対応付けられている。
【００８４】
画面遷移テーブル２３２は，画面遷移を示すテーブルであり，Ｎｏ，遷移元画面，イベント，遷移先画面などが格納される。Ｎｏは遷移を識別する番号，遷移元画面は遷移元となる画面を特定する情報，イベントは遷移を生じる操作，遷移先画面は遷移先となる画面を特定する情報である。
【００８５】
図８は，画面項目情報２４の例を示す図である。本実施例では，画面項目情報２４は，各画面の画面項目テーブルとして保持される。
【００８６】
画面項目テーブルは，各画面が備える項目を示すテーブルであり，Ｎｏ，項目名，変数名，入出力，要否などが格納される。Ｎｏは項目を識別する番号，項目名は項目の名称，変数名は項目に入力／出力される値の変数名，入出力は項目の種別（入力／出力），要否はデータ推移に関係するかを示す情報（関係がある場合は“要”）である。
【００８７】
図８（Ａ）はログイン画面４１の画面項目テーブル例，図８（Ｂ）は商品選択画面４２の画面項目テーブル例，図８（Ｃ）は確認画面４４の画面項目テーブル例，図８（Ｄ）は支払画面４５の画面項目テーブル例を示す。
【００８８】
以下，データ生成装置３のデータ制約生成部３１の処理動作について，図３に示す画面遷移を持つＷｅｂアプリケーションを例に説明する。
【００８９】
図９は，データ制約生成部３１の処理フロー例を示す図である。
【００９０】
情報取得処理（ステップＳ１）：  画面情報設定部３１１は，記憶部２０から，検査対象プログラム２７の画面遷移情報２３および画面項目情報２４を読み込む。
【００９１】
プロパティ配置処理（ステップＳ２）：  プロパティ配置部３１２は，プロパティ２１を読み込み，画面遷移情報２３および画面項目情報２４にもとづいて，プロパティ２１各々が，画面遷移上のどの遷移の仕様に該当するかを判定し，プロパティ２１を該当する画面遷移に関連付けて，画面遷移上に配置する。
【００９２】
プロパティの入力判定処理（ステップＳ３）：  入力判定部３１３は，画面遷移に配置されたプロパティ２１を順に選択し，選択したプロパティ２１の事前条件が，画面遷移上で直近イベントでの入力項目に起因するかを判定する。事前条件が入力項目に起因する場合に，そのプロパティ２１の入力判定を「真」とする。
【００９３】
プロパティ遡及取得処理（ステップＳ４）：  依存プロパティ収集部３１４は，プロパティ２１の事前条件が直近イベントの入力項目に起因していない場合に，画面遷移上を遡って画面遷移に配置されたプロパティ２１を取得し，取得したプロパティ２１の入力項目の判定が真となるまで，プロパティ取得を繰り返す。
【００９４】
依存プロパティ抽出処理（ステップＳ５）：  依存プロパティ収集部３１４は，取得したプロパティ２１をもとに，入力判定が真となるまで収集したプロパティの集合（プロパティ列）を，依存プロパティとして抽出する。
【００９５】
プロパティ補完処理（ステップＳ６）：  プロパティ補完部３１５は，依存プロパティ収集部３１４によって入力判定が真となるプロパティ２１を抽出できなかった場合に，入力判定を真とするために不足しているプロパティを補完する。
【００９６】
依存プロパティ整理処理（ステップＳ７）：  依存プロパティ整理部３１６は，抽出された依存プロパティの中で，重複またはデータ推移として無関係なプロパティ２１を除外する。
【００９７】
制約条件生成処理（ステップＳ８）：  データ制約生成部３１７は，依存プロパティにおいて，連続するプロパティの事前条件および事後条件ならびに連結条件にもとづいて，テストデータ２５の生成の制約条件となるデータ制約を生成する。
【００９８】
図１０は，プロパティ配置処理（ステップＳ２）のより詳細な処理フロー例を示す図である。
【００９９】
プロパティ配置部３１２は，画面情報設定部３１１が保持する画面遷移情報２３，画面項目情報２４を読み込み，記憶部２０からプロパティ２１を読み込む（ステップＳ１０）。プロパティ配置部３１２は，読み込んだプロパティ２１を順に選択して，未処理のプロパティ２１があれば（ステップＳ１１のＹ），プロパティ２１を事前条件と事後条件とに分け，各条件に含まれる変数およびイベントを抽出し（ステップＳ１２），未処理のプロパティ２１がなければ（ステップＳ１１のＮ），ステップＳ１７の処理へ進む。
【０１００】
さらに，プロパティ配置部３１２は，画面遷移テーブル２３２から，ステップＳ１２の処理で抽出したイベントと一致するイベントを含む行を全て抽出する（ステップＳ１３）。プロパティ配置部３１２は，画面遷移テーブル２３２から抽出した行を順に選択して，未処理の抽出行があれば（ステップＳ１４のＹ），ステップＳ１５の処理へ進み，未処理の抽出行がなければ（ステップＳ１４のＮ），ステップＳ１１の処理へ戻る。
【０１０１】
ステップＳ１５で，プロパティ配置部３１２は，抽出された変数，イベントにおいて，事前条件または事後条件の変数が，それぞれ，抽出された画面遷移テーブル２３２の行の遷移元画面または遷移後画面のものと一致するかを判定する（ステップＳ１５）。
【０１０２】
抽出された変数，イベントにおいて，遷移元画面または遷移後画面の変数が一致すると判定した場合に（ステップＳ１５のＹ），プロパティ配置部３１２は，一致した画面遷移テーブルの行とプロパティとを関連付けて，結果テーブルに格納する（ステップＳ１６）。一方，抽出された変数，イベントにおいて，変数が一致しないと判定した場合に（ステップＳ１５のＮ），プロパティ配置部３１２は，ステップＳ１４の処理へ戻る。
【０１０３】
ステップＳ１１で，未処理のプロパティがなければ（ステップＳ１１のＮ），プロパティ配置部３１２は，結果テーブルを保持して（ステップＳ１７），処理を終了する。
【０１０４】
図１１は，プロパティ配置部３１２によって，各プロパティ２１から抽出される情報（事前条件の変数，イベント，事後条件の変数）をテーブルとして示す図である。
【０１０５】
図１１により，プロパティＰ１から，事前条件の変数として「ログイン画面＃ＩＤ，ログイン画面＃パスワード，顧客ＤＢ＃ＩＤ，顧客ＤＢ＃ＰＷ」が，イベントとして「ログインボタン」が，事後条件の変数として「商品選択画面＃氏名，商品選択画面＃会員種別，ログイン画面＃ＩＤ，顧客ＤＢ＃ＩＤ，顧客ＤＢ＃名前，顧客ＤＢ＃種別」が，それぞれ抽出されたことがわかる。
【０１０６】
図１２は，プロパティ配置部３１２で生成される結果テーブルの例を示す図である。
【０１０７】
プロパティ配置部３１２の結果テーブルでは，各遷移の内容（遷移元画面，イベント，遷移先画面）に，関連付けられたプロパティ２１が設定される。
【０１０８】
図１３は，プロパティ配置部２１３の処理結果（結果テーブル）を，画面遷移上に対応付けて示す図である。
【０１０９】
画面遷移上で，一例として，配置結果テーブルのＮｏ．１のログイン画面４１から商品選択画面４２への画面遷移に対しプロパティＰ１が関連付けて設置されていることが表されている。また，確認画面４４から支払画面４５ａへの画面遷移に対し，プロパティＰ５，Ｐ７，Ｐ８が，確認画面４４から支払画面４５ｂへの画面遷移に対し，プロパティＰ６，Ｐ７，Ｐ８が，それぞれ設置されている。
【０１１０】
図１４は，プロパティの入力判定処理（ステップＳ３）のより詳細な処理フロー例を示す図である。
【０１１１】
入力判定部３１３は，プロパティ配置部３１２の結果テーブルから，画面遷移上で各画面遷移に配置されたプロパティの集合を取得する（ステップＳ２０）。入力判定部３１３は，取得したプロパティの集合から，プロパティ２１を順に選択し（ステップＳ２１），未選択のプロパティ２１があれば（ステップＳ２２のＹ），事前条件の画面変数を抽出し（ステップＳ２３），未選択のプロパティ２１がなければ（ステップＳ２２のＮ），ステップＳ２１０の処理へ進む。
【０１１２】
さらに，入力判定部３１３は，抽出した画面変数を順に選択し（ステップＳ２４），未選択の事前条件の画面変数があれば（ステップＳ２５のＹ），ステップＳ２７の処理へ進み，未選択の画面変数がなければ（ステップＳ２５のＮ），そのプロパティ２１の入力判定を，「真（ＯＫ）」として（ステップＳ２６），ステップＳ２１の処理へ戻る。
【０１１３】
ステップＳ２７で，入力判定部３１３は，選択した事前条件の画面変数が，そのプロパティ２１のイベントが生じる画面での入力項目であるかを判定する。選択した事前条件の画面変数が，そのプロパティ２１のイベントが生じる画面での入力項目であれば（ステップＳ２７のＹ），抽出した事前条件の画面変数の入力判定を「真（ＯＫ）」として（ステップＳ２８），ステップＳ２４の処理へ戻る。事前条件の画面変数が入力項目でなければ（ステップＳ２７のＮ），入力判定部３１３は，そのプロパティの入力判定を「偽（ＮＧ）」として（ステップＳ２９），ステップＳ２１の処理へ戻る。
【０１１４】
ステップＳ２１０で，入力判定部３１３は，結果を出力して，処理を終了する。
【０１１５】
図１５は，入力判定部３１３の処理結果（結果テーブル）例を示す図である。
【０１１６】
入力判定部３１３が出力する結果テーブルでは，各プロパティ２１について，プロパティの入力判定の結果，および，プロパティに含まれる事前条件の変数ごとの入力判定結果（個別入力判定）が設定される。画面変数の個別入力判定に「偽（ＮＧ）」が１つでもある場合には，そのプロパティの入力判定の結果は「偽（ＮＧ）」と判定される。
【０１１７】
また，プロパティに事前条件の画面変数が含まれない場合には，事前条件の画面変数に「なし」が，個別入力判定に「真（ＯＫ）」が記録される。
【０１１８】
図１６は，入力判定部３１３の処理の結果を，画面遷移に対応付けて示す図である。
【０１１９】
図１６に示す画面遷移には，各遷移に配置されたプロパティ２１に，図１５に示す結果テーブルの内容に対応した入力判定の結果が設定されている。例えば，ログイン画面４１から商品選択画面４２への遷移に配置されたプロパティＰ１の入力判定は「真（ＯＫ）」であることを示している。
【０１２０】
図１７は，プロパティ遡及取得処理（ステップＳ４）および依存プロパティ抽出処理（ステップＳ５）のより詳細な処理フロー例を示す図である。
【０１２１】
依存プロパティ収集部３１４は，入力判定部３１３の結果テーブルから，入力判定が「偽（ＮＧ）」とされたプロパティ２１の集合を取得する（ステップＳ３０）。依存プロパティ収集部３１４は，取得したプロパティの集合からプロパティを順に選択し（ステップＳ３１），未選択のプロパティがあれば（ステップＳ３２のＹ），入力判定部３１３で個別入力判定が「偽（ＮＧ）」であった変数を取得して，未解決変数とする（ステップＳ３３）。未処理のプロパティがなければ（ステップＳ３２のＮ），ステップＳ３１２の処理へ進む。
【０１２２】
依存プロパティ収集部３１４は，入力判定部３１３の結果テーブルを用いて，そのプロパティ２１を起点として画面遷移を遡り，遷移に配置されたプロパティ２１を取得し（ステップＳ３４），プロパティ２１が取得できたかを判定する（ステップＳ３５）。
【０１２３】
画面遷移を遡ってプロパティ２１が取得できた場合に（ステップＳ３５のＹ），依存プロパティ収集部３１４は，取得したプロパティ２１の事前条件および事後条件に未解決変数が含まれ，かつ，未解決変数を含む条件式が未解決変数との等式であるかを判定する（ステップＳ３６）。依存プロパティ収集部３１４は，その未解決変数が，ステップＳ３６の判定条件を満たす場合に（ステップＳ３６のＹ），ステップＳ３８の処理へ進む。画面遷移を遡ってプロパティが取得できなかった場合（ステップＳ３５のＮ），または，遡って取得したプロパティにおいて未解決変数が上記のステップＳ３６の判定条件を満たさなかった場合（ステップＳ３６のＮ）に，ステップＳ３７の処理へ進む。
【０１２４】
ステップＳ３７では，依存プロパティ収集部３１４は，図１８に例示する作業テーブルに，選択したプロパティ２１を，未解決プロパティとして「未解決（×）」を記録し，ステップＳ３１の処理へ戻る。図１８に示す作業テーブルは，プロパティごとに，未解決変数，依存プロパティ，依存プロパティの事後条件が含む遷移元変数，解決の状態を示す。
【０１２５】
ステップＳ３８では，依存プロパティ収集部３１４は，画面遷移を遡って取得したプロパティ２１を依存プロパティ・リストに追加し，作業テーブルに，未解決変数およびその未解決変数と等号で関係付けられた変数を「遷移元変数」として記録する。さらに，依存プロパティ収集部３１４は，画面遷移を遡って取得したプロパティ２１の入力判定が「真（ＯＫ）」であるかを判定する（ステップＳ３９）。
【０１２６】
依存プロパティ収集部３１４は，画面遷移を遡って取得したプロパティ２１の入力判定が真であれば（ステップＳ３９のＹ），作業テーブルの該当する未解決変数の解決欄に「解決（○）」を記録する（ステップＳ３１０）。プロパティの入力判定が真でなければ（ステップＳ３９のＮ），依存プロパティ収集部３１４は，作業テーブルの該当する未解決変数の解決欄に「未解決（×）」を記録し，遷移元画面の画面変数を未解決変数に追加して（ステップＳ３１０），ステップＳ３１の処理へ戻る。
【０１２７】
ステップＳ３１２では，依存プロパティ収集部３１４は，処理結果として，依存プロパティ・リストを出力して，処理を終了する。
【０１２８】
図１９は，依存プロパティ収集部の出力結果である依存プロパティで・リストの例を示す図である。
【０１２９】
依存プロパティ・リストには出力された依存プロパティ列の一覧が記録され，依存プロパティ列ごとに，識別番号（Ｎｏ）と，依存プロパティ列に含まれるプロパティ２１が記録される。例えば，Ｎｏ＝１の依存プロパティ列は，プロパティＰ３，プロパティＰ１を要素とするプロパティの集合であることを示す。
【０１３０】
図２０は，依存プロパティ収集部３１４の処理の結果を，画面遷移に対応付けて示す図である。
【０１３１】
図２０に示す画面遷移には，各遷移に設置されたプロパティ２１に，図１９に示す依存プロパティ・リスト中の対応する依存プロパティ列が設定されている。例えば，商品選択画面４２から確認画面４４への遷移のプロパティＰ３に対して，プロパティ列｛プロパティＰ３，プロパティＰ１｝が対応付けられている。
【０１３２】
図２１は，プロパティ整理処理（ステップＳ７）のより詳細な処理フロー例を示す図である。
【０１３３】
依存プロパティ整理部３１６は，依存プロパティ・リスト（依存プロパティ列の集合）を取得する（ステップＳ４０）。依存プロパティ整理部３１６は，依存プロパティ・リストから，依存プロパティ列を順に選択し（ステップＳ４１），未選択の依存プロパティ列があれば（ステップＳ４２のＹ），ステップＳ４３の処理へ進み，未選択の依存プロパティ列がなければ（ステップＳ４２のＮ），ステップＳ４６の処理へ進む。
【０１３４】
ステップＳ４３では，依存プロパティ整理部３１６は，選択した依存プロパティ列と，依存プロパティ・リストの他の依存プロパティ列とを比較し，選択した依存プロパティ列が他の依存プロパティ列に含まれるかを調べて（ステップＳ４４）。
【０１３５】
ここで，依存プロパティ列Ｌ１が，依存プロパティ列Ｌ２に含まれるとは，以下の包含条件Ｃ１または包含条件Ｃ２が成立することを意味する。
【０１３６】
包含条件Ｃ１＝依存プロパティ列Ｌ１の全ての要素プロパティが，依存プロパティ列Ｌ２の要素である。
【０１３７】
包含条件Ｃ２＝依存プロパティ列Ｌ１と依存プロパティ列Ｌ２は，２番目以降のプロパティ要素は同一で１番目のプロパティ要素だけが相違であり，かつ，依存プロパティ列Ｌ１の１番目のプロパティの事前条件が，依存プロパティ列Ｌ２の１番目のプロパティの事前条件に含まれる。
【０１３８】
依存プロパティ整理部３１６は，選択した依存プロパティ列が他の依存プロパティ列に含まれる場合に（ステップＳ４４のＹ），その選択した依存プロパティ列を，依存プロパティ・リストから削除する（ステップＳ４５）。選択した依存プロパティ列が他の依存プロパティ列に含まれない場合に（ステップＳ４４のＮ），依存プロパティ整理部３１６は，ステップＳ４１の処理へ戻る。
【０１３９】
ステップＳ４６では，依存プロパティ整理部３１６は，処理結果を出力し，処理を終了する。
【０１４０】
図２２は，依存プロパティ整理部の処理結果（結果テーブル）の例を示す図である。
【０１４１】
図２２に示す依存プロパティ・リストにおいて，Ｎｏ＝１の依存プロパティ列は，包含条件Ｃ１により，Ｎｏ＝２および３の依存プロパティ列に含まれる。また，Ｎｏ＝４の依存プロパティ列は，包含条件Ｃ２によりＮｏ＝２および３の依存プロパティ列に含まれる。よって，依存プロパティ整理部３１６によって，依存プロパティ・リストから，Ｎｏ＝１および４の依存プロパティ列が削除される。
【０１４２】
図２３は，制約条件生成処理（ステップＳ８）のより詳細な処理フロー例を示す図である。
【０１４３】
データ制約生成部３１７は，依存プロパティ整理部３１６の結果テーブルから，依存プロパティ・リストを取得する（ステップＳ５０）。データ制約生成部３１７は，依存プロパティ・リストから依存プロパティ列を順に選択し（ステップＳ５１），未選択の依存プロパティ列があれば（ステップＳ５２のＹ），ステップＳ５３の処理へ進み，未選択の依存プロパティ列がなければ（ステップＳ５２のＮ），ステップＳ５４の処理へ進む。
【０１４４】
ステップＳ５３では，データ制約生成部３１７は，選択した依存プロパティ列の１番目のプロパティの事前条件，２番目から最後までのプロパティの事前条件および事後条件を，ＡＮＤで結合してデータ制約として結果テーブルに保存し，ステップＳ５１の処理へ戻る。
【０１４５】
ステップＳ５４では，データ制約生成部３１７は，結果テーブルを出力する。
【０１４６】
図２４は，データ制約生成部の処理結果（結果テーブル）の例を示す図である。
【０１４７】
データ制約生成部３１７の結果テーブルでは，データ制約ごとに，識別番号（Ｎｏ），および依存プロパティ列を構成するプロパティ要素（依存プロパティ），データ制約の内容が記録される。
【０１４８】
例えば，Ｎｏ＝１のデータ制約として，
「（確認画面＃会員種別＝“ゴールド”）ＡＮＤ（商品選択画面＃会員種別！＝“”）ＡＮＤ（商品選択画面＃数量＞０）ＡＮＤ（商品選択画面＃氏名＝確認画面＃氏名）ＡＮＤ（商品選択画面＃会員種別＝確認画面＃会員種別）ＡＮＤ（商品選択画面＃数量＝確認画面＃数量）ＡＮＤ（商品選択画面＃商品名＝確認画面＃商品名）ＡＮＤ（商品選択画面＃価格＝確認画面＃価格）ＡＮＤ（ＣＯＵＮＴ（顧客ＤＢ，（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ）ＡＮＤ（顧客ＤＢ＃ＰＷ＝ログイン画面＃パスワード））＝１）ＡＮＤ（商品選択画面＃氏名＝顧客ＤＢ＃名前．ｗｈｅｒｅ（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ））ＡＮＤ（商品選択画面＃会員種別＝顧客ＤＢ＃種別．ｗｈｅｒｅ（顧客ＤＢ＃ＩＤ＝ログイン画面＃ＩＤ））」
という制約条件の記述が生成され，記録される。
【０１４９】
プロパティ補完処理（ステップＳ６）は，依存プロパティ収集部３１４によって，入力判定が真となるプロパティ・リストを抽出できなかった場合のみ，依存プロパティ収集部３１４によって実行される。
【０１５０】
図２５および図２６は，入力判定が真とならないプロパティの例を示す図である。
【０１５１】
図２５に示すプロパティ・リストでは，図６に例示するプロパティ２１と比べて，プロパティＰ３の事後条件において，「（商品選択画面＃会員種別＝確認画面＃会員種別）」の条件がない。このような条件の欠落は，プロパティＰ３で，遷移元画面である商品選択画面４２と遷移先画面である確認画面４４において，表示項目の会員種別が同一であるとして省略されていることなどから生じる。
【０１５２】
また，図２６に示すプロパティ・リストでは，図６に示すプロパティＰ３自体がない。このようなプロパティ２１の欠落は，遷移元画面である商品選択画面４２と遷移先画面である確認画面４４の表示項目が全て同一であることなどから生じる。
【０１５３】
図２５および図２６のいずれの例でも，図６に示すプロパティＰ３の事後条件の「（商品選択画面＃会員種別＝確認画面＃会員種別）」がないために，依存プロパティ・リスト収集部３１４によって，入力判定が真となるプロパティを抽出することができない。
【０１５４】
図２７は，プロパティ補完処理（ステップＳ６）のより詳細な処理フロー例を示す図である。
【０１５５】
プロパティ補完部３１５は，記憶部２０から，画面遷移情報２３，画面項目情報２４，およびプロパティ２１と，プロパティ配置手段３１２の結果テーブルとを読み込む（ステップＳ６０）。プロパティ補完部３１５は，画面遷移情報２３から，遷移関係にある画面の組を取得する（ステップＳ６１）。プロパティ補完部３１５は，未処理の画面の組があれば（ステップＳ６２のＹ），ステップＳ６３の処理へ進み，未処理の画面の組がなければ（ステップＳ６２のＮ），ステップＳ６９の処理へ進む。
【０１５６】
ステップＳ６３の処理では，プロパティ補完部３１５は，その画面の組の遷移に配置されたプロパティを取得し，プロパティが取得できれば（ステップＳ６４のＹ），ステップＳ６５の処理へ進み，プロパティが取得できなければ（ステップＳ６４のＮ），ステップＳ６８の処理へ進む。
【０１５７】
ステップＳ６５では，プロパティ補完部３１５は，遷移元画面の画面項目のうち，取得したプロパティの事後条件に登場しない画面項目があるかを調べ，登場しない画面項目があれば（ステップＳ６５のＹ），その画面項目を収集する（ステップＳ６６）。さらに，プロパティ補完部３１５は，遷移元画面の未登場の画面項目に関してプロパティを生成して（ステップＳ６７），ステップＳ６１の処理へ戻る。プロパティ補完部３１５は，登場しない画面項目がなければ（ステップＳ６５のＮ），ステップＳ６１の処理へ戻る。
【０１５８】
遷移元画面の未登場の画面項目に関するプロパティの生成は，例えば以下のように行う。
【０１５９】
・  事前条件は「ＴＲＵＥ」とする，
・  イベントは，この画面間の遷移を起こすイベントとする，
・  事後条件は，未登場の画面項目が，遷移先画面において未登場の画面項目名と同名の画面項目と等しいとする。このとき，遷移先画面に，未登場の画面項目名と同名の画面項目がない場合でも，遷移先画面に該名の画面項目があるとして，上記の条件を生成する。
【０１６０】
ステップＳ６４の処理では，プロパティが取得できなければ（ステップＳ６４のＮ），プロパティ補完部３１５は，遷移元画面の全ての画面項目を，非存在の画面項目として（ステップＳ６８）ステップＳ６７の処理へ進む。
【０１６１】
ステップＳ６９では，プロパティ補完部３１５は，処理結果（結果テーブル）を保持する。
【０１６２】
図２８は，プロパティ補完部の処理結果の例を示す図である。
【０１６３】
図２８（Ａ）に示す結果テーブルは，図２５に示すプロパティに対する補完として生成されたプロパティ記述である。
【０１６４】
プロパティ補完部３１５によって，遷移元画面である商品選択画面４２の画面項目のうち，取得したプロパティＰ３の事後条件に登場しない項目として「会員種別」が特定され，遷移先画面である確認画面４４の同一名の項目とをもとに，「（商品選択画面＃会員種別＝確認画面＃会員種別）」が生成される。さらに，事前条件が「ＴＲＵＥ」であり，イベントが，この遷移を起こす「確認ボタン押下」であり，事後条件が「（商品選択画面＃会員種別＝確認画面＃会員種別）」であるプロパティ記述が生成される。
【０１６５】
図２８（Ｂ）は，図２６に示すプロパティに対する補完として生成されたプロパティ記述である。
【０１６６】
プロパティ補完部３１５によって，遷移元画面である商品選択画面４２の全ての画面項目を用いて，「（商品選択画面＃氏名＝確認画面＃氏名）ＡＮＤ（商品選択画面＃会員種別＝確認画面＃会員種別）ＡＮＤ（商品選択画面＃数量＝確認画面＃数量）ＡＮＤ（商品選択画面＃商品名＝確認画面＃商品名）ＡＮＤ（商品選択画面＃価格＝確認画面＃価格）」が生成される。そして，事前条件が「ＴＲＵＥ」であり，イベントが，この遷移を起こす「確認ボタン押下」であり，事後条件が上記の生成された記述であるプロパティ記述が生成される。
【０１６７】
以上説明したように，データ生成装置３では，データ制約生成部３１がプロパティ事前条件からテストデータ２５の生成のためのデータ制約を生成し，データ生成部３３が，ＳＭＴソルバでそのデータ制約を解くことによって，モデル検査用のテストデータを生成することができる。
【０１６８】
データ生成装置３によれば，実行経路上においてプロパティが前後関係を持って設定されている検査対象プログラムについて，そのプロパティの事前条件が真となるようなデータを生成のためのデータ制約を決定できるようになり，モデル検査のためのテストデータ生成の処理負担を軽減させることができる。
【０１６９】
また，データ生成装置３によれば，前後関係を持つプロパティにもとづいて構成されたデータ制約（制約条件）が，ＳＭＴソルバやＳＡＴソルバを利用したデータ生成部３３に指定されることによって，データ制約を満たす具体的なデータを生成することができる。
【符号の説明】
【０１７０】
１  モデル検査装置
１０  制御部
２０  記憶部
２１  プロパティ
２２  データベース（ＤＢ）情報
２３  画面遷移情報
２４  画面項目情報
２５  テストデータ
２７  検査対象プログラム
３  データ生成装置
３１  データ制約生成部
３１１  画面情報設定部
３１２  プロパティ配置部
３１３  入力判定部
３１４  依存プロパティ収集部
３１５  プロパティ補完部
３１６  依存プロパティ整理部
３１７  データ制約生成部
３３  データ生成部
３３１  データ制約条件保持部
３３２  データ制約ソルバ
５  検査実行装置
５１  ドライバ
５３  検査実行部
【図１】
0005561135.tif 000002
【図２】
0005561135.tif 000003
【図３】
0005561135.tif 000004
【図４】
0005561135.tif 000005
【図５】
0005561135.tif 000006
【図６】
0005561135.tif 000007
【図７】
0005561135.tif 000008
【図８】
0005561135.tif 000009
【図９】
0005561135.tif 000010
【図１０】
0005561135.tif 000011
【図１１】
0005561135.tif 000012
【図１２】
0005561135.tif 000013
【図１３】
0005561135.tif 000014
【図１４】
0005561135.tif 000015
【図１５】
0005561135.tif 000016
【図１６】
0005561135.tif 000017
【図１７】
0005561135.tif 000018
【図１８】
0005561135.tif 000019
【図１９】
0005561135.tif 000020
【図２０】
0005561135.tif 000021
【図２１】
0005561135.tif 000022
【図２２】
0005561135.tif 000023
【図２３】
0005561135.tif 000024
【図２４】
0005561135.tif 000025
【図２５】
0005561135.tif 000026
【図２６】
0005561135.tif 000027
【図２７】
0005561135.tif 000028
【図２８】
0005561135.tif 000029