(57)【要約】【課題】プログラムモデル検査において、擬似システムのプロパティから繰り返しの要因を抽出し、該要因による繰り返しを停止させる条件を加味した最適な同値クラスを生成し、無駄な繰り返しを減少させるデータ生成プログラム、データ生成装置およびデータ生成方法を提供する。【解決手段】擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出し、帰結部を構成する部分式が予め決められた再帰的定義により記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、要因式と再帰変数に基づいて、要因変数を特定する処理と、要因プロパティに対応する同値クラスから再帰変数を含む部分式を抽出し、否定条件式を作成し、否定条件式と要因式に基づいて要因変数に関する停止条件を算出する処理と、条件式および繰り返し停止条件に基づいて最適化同値クラスを生成する処理を、実行する。【選択図】図１
2010191507.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータに、
記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出し、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、前記形式で記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定する繰り返し要因特定処理と、
前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出し、抽出した部分式である条件式を否定した否定条件式を作成し、前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出する繰り返し停止条件抽出処理と、
前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する最適化同値クラス生成処理と、
を実行させることを特徴とするデータ生成プログラム。
【請求項２】
最適化同値クラス生成処理は、
前記条件式と前記繰り返し停止条件との論理積を作成して要因変数に関する条件式を再構築し、再構築した該条件式に前記要因変数以外の変数に関する条件式を加えた最適化同値クラスを生成することを特徴とする請求項１に記載のデータ生成プログラム。
【請求項３】
記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出し、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、前記形式で記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定する繰り返し要因特定部と、
前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出し、抽出した部分式である条件式を否定した否定条件式を作成し、前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出する繰り返し停止条件抽出部と、
前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する最適化同値クラス生成部と、
を備えることを特徴とするデータ生成装置、
【請求項４】
記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出し、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、
前記予め決められた形式で記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、
前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定し、
前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出し、
前記抽出した部分式である条件式を否定した否定条件式を作成し、
前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出し、
前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する、
ことを特徴とするデータ生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、効率的なモデル検査を行うためのデータ生成技術に関する。
【背景技術】
【０００２】
モデル検査とは、テスト対象システムの振舞いを設計書・仕様書から取り出し、モデル検査の専用言語で記述したプログラム（擬似システム）を作成し、当該擬似システムにテストデータを入力することで実施するテストのことである。テストデータは、設計書・仕様書に基づき、状態遷移の各状態が取りうる全ての組み合わせを抽出したものである。
【０００３】
図１１は従来のモデル検査を実施するときに用いる構成を示す図である。クライアントの代わりにドライバ１１１から検査対象プログラム１１２に対してユーザ操作を模倣した入力データ１１６が入力される。図１１では検査対象プログラム１１２と検査対象プログラム１１２に接続されているデータベーススタブ１１３とネットワークスタブ１１４に対して網羅的な検査が行われる。
【０００４】
ドライバ１１１は検査対象プログラム１１２をさまざまなバリエーションで複数回、連続的に呼び出していく。モデル検査装置１１５は、その中で機能仕様（プロパティ１１７に格納されている）が満たされているかチェックする。検査対象プログラム１１２をさまざまな実行順序で呼び出す際、引数として渡す入力データもさまざまなバリエーションが必要である。
【０００５】
また、対象プログラム１１２のあらゆる動作を想定して検査ができるドライバ１１１を作成するためには、対象プログラム１１２の操作イベント、および操作イベントの引数となるデータについて、仕様上可能な組み合わせを再現できるようにする必要がある。
【０００６】
そこで、従来は上記のような網羅的なドライバ作成のためのデータ設計について、各データについて機能仕様から同値分割を行い、その各同値クラスから代表値を選ぶ方法(境界値分析)が実施されている。
【０００７】
しかしながら、状態空間を明示的に探索するＪａｖａ  ＰａｔｈＦｉｎｄｅｒに代表されるようなプログラムモデル検査手法において、従来の境界値分析を適用すると次のような問題が生じる。
【０００８】
既存の境界値分析をもとに作成された代表値から状態空間を作成すると、検査の観点において同様の局面を表わす部分的なグラフが複数回繰り返して出現する可能性がある。
このように従来の境界値分析では、部分的なグラフの繰り返し構造を防ぐことを加味した同値分割は不可能であり、特にモデル検査では状態爆発につながる問題がある。
【０００９】
なお、特許文献１にはデータ定義文から各種代表値を抽出するという技術や、各種代表値をテストデータとして用いるような技術が提案されている。
【先行技術文献】
【特許文献】
【００１０】
【特許文献１】特許３１０５２７９号公報
【発明の概要】
【発明が解決しようとする課題】
【００１１】
上記のような実情に鑑みてなされたものであり、プログラムモデル検査手法において、擬似システムのプロパティから繰り返しの要因を抽出し、当該要因による繰り返しを停止させる条件を加味した最適な同値クラスを生成することにより、無駄な繰り返しを減少させるデータ生成プログラム、データ生成装置およびデータ生成方法を提供することを目的とする。
【課題を解決するための手段】
【００１２】
態様のひとつは、繰り返し要因特定処理、繰り返し停止条件抽出処理、最適化同値クラス生成処理を実行する。
繰り返し要因特定処理は、記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出する。そして、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、前記形式で記述されていれば要因式と特定する。さらに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定する。繰り返し停止条件抽出処理は、前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出する。抽出した部分式である条件式を否定した否定条件式を作成し、前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出する。最適化同値クラス生成処理は、前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する。
【発明の効果】
【００１３】
擬似システムのプロパティから繰り返しの要因を抽出し、当該要因による繰り返しを停止させる条件を加味した最適な同値クラスを生成することにより、無駄な繰り返しを減少させることができる。
【図面の簡単な説明】
【００１４】
【図１】実施例１の構成を示す図である。
【図２】プロパティと同値クラスの関係を示す図である。
【図３】プロパティＰ１〜Ｐ３に対する同値クラスと最適化同値クラスのモデル検査の比較結果を示す図である。
【図４】データ生成装置１の詳細な構成を示す図である。
【図５】プロパティテーブルと同値クラステーブルの構造を示す図である。
【図６】データ生成装置１の動作を示すフロー図である。
【図７】帰結式テーブル、要因テーブルの構造を示す図である。
【図８】停止条件テーブルの構造を示す図である。
【図９】同値クラステーブルの構造を示す図である。
【図１０】本発明を実現させるためのシステム構成を示したブロック図である
【図１１】従来のモデル検査を実施するときに用いる構成を示す図である。
【発明を実施するための形態】
【００１５】
以下図面に基づいて、本発明の実施形態について詳細を説明する。
（実施例１）
図１は、擬似システムである検査対象プログラムのモデル検査を行うシステムの構成を示す図である。
【００１６】
データ生成装置１は、検査対象プログラムと、検査対象プログラムの実行を制御するドライバと、機能仕様を示すプロパティ８を用いて、プロパティ８に示される機能仕様が満たされているかを判定するモデル検査装置（図１に不図示）に入力する入力データを生成
する。
また、モデル検査に用いる入力データを生成するデータ生成装置１は、繰り返し要因特定部２、繰り返し停止条件抽出部３、最適化同値クラス生成部４を備えている。
【００１７】
（繰り返し要因特定処理）
繰り返し要因特定部２は、記録部に記録されている擬似システムのモデル検査に用いるプロパティ８から帰結部を抽出する。例えば、プロパティ８には、仕様書や設計書に記載された機能仕様が「Ａ（条件部）ならばＢ（帰結部）」（Ａ−＞Ｂ）の形で示されている（図２参照）。帰結部はＢに当たる部分である。
【００１８】
図２のＰ１の場合であれば、条件部が、（１０≦在庫数−数量）ａｎｄ（顧客コード！＝ｎｕｌｌ）であり、帰結部が（メッセージ＝ｎｕｌｌ）ａｎｄ（在庫数（ａｆｔｅｒ）＝在庫数−数量）である。また、帰結部の特定は「→」を検出して、「→」の後段にある文字列を帰結部に特定する方法が考えられる。
【００１９】
次に、帰結部を構成する部分式が予め決められた形式で記述されているか判定し、予め決められた形式で記述されていれば要因式と再帰変数を特定する。
帰結部を構成する部分式とは、図２のＰ１の場合であれば、帰結部が（メッセージ＝ｎｕｌｌ）ａｎｄ（在庫数（ａｆｔｅｒ）＝在庫数−数量）であり、部分式は（メッセージ＝ｎｕｌｌ）と（在庫数（ａｆｔｅｒ）＝在庫数−数量）のことである。部分式の特定は「ａｎｄ」（論理積）を検出して、「ａｎｄ」の前後の文字列を分割して特定する方法が考えられる。
【００２０】
要因式と再帰変数の特定は、予め決められた形式ｖａｒ（ａｆｔｅｒ）＝ｏｐ（ｖａｒ，ｖａｒ’）のような再帰的な式（予め決められた再帰的定義により記載された式）されている部分式であるかを判定する。ここで、ｏｐは２項演算子（例えば＋、−）であり、ｖａｒは再帰変数を示している。
【００２１】
図２のＰ１の場合であれば、部分式（在庫数（ａｆｔｅｒ）＝在庫数−数量）が再帰的な式で表されていることがわかる。つまり、在庫数が再帰変数（ｖａｒ）であり、在庫数を含む部分式を要因式（再帰的な式）として特定する。また、要因式を含むプロパティを特に要因プロパティと呼ぶ。
【００２２】
次に、要因式と再帰変数に基づいて、要因式に含まれる繰り返しの要因となる要因変数を特定する。要因変数の特定は、上記ｖａｒ（ａｆｔｅｒ）＝ｏｐ（ｖａｒ，ｖａｒ’）のｖａｒ’に相当する変数である。図２のＰ１のプロパティの場合であれば、要因変数は、要因式（在庫数（ａｆｔｅｒ）＝在庫数−数量）の数量に相当する。
その後、特定した要因式、再帰変数、要因変数は記録部に記録される。
【００２３】
（繰り返し停止条件抽出処理）
繰り返し停止条件抽出部３は、記録部に記録されている要因式を含む要因プロパティに対応する同値クラスから再帰変数を含む部分式を抽出する。
【００２４】
ここで、同値クラスは、境界値分析装置７によりプロパティに基づいて生成される。同値クラスの生成について詳しい説明はしないが、図２のＰ１の例であれば、境界値分析装置７は、条件部（１０≦在庫数−数量）ａｎｄ（顧客コード！＝ｎｕｌｌ）を特定する。そして、予め決められた変数を含む部分式を特定する。本例では、部分式（１０≦在庫数−数量）が特定される。次に、同値分割を行い、例えば、在庫数＝１００、数量＞０の条件で、部分式（１０≦在庫数−数量）に対する同値クラスを求める。その結果、図２の同値クラスのＣ１に示すような０＜数量≦９０が求められる。さらに、代表値選択を行い、
代表値を求める。本例では図２の代表値のＣ１に示すような数量＝１が求められる。このように求められた同値クラスは、各プロパティと関連付けて記録部に記録される。
【００２５】
次に、各プロパティに対応して求められた同値クラスから、要因プロパティに対応する同値クラスを特定し、特定した同値クラス内の再帰変数を含む部分式（条件式）を抽出する。例えば、（在庫数（ａｆｔｅｒ）＝在庫数−数量）に対応する再帰変数（在庫数）を含む条件式は（数量＜＝在庫数−１０）になる。
【００２６】
次に、条件式を否定した否定条件式を作成する。例えば、条件式（数量＜＝在庫数−１０）の否定条件式は（在庫数−１０＜数量）になる。
その後、否定条件式と要因式に基づいて要因変数に関する繰り返し停止条件を算出する。算出した否定条件式に対して、再帰的変数部分に要因式を代入することで、要因変数に関する繰り返し停止条件を求める。例えば、あるプロパティに対して再帰的処理（繰り返し同じ処理）が実行されるような場合に、繰り返し同じ処理が続かないように、該プロパティが満たされない条件を求める。
【００２７】
例えば、否定条件式が（在庫数−１０＜数量）の場合、“在庫数”に要因式の“在庫数（ａｆｔｅｒ）”を代入し、（在庫数−数量）−１０＜数量を生成する。さらに、この（在庫数−数量）−１０＜数量を、数量に関して変形して繰り返し停止条件となる数量＞（在庫数-１０／２）を生成する。その後、繰り返し停止条件を記録部に記録する。
【００２８】
（最適化同値クラス生成処理）
最適化同値クラス生成部４は、条件式と繰り返し停止条件との論理積を作成して要因変数に関する条件式を再構築し、再構築した該条件式に前記要因変数以外の変数に関する条件式を加えた最適化同値クラスを生成する。
【００２９】
最適化同値クラスは、要因変数に対する元の同値クラスを狭め、要因プロパティが１度満された後、２度目の同じ要因プロパティを満たされないようにするものである。
例えば、条件式（数量＜＝在庫数−１０）と繰り返し停止条件と数量＞（在庫数-１０／２）に基づいて（在庫数-１０／２）＜数量＜＝在庫数−１０を生成する。図２のＰ１のプロパティの場合であれば、次のような最適化同値クラス１０が生成される。
（（在庫数-１０／２）＜数量＜＝在庫数−１０）ａｎｄ（顧客コード！＝ｎｕｌｌ）
【００３０】
図３に、図２に示したプロパティＰ１〜Ｐ３に対する同値クラスと最適化同値クラスのモデル検査の比較結果を示す。
プロパティＰ１の場合には、同値クラスのＣ１は０＜数量≦９０、Ｃ２は９０＜数量≦１００、Ｃ３は１００＜数量である。代表値のＣ１が数量＝１、Ｃ２が数量＝１００、Ｃ３が数量＝１０１である。よって、同値クラスの場合、８９回の購入処理が繰り返される。つまり、既存の境界値分析をもとに作成された代表値から状態空間を作成すると、代表値の取り方に依存して、イベントが起こっても同様の局面を表わすサブグラフが複数繰り返して出現する（充足するプロパティの集合が変化しない状態が続く）。
【００３１】
しかし、最適化同値クラスを用いると、（（在庫数-１０／２）＜数量＜＝在庫数−１０）ａｎｄ（顧客コード！＝ｎｕｌｌ）により、４５＜数量＜＝９０の代表値が数量＝４６となるので１回の処理で状態が収束することがわかる。
【００３２】
つまり、擬似システムのプロパティから繰り返しの要因となる再帰変数を抽出し、当該再帰変数による繰り返し（サブグラフ）を停止させる条件を加味した最適化した同値クラスを生成することにより、本来検査すべき場合分けを保ちつつ、無駄な繰り返しを減少させることができる。
【００３３】
（実施例２）
図４は、データ生成装置１の詳細な構成を示す図である。
データ生成装置１の繰り返し要因特定部２は、要因式抽出部４１、要因変数抽出部４２を備えている。
データ生成装置１の繰り返し停止条件抽出部３は、要因変数条件式抽出部４３、停止条件抽出部４４を備えている。
【００３４】
また、データ生成装置１は、記録部として帰結式格納部４５（帰結式テーブル）、要因格納部４６（要因テーブル）、停止条件格納部４７（停止条件テーブル）、プロパティ格納部４８（プロパティテーブル）、同値クラス格納部４９（同値クラステーブル）を備えている。
【００３５】
要因式抽出部４１は要因式を抽出する。プロパティ格納部４８（プロパティテーブル）に記録されている擬似システムのモデル検査に用いるプロパティから帰結部を抽出し、帰結部を構成する部分式が予め決められた再帰的定義により記述されているかを判定する。そして、予め決められた式で記述されていれば要因式を抽出し、要因格納部４６（要因テーブル）に記録する。さらに、該要因式に含まれる再帰的な変数を特定し再帰変数を要因格納部４６（要因テーブル）に記録する。
【００３６】
要因変数抽出部４２は、要因式と再帰変数に基づいて、要因式に含まれる繰り返しの要因となる要因変数を抽出し、要因変数を要因格納部４６（要因テーブル）に記録する。
要因変数条件式抽出部４３は、同値クラス格納部４９（同値クラステーブル）要因式を含む要因プロパティに対応する同値クラスから再帰変数を含む部分式（制約式）を抽出する。
【００３７】
停止条件抽出部４４は、抽出した部分式（制約式）である条件式を否定した否定条件式を作成し、否定条件式と要因式に基づいて要因変数に関する繰り返し停止条件を算出し、繰り返し停止条件を停止条件格納部４７（停止条件テーブル）に記録する。
【００３８】
帰結式格納部４５は、後述する帰結式テーブルを有している（図７）。要因格納部４６は、後述する要因テーブルを有している（図７）。停止条件格納部４７は、後述する停止条件テーブルを有している（図８）。プロパティ格納部４８は、図５に示すプロパティテーブルを有している。同値クラス格納部４９は、図５に示す同値クラステーブルを有している。
【００３９】
図５は、プロパティテーブルと同値クラステーブルの構造を示す図である。
プロパティテーブルは、「プロパティＩＤ」「プロパティ式」を有している。「プロパティＩＤ」にはプロパティを識別するために付される識別番号が記録されている。図５の例ではＰ１〜Ｐ３が記録されている。「プロパティ式」には、識別番号に関連付けられたプロパティ（条件部→帰結部：プロパティ式）が記録されている。図５の例では、Ｐ１に（１０＜＝在庫数−数量）ａｎｄ（顧客コード！＝ｎｕｌｌ）→（メッセージ＝＝ｎｕｌｌ）ａｎｄ（在庫数（ａｆｔｅｒ）＝＝在庫数−数量）が連付けられている。同様に、Ｐ２、Ｐ３にもプロパティが関連付けられている。
【００４０】
同値クラステーブルは、「同値クラスＩＤ」「プロパティＩＤ」「制約式」を有している。「同値クラスＩＤ」には、プロパティＩＤに対応する同値クラスの識別番号が記録されている。図５の例ではＣ１〜Ｃ３が記録されている。「制約式」には、同値クラスＩＤに関連付けられた制約式が記録されている。図５の例では、Ｃ１に（０＜数量＜＝在庫数−１０）ＡＮＤ（顧客コード！＝ｎｕｌｌ）が連付けられている。同様に、Ｃ２、Ｃ３に
も制約式が関連付けられている。
【００４１】
図６は、データ生成装置１の動作を示すフロー図である。
ステップＳ１では、プロパティテーブル内に処理すべきプロパティが残っているかを判定する。繰り返し要因特定部２が備える制御機能により、プロパティテーブルに記録されている全てのプロパティ式について、ステップＳ２の処理をしたかを判定して、全ての処理が完了していればステップＳ３に移行し、まだ処理すべきプロパティが残っていればステップＳ２に移行する。図５の例では、Ｐ１〜Ｐ３間での処理がされたか否かを判定する。
【００４２】
ステップＳ２では、要因式抽出部４１が該当プロパティの帰結部分を帰結式テーブルに設定する。
帰結式テーブルは、図７に示すように「帰結ＩＤ」「プロパティＩＤ」「帰結式」を有している。「帰結ＩＤ」には、上記説明したプロパティＩＤに関連付けられた各プロパティの帰結部の識別番号が記録される。「帰結ＩＤ」には図７ではＰ１’〜 Ｐ３’が記録されている。「帰結式」は、上記説明した帰結ＩＤに関連付けられた各プロパティの帰結部が記録されている。図７ではＰ１’に関連付けられた帰結式（メッセージ＝ｎｕｌｌ）ａｎｄ（在庫数（ａｆｔｅｒ）＝在庫数−数量）が記録される。同様に、Ｐ２’Ｐ３’にも帰結式が関連付けられている。
【００４３】
ステップＳ３では、帰結式テーブル内に処理すべき式が残っているかを判定する。繰り返し要因特定部２が備える制御機能により、プロパティテーブルに記録されている全てのプロパティ式について、後述するステップＳ４〜Ｓ５の処理をしたかを判定して、全ての処理が完了していればステップＳ６に移行し、まだ処理すべきプロパティが残っていればステップＳ４に移行する。
【００４４】
ステップＳ４では、要因式抽出部４１が帰結式テーブルの該当帰結部に再帰的定義が含まれるかを判定する。再帰的定義が含まれていればステップＳ５に移行し、含まれていなければステップＳ６に移行する。例えば、要因式抽出部４１は、帰結式テーブルの該当帰結部に予め決められた形式ｖａｒ（ａｆｔｅｒ）＝ｏｐ（ｖａｒ，ｖａｒ’）のような再帰的な式で記載されている部分式があるかを判定する。ここで、ｏｐは２項演算子（例えば＋，−）であり、ｖａｒは再帰変数を示している。ｖａｒ（ａｆｔｅｒ）はｏｐ（ｖａｒ，ｖａｒ’）の演算後の値であることを示している。
【００４５】
図７の帰結式テーブルのＰ１’に関連付けられた帰結式の場合であれば、部分式（在庫数（ａｆｔｅｒ）＝在庫数−数量）が再帰的な式で表されていることがわかる。つまり、在庫数が再帰変数（ｖａｒ）であり、在庫数を含む部分式を要因式（再帰的な式）として特定する。また、要因式を含むプロパティを特に要因プロパティと呼ぶ。
【００４６】
次に、要因変数抽出部４２が要因テーブルの要因式と再帰変数に基づいて、要因式に含まれる繰り返しの要因となる要因変数を特定する。要因変数の特定は、上記ｖａｒ（ａｆｔｅｒ）＝ｏｐ（ｖａｒ，ｖａｒ’）のｖａｒ’に相当する変数である。図７のＰ１のプロパティの場合であれば、要因変数は、要因式（在庫数（ａｆｔｅｒ）＝在庫数−数量）の数量に相当する。
【００４７】
ステップＳ５では、要因式抽出部４１と要因変数抽出部４２が特定した要因式、再帰変数、要因変数を、要因式抽出部４１と要因変数抽出部４２が要因テーブルに記録する。
要因テーブルは、「要因ＩＤ」「要因プロパティ」「要因式」「要因変数」「再帰変数」を有している。「要因ＩＤ」は要因式に関連付けられた識別番号であり、要因式を含むプロパティにも関連付けられている。図７の要因テーブルの場合であればＦ１が記録されている。「要因プロパティ」には要因式を含むプロパティの識別番号が記録される。図７の要因テーブルの場合であればＰ１が記録される。「要因式」には、要因式が記録されている。図７の要因テーブルの場合であれば、Ｆ１とＰ１に要因式（在庫数（ａｆｔｅｒ）＝在庫数−数量）が関連付けられて記録される。また、「要因変数」と「再帰変数」には、該当する要因式に関連する要因変数と再帰変数が記録される。図７の要因テーブルの場合であれば数量と在庫数がＦ１とＰ１に関連付けられて記録される。
【００４８】
ステップＳ６では、要因テーブル内に処理すべき要因式が残っているかを判定する。繰り返し停止条件抽出部３が備える制御機能により、要因テーブルに記録されている全ての要因式について、後述するステップＳ７の処理をしたかを判定して、全ての処理が完了していればステップＳ８に移行し、まだ処理すべき要因式が残っていればステップＳ６に移行する。
【００４９】
ステップＳ７では、要因変数条件式抽出部４３が、該当要因式の要因プロパティに対応する同値クラス内の要因変数に対応する条件式（制約式）を抽出し、停止条件テーブルに記録する。
【００５０】
停止条件テーブルは、「停止条件ＩＤ」「元同値クラス」「元制約式」「停止条件」を有している。「停止条件ＩＤ」には、要因プロパティに対応する同値クラスの識別番号Ｃ１に関連付けられた識別番号が記録される。図８の場合であればＳ１が記録される。「元同値クラス」には、要因プロパティに対応する同値クラスの識別番号が記録されている。図８の場合であればＣ１が記録される。「元制約式」には、同値クラステーブルに記録された制約式の要因変数と再帰変数に関連する部分式が記録される。
【００５１】
図８のＳ１の例であれば、図５の制約式（０＜数量＜＝在庫数−１０）ＡＮＤ（顧客コード！＝ｎｕｌｌ）を特定し、要因変数と再帰変数を含む部分式を特定する。本例では、部分式（０＜数量＜＝在庫数−１０）が特定され、（０＜数量＜＝在庫数−１０）は同値クラステーブルの制約式としてＳ１に関連付けて記録される。
【００５２】
ステップＳ８では、停止条件テーブル内に処理すべき停止条件が残っているかを判定する。繰り返し停止条件抽出部３が備える制御機能により、停止条件テーブルに記録されている全ての停止条件について、後述するステップＳ９〜Ｓ１０の処理をしたかを判定して、全ての処理が完了していればステップＳ１１に移行し、まだ処理すべきプロパティが残っていればステップＳ９に移行する。
【００５３】
ステップＳ９では、停止条件抽出部４４が、該当停止条件の元制約式の否定を作成する。条件式を否定した否定条件式を作成する。例えば、条件式（制約式）（数量＜＝在庫数−１０）の否定条件式は（在庫数−１０＜数量）になる。
【００５４】
ステップＳ１０では、停止条件抽出部４４が、作成した否定式内の再帰的変数部分に該当要因式を代入した式を、停止条件テーブルに記録する。算出した否定条件式に対して、再帰的変数部分に要因式を代入することで、要因変数に関する繰り返し停止条件を求める。
【００５５】
例えば、否定条件式が（在庫数−１０＜数量）の場合、“在庫数”に要因式の“在庫数（ａｆｔｅｒ）”を代入し、（在庫数−数量）−１０＜数量を生成する。さらに、この（在庫数−数量）−１０＜数量を、数量に関して変形して繰り返し停止条件となる数量＞（在庫数-１０／２）を生成する。その後、繰り返し停止条件を停止条件テーブルに記録する。
【００５６】
ステップＳ１１では、停止条件テーブル内に処理すべき停止条件が残っているかを判定する。最適化同値クラス生成部４が備える制御機能により、停止条件テーブルに記録されている全てのプロパティ式について、後述するステップＳ１２〜Ｓ１３の処理をしたかを判定して、全ての処理が完了していればＥＮＤに移行し、まだ処理すべき停止条件が残っていればステップＳ１２に移行する。
【００５７】
ステップＳ１２では、最適化同値クラス生成部４は、停止条件テーブルの元制約式と停止条件の論理積を作成する。例えば、停止条件テーブルの元制約式（数量＜＝在庫数−１０）と停止条件と数量＞（在庫数-１０／２）に基づいて（在庫数-１０／２）＜数量＜＝在庫数−１０を生成する。図２のＰ１のプロパティの場合であれば、次のような最適化同値クラスが生成される。
（（在庫数-１０／２）＜数量＜＝在庫数−１０）ａｎｄ（顧客コード！＝ｎｕｌｌ）
【００５８】
ステップＳ１３では、作成した論理積を図９に示すように同値クラステーブル内の対応する制約式に記録する。このとき現在の同値クラスに該論理積を上書きしてもよい。
【００５９】
上記のように境界値分析後に上記実施例を適用することで、検査の観点（プロパティ群がきちんと検査されるという観点）において、必要かつ十分な状態空間（漏れ・無駄のない空間）を生成するドライバが生成される。モデル検査では一般的に容易に状態爆発を起こすため、特に無駄（繰り返し構造）を排除した状態空間は、探索時間の削減に大きく貢献するものであり、モデル検査技術の適用可能性を拡大する効果がある。
【００６０】
（本発明の実施形態がコンピュータプログラムとして実現される場合の構成）
図１０は、上記本発明の実施形態の装置を実現できるコンピュータのハードウェア構成の一例を示す図である。
【００６１】
コンピュータのハードウェア１００は、ＣＰＵ１０１、記録部１０２（ＲＯＭ、ＲＡＭ、ハードディスクドライブなど）、記録媒体読取装置１０３、入出力インタフェース１０４（入出力Ｉ／Ｆ）、通信インタフェース１０５（通信Ｉ／Ｆ）などを備えている。また、上記各構成部はバス１０６によってそれぞれ接続されている。
【００６２】
ＣＰＵ１０１は、記録部１０２に格納されている上記説明した繰り返し要因特定処理、繰り返し停止条件抽出処理、最適化同値クラス生成処理を入力データに応じて実行する。
記録部１０２は、ＣＰＵ１０１が実行するプログラムやデータが記録されている。また、帰結式格納部４５、要因格納部４６、停止条件格納部４７、プロパティ格納部４８、同値クラス格納部４９を有している。また、ワークエリアなどとして使用される。
【００６３】
記録媒体読取装置１０３は、ＣＰＵ１０１の制御にしたがって記録媒体１０３ａに対するデータのリード／ライトを制御する。そして、記録媒体１０３ａ、記録媒体読取装置１０３の制御で書き込まれたデータを記憶したり、記録媒体１０３ａに記憶されたデータを読み取らせたりする。また、着脱可能な記録媒体１０３ａは、コンピュータで読み取り可能な記録媒体として、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記録装置には、ハードディスク装置（ＨＤＤ）などがある。光ディスクには、ＤＶＤ(Digital Versatile Disc)、ＤＶＤ−ＲＡＭ(Random Access Memory)、ＣＤ−ＲＯＭ(Compact Disc Read Only Memory)、ＣＤ−Ｒ(Recordable)／ＲＷ(ReWritable)などがある。光磁気記録媒体には、ＭＯ(Magneto-Optical disk)などがある。
【００６４】
入出力インタフェース１０４には、入出力装置１０４ａ（マウス、キーボード、ディスプレイなど）が接続され、ユーザが入力した情報を受信し、バス１０６を介してＣＰＵ１０１に送信する。また、ＣＰＵ１０１からの命令に従ってディスプレイの画面上に操作情報などを表示する。
【００６５】
通信インタフェース１０５は、必要に応じ、他のコンピュータとの間のＬＡＮ接続やインターネット接続や無線接続のためのインタフェースである。また、他の装置に接続され、外部装置からのデータの入出力を制御する。
【００６６】
このようなハードウェア構成を有するコンピュータを１台または２台以上用いることによって、上記説明した各種処理機能（実施例で説明した処理（フローチャートなど））が実現される。その場合システムが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体１０３ａに記録しておくことができる。
【００６７】
プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭなどの可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【００６８】
プログラムを実行するコンピュータは、例えば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。
【００６９】
また、本発明は、上記実施の形態に限定されるものでなく、本発明の要旨を逸脱しない範囲内で種々の改良、変更が可能である。
【００７０】
以上実施例を含む実施形態に関し、更に以下の付記を開示する。
（付記１）
コンピュータに、
記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出し、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、前記形式で記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定する繰り返し要因特定処理と、
前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出し、抽出した部分式である条件式を否定した否定条件式を作成し、前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出する繰り返し停止条件抽出処理と、
前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する最適化同値クラス生成処理と、
を実行させることを特徴とするデータ生成プログラム。
（付記２）
最適化同値クラス生成処理は、
前記条件式と前記繰り返し停止条件との論理積を作成して要因変数に関する条件式を再構築し、再構築した該条件式に前記要因変数以外の変数に関する条件式を加えた最適化同値クラスを生成することを特徴とする付記１に記載のデータ生成プログラム。
（付記３）
記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成
されるプロパティから帰結部を抽出し、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、前記形式で記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定する繰り返し要因特定部と、
前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出し、抽出した部分式である条件式を否定した否定条件式を作成し、前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出する繰り返し停止条件抽出部と、
前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する最適化同値クラス生成部と、
を備えることを特徴とするデータ生成装置、
（付記４）
記録部に記録されている擬似システムのモデル検査に用いる条件部と帰結部により構成されるプロパティから帰結部を抽出し、前記帰結部を構成する部分式が予め決められた再帰的定義により記述されているか判定し、
前記予め決められた形式で記述されていれば要因式と特定するとともに、該要因式に含まれる再帰的な変数を特定し再帰変数とし、
前記要因式と前記再帰変数に基づいて、前記要因式に含まれる繰り返しの要因となる要因変数を特定し、
前記要因式を含む要因プロパティに対応する同値クラスから前記再帰変数を含む部分式を抽出し、
前記抽出した部分式である条件式を否定した否定条件式を作成し、
前記否定条件式と前記要因式に基づいて前記要因変数に関する繰り返し停止条件を算出し、
前記条件式および前記繰り返し停止条件に基づいて最適化同値クラスを生成して前記記録部に記録する、
ことを特徴とするデータ生成方法。
（付記５）
最適化同値クラス生成部は、
前記条件式と前記繰り返し停止条件との論理積を作成して要因変数に関する条件式を再構築し、再構築した該条件式に前記要因変数以外の変数に関する条件式を加えた最適化同値クラスを生成することを特徴とする付記３に記載のデータ生成装置。
（付記６）
前記条件式と前記繰り返し停止条件との論理積を作成して要因変数に関する条件式を再構築し、再構築した該条件式に前記要因変数以外の変数に関する条件式を加えた最適化同値クラスを生成することを特徴とする付記４に記載のデータ生成方法。
【符号の説明】
【００７１】
１      データ生成装置、
２      繰り返し要因特定部、
３      繰り返し停止条件抽出部、
４      最適化同値クラス生成部、
５      要因式・要因変数、
６      繰り返し停止条件、
７      境界値分析装置、
８      プロパティ、
９      プロパティ・同値クラス、
１０      最適化同値クラス、
４１      要因式抽出部、
４２      要因変数抽出部、
４３      要因変数条件式抽出部、
４４      停止条件抽出部、
４５      帰結式格納部、
４６      要因格納部、
４７      停止条件格納部、
４８      プロパティ格納部、
４９      同値クラス格納部、
【図２】
2010191507.tif 000003
【図３】
2010191507.tif 000004
【図４】
2010191507.tif 000005
【図５】
2010191507.tif 000006
【図６】
2010191507.tif 000007
【図７】
2010191507.tif 000008
【図８】
2010191507.tif 000009
【図９】
2010191507.tif 000010
【図１０】
2010191507.tif 000011
【図１１】
2010191507.tif 000012
【図１】
2010191507.tif 000013