(57)【要約】  テストで利用する情報であるテスト情報を格納し得るテスト情報格納部と、対象の仕様について記述する言語である仕様記述言語で記述された対象の仕様に関する情報であり、１以上の変数の宣言を含む情報であり、テスト情報を生成するためのテスト元情報を含む情報である仕様記述情報を格納し得る仕様記述情報格納部と、変数の宣言およびテスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得部と、テスト情報取得部が取得した１以上のテスト情報をテスト情報格納部に蓄積するテスト情報蓄積部とを具備するテスト仕様生成装置により、対象の設計時にテスト設計のための情報を記載すれば、適切なテスト仕様に関する情報が自動生成できる。
2012128120.tif 000002
【特許請求の範囲】
【請求項１】
テストで利用する情報であるテスト情報を格納し得るテスト情報格納部と、
対象の仕様について記述する言語である仕様記述言語で記述された前記対象の仕様に関する情報であり、１以上の変数の宣言を含む情報であり、テスト情報を生成するためのテスト元情報を含む情報である仕様記述情報を格納し得る仕様記述情報格納部と、
前記変数の宣言および前記テスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得部と、
前記テスト情報取得部が取得した１以上のテスト情報を前記テスト情報格納部に蓄積するテスト情報蓄積部とを具備するテスト仕様生成装置。
【請求項２】
前記変数は、型を有し、
前記仕様記述情報は、
前記１以上の変数のうち、１以上の各変数に対応付けて、各変数が採り得る値の中で、テストで使用する値を特定する情報であるテスト元情報を有し、
前記テスト情報取得部は、
前記仕様記述情報から、前記テスト元情報を前記変数と対応付けて取得するテスト元情報取得手段と、
前記仕様記述情報から、テスト元情報を有さない変数と当該変数の型を取得する変数情報取得手段と、
前記テスト情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値を変数ごとに取得し、かつ、前記変数情報取得手段が取得した変数と当該変数の型から入力値を変数ごとに取得するテスト情報取得手段とを具備する請求項１記載のテスト仕様生成装置。
【請求項３】
前記テスト情報取得手段は、
前記テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、前記変数情報取得手段が取得した変数と当該変数の型から入力値および出力値を変数ごとに取得する請求項２記載のテスト仕様生成装置。
【請求項４】
前記仕様記述情報は、
１以上の変数の宣言、および制約に関する記述である１以上の制約情報を有し、
前記テスト情報取得手段は、
前記テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、前記変数情報取得手段が取得した変数と当該変数の型から入力値および出力値を変数ごとに取得し、かつ、前記すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する請求項３記載のテスト仕様生成装置。
【請求項５】
前記制約情報は、１以上の変数の値の集合を有する状態である遷移前状態と当該遷移前状態に対して発生するイベントと前記状態の場合に前記イベントが発生した場合に移行する状態である遷移後状態と明示的にイベントを発生させるアクションとを有する状態遷移情報、または１以上の変数の値の集合を有する第一状態と当該第一状態の場合に必ず採用される１以上の変数の値の集合を有する第二状態とを有する不変条件情報である請求項４記載のテスト仕様生成装置。
【請求項６】
前記テスト情報取得手段は、
前記１以上の制約情報が有する遷移前状態とイベントとの組である１以上の前提情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する請求項５記載のテスト仕様生成装置。
【請求項７】
前記テスト情報取得部は、
イベントに関する制約を示す１以上のイベント制約情報を格納し得るイベント制約情報格納手段をさらに具備し、
前記テスト情報取得手段は、
前記１以上のイベント制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する請求項５記載のテスト仕様生成装置。
【請求項８】
前記テスト情報取得手段は、
既に取得したテストスイートに対応する制約情報から、当該制約情報が有する遷移前状態とイベントに関する情報を削除し、かつ、当該遷移前状態以外の当該制約情報が有する部分の論理否定を構成した１以上の第二制約情報を取得し、当該１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する請求項５記載のテスト仕様生成装置。
【請求項９】
前記テスト情報取得手段は、
前記１以上の各制約情報から、各制約情報が有する遷移後状態を削除し、かつ、前記各制約情報が有する部分であり、当該遷移後状態以外の部分の論理否定を構成した１以上の第二制約情報を取得し、当該１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する請求項５記載のテスト仕様生成装置。
【請求項１０】
記憶媒体に、
テストで利用する情報であるテスト情報と、
対象の仕様について記述する言語である仕様記述言語で記述された前記対象の仕様に関する情報であり、１以上の変数の宣言を含む情報であり、テスト情報を生成するためのテスト元情報を含む情報である仕様記述情報を格納しており、
テスト情報取得部、およびテスト情報蓄積部により実現され得るテスト仕様生成方法であって、
前記テスト情報取得部が、前記変数の宣言および前記テスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得ステップと、
前記テスト情報蓄積部が、前記テスト情報取得ステップで取得された１以上のテスト情報を前記テスト情報格納部に蓄積するテスト情報蓄積ステップとを具備するテスト仕様生成方法。
【請求項１１】
記憶媒体に、
テストで利用する情報であるテスト情報と、
対象の仕様について記述する言語である仕様記述言語で記述された前記対象の仕様に関する情報であり、１以上の変数の宣言を含む情報であり、テスト情報を生成するためのテスト元情報を含む情報である仕様記述情報を格納しており、
コンピュータを、
前記変数の宣言および前記テスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得部と、
前記テスト情報取得部が取得した１以上のテスト情報を前記テスト情報格納部に蓄積するテスト情報蓄積部として機能させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、仕様記述言語で記述された仕様記述情報から、テスト仕様を生成するテスト仕様生成装置等に関するものである。
【背景技術】
【０００２】
従来、UMLのような自然文を含む仕様記述言語による仕様記述において、自然言語の特性から来る作成効率、品質の問題を改善する仕様記述支援方法があった（例えば、特許文献１参照）。かかる仕様記述支援方法において、変更可能部分と変更不能部分とで構成される自然文のテンプレートからひとつを選択し、テンプレートの変更可能部分に用語の入力を行う。また、本仕様記述支援方法において、用語の辞書を有し、未登録の用語について、用語の登録を促すことを特徴とする。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００８−１５８７９号公報（第１頁、第１図等）
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、従来技術において、設計段階での仕様記述の支援は行えても、テスト工程の支援は不十分で、テスト設計のために多大な労力を要していた。
【課題を解決するための手段】
【０００５】
本第一の発明のテスト仕様生成装置は、テストで利用する情報であるテスト情報を格納し得るテスト情報格納部と、対象の仕様について記述する言語である仕様記述言語で記述された対象の仕様に関する情報であり、１以上の変数の宣言を含む情報であり、テスト情報を生成するためのテスト元情報を含む情報である仕様記述情報を格納し得る仕様記述情報格納部と、変数の宣言およびテスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得部と、テスト情報取得部が取得した１以上のテスト情報をテスト情報格納部に蓄積するテスト情報蓄積部とを具備するテスト仕様生成装置である。【０００６】
かかる構成により、対象の設計時に仕様に関する情報を形式的に記載すれば、適切なテスト仕様に関する情報が自動生成できる。【０００７】
また、本第二の発明のテスト仕様生成装置は、第一の発明に対して、変数は、型を有し、仕様記述情報は、１以上の変数のうち、１以上の各変数に対応付けて、各変数が採り得る値の中で、テストで使用する値を特定する情報であるテスト元情報を有し、テスト情報取得部は、仕様記述情報から、テスト元情報を変数と対応付けて取得するテスト元情報取得手段と、仕様記述情報から、テスト元情報を有さない変数と変数の型を取得する変数情報取得手段と、テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値を変数ごとに取得し、かつ、変数情報取得手段が取得した変数と変数の型から入力値を変数ごとに取得するテスト情報取得手段とを具備するテスト仕様生成装置である。【０００８】
かかる構成により、対象の設計時に、形式的に記載された仕様の中で、変数に対応付けてテストで使用する値を特定すれば、適切なテスト仕様に関する情報が自動生成できる。【０００９】
また、本第三の発明のテスト仕様生成装置は、第二の発明に対して、テスト情報取得手段は、テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、変数情報取得手段が取得した変数と変数の型から入力値および出力値を変数ごとに取得するテスト仕様生成装置である。【００１０】
かかる構成により、対象の設計時に、形式的に記載された仕様の中で、変数に対応付けてテストで使用する値を特定すれば、適切なテストスイートが自動生成できる。【００１１】
また、本第四の発明のテスト仕様生成装置は、第三の発明に対して、仕様記述情報は、１以上の変数の宣言、および制約に関する記述である１以上の制約情報を有し、テスト情報取得手段は、テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、変数情報取得手段が取得した変数と変数の型から入力値および出力値を変数ごとに取得し、かつ、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するテスト仕様生成装置である。【００１２】
かかる構成により、対象の設計時に、形式的に記載された仕様の中で、変数に対応付けてテストで使用する値を特定すれば、適切なテストスイートが自動生成できる。【００１３】
また、本第五の発明のテスト仕様生成装置は、第四の発明に対して、制約情報は、１以上の変数の値の集合を有する状態である遷移前状態と、遷移前状態に対して発生するイベントと、遷移前状態の場合にイベントが発生した場合に移行する状態である遷移後状態とを有する状態遷移情報、または１以上の変数の値の集合を有する第一状態と第一状態の場合に必ず採用される１以上の変数の値の集合を有する第二状態とを有する不変条件情報であるテスト仕様生成装置である。【００１４】
かかる構成により、対象の設計時に、形式的に記載された仕様の中で、変数に対応付けてテストで使用する値を特定すれば、適切なテストスイートが自動生成できる。【００１５】
また、本第六の発明のテスト仕様生成装置は、第五の発明に対して、テスト情報取得手段は、１以上の制約情報が有する遷移前状態とイベントとの組である１以上の前提情報をも制約情報として用いて、すべての制約情報を満たすような、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するテスト仕様生成装置である。【００１６】
かかる構成により、状態遷移の前提条件を満たさないテストスイートの生成を防止できる。【００１７】
また、本第七の発明のテスト仕様生成装置は、第五の発明に対して、テスト情報取得部は、イベントに関する制約を示す１以上のイベント制約情報を格納し得るイベント制約情報格納手段をさらに具備し、テスト情報取得手段は、１以上のイベント制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するテスト仕様生成装置である。【００１８】
かかる構成により、指定したイベントを含むテストスイートの生成を防止できる。【００１９】
また、本第八の発明のテスト仕様生成装置は、第五の発明に対して、テスト情報取得手段は、既に取得したテストスイートに対応する情報から、遷移前状態の情報を削除し、かつ、遷移前状態以外の情報が有する部分の論理否定を構成した１以上の第二制約情報を取得し、１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するテスト仕様生成装置である。【００２０】
かかる構成により、遷移後状態として既知のものを持つテストスイートの生成を防止できる。【００２１】
また、本第九の発明のテスト仕様生成装置は、第五の発明に対して、テスト情報取得手段は、既に取得したテストスイートに対応する情報から、遷移後状態の情報を削除し、かつ、遷移後状態以外の情報が有する部分の論理否定を構成した１以上の第二制約情報を取得し、１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するテスト仕様生成装置である。【００２２】
かかる構成により、遷移前状態として既知のものを持つテストスイートの生成を防止できる。
【発明の効果】
【００２３】
本発明によるテスト仕様生成装置によれば、対象の設計時に、形式的に記載された仕様の中で、テスト設計のための情報を記載すれば、適切なテスト仕様に関する情報が自動生成できる。
【図面の簡単な説明】
【００２４】
【図１】実施の形態１におけるテスト仕様生成装置のブロック図
【図２】同テスト仕様生成装置の動作について説明するフローチャート
【図３】同変数表取得処理について説明するフローチャート
【図４】同命題論理式取得処理について説明するフローチャート
【図５】同テスト情報取得処理について説明するフローチャート
【図６】同仕様記述情報を示す図
【図７】同変数表を示す図
【図８】同命題論理式の集合の例を示す図
【図９】同テスト情報取得手段が取得した数値列を示す図
【図１０】同テスト情報を示す図
【図１１】同テスト情報取得部の動作の概念について説明する図
【図１２】同テスト仕様生成装置の処理の流れを説明する図
【図１３】実施の形態２におけるテスト仕様生成装置２のブロック図
【図１４】同仕様記述情報を示す図
【図１５】同変数表を示す図
【図１６】同命題論理式の集合の例を示す図
【図１７】同テスト情報取得手段が取得した数値列を示す図
【図１８】同無用なテストスイートの抑制を図る動作を説明する図
【図１９】実施の形態１におけるコンピュータシステムの概観図
【図２０】同コンピュータシステムのブロック図
【発明を実施するための形態】
【００２５】
以下、テスト仕様生成装置等の実施形態について図面を参照して説明する。なお、実施の形態において同じ符号を付した構成要素は同様の動作を行うので、再度の説明を省略する場合がある。
【００２６】
（実施の形態１）
本実施の形態において、仕様記述言語で記述された仕様記述情報から、テスト仕様を生成する生成テスト仕様生成装置について説明する。なお、仕様記述言語は、通常、形式的な仕様記述言語であるが、その形式を問わない。仕様記述言語は、通常、ソフトウェアを設計・構築する際に、その仕様を記述するために用いられる言語であるが、ハードウェア記述言語でも良い。また、仕様記述言語で記述された仕様記述情報は、プログラムに自動変換されることは好適であるが、必ずしもプログラムに自動変換される必要はない。
【００２７】
図１は、本実施の形態におけるテスト仕様生成装置１のブロック図である。テスト仕様生成装置１は、テスト情報格納部１１、仕様記述情報格納部１２、受付部１３、テスト情報取得部１４、テスト情報蓄積部１５、およびテスト情報出力部１６を備える。
【００２８】
また、テスト情報取得部１４は、テスト元情報取得手段１４１、変数情報取得手段１４２、およびテスト情報取得手段１４３を備える。
【００２９】
テスト情報格納部１１は、テスト情報を格納し得る。テスト情報は、対象のテストで利用する情報である。対象とは、仕様記述の対象であり、通常、ソフトウェアであるが、ハードウェアでも良い。また、テスト情報とは、いわゆる１以上のテストケースでも良いし、いわゆる１以上のテストスイートでも良い。テストケースは、テストの際に対象に与える入力の情報（例えば、１以上の入力値）である。テストスイートは、テストの際に対象に与える入力の情報（例えば、１以上の入力値）と、入力の情報を与えた場合の出力の情報（例えば、１以上の出力値）の組である。テスト情報は、テストの実施に役立つ情報であれば良い。テスト情報は、自動テストのための情報でも良いし、手動でのテストで利用される情報でも良い。なお、出力の情報とは、対象の動作の結果である。
【００３０】
テスト情報格納部１１は、不揮発性の記録媒体が好適であるが、揮発性の記録媒体でも実現可能である。
【００３１】
仕様記述情報格納部１２は、仕様記述情報を格納し得る。仕様記述情報は、仕様記述言語で記述された対象の仕様に関する情報である。また、仕様記述情報は、通常、１以上の変数の宣言を含む情報である。また、仕様記述情報は、テスト情報を生成するためのテスト元情報を含む情報であることは好適である。仕様記述情報は、１以上（ｎ個）の変数のうち、１以上の各変数（ｍ個，ｎ＞＝ｍ）に対応付けて、各変数が採り得る値の中で、テストで使用する変数の値を特定する情報であるテスト元情報を有しても良い。つまり、テスト元情報は、テストで使用する１以上の値でも良いし、テストで使用する値の範囲（例えば、１〜１０、など）でも良いし、テストで使用しない１以上の値でも良いし、テストで使用しない値の範囲でも良いし、テストで使用する値の条件（例えば、偶数、３文字以内のアルファベットの組み合わせの文字列等）でも良いし、テストで使用しない値の条件（例えば、３で割り切れる自然数等）でも良い。
【００３２】
また、仕様記述情報は、１以上の変数の宣言、および制約に関する記述である１以上の制約情報を有することは好適である。制約情報は、例えば、状態遷移情報または不変条件情報であることは好適である。また、状態遷移情報とは、状態遷移に関する情報である。状態遷移情報は、遷移前状態とイベントと遷移後状態とアクションとを有することは好適である。状態遷移情報は、遷移前状態とイベントと遷移後状態とを有する情報であっても良い。遷移前状態は、イベントを受け付ける前の状態である。遷移前状態は、１以上の変数の値の集合を有する状態である。イベントは、遷移前状態に対して発生する。遷移後状態とは、遷移前状態の際にイベントが発生した場合に移行する状態である。遷移後状態は、１以上の変数の値の集合を有する状態である。アクションは、明示的に特定のイベントを発生させる。また、不変条件情報は、不変条件を示す。不変条件情報は、第一状態と第二状態とを有する。第一状態は、１以上の変数の値の集合を有する。第二状態は、第一状態の場合に必ず採用される１以上の変数の値の集合を有する。不変条件情報は、第一状態でも第二状態でも変わらず成立する条件を示す。また、ここで、変数は、通常、型を有する。型は、データタイプとも言う。型には、採り得る値や範囲が決まっている型もある。なお、仕様記述情報は、ファイルであることは好適であるが、そのデータ構造は問わない。
【００３３】
仕様記述情報格納部１２は、不揮発性の記録媒体が好適であるが、揮発性の記録媒体でも実現可能である。
【００３４】
仕様記述情報格納部１２に仕様記述情報が記憶される過程は問わない。例えば、記録媒体を介して仕様記述情報が仕様記述情報格納部１２で記憶されるようになってもよく、通信回線等を介して送信された仕様記述情報が仕様記述情報格納部１２で記憶されるようになってもよく、あるいは、入力デバイスを介して入力された仕様記述情報が仕様記述情報格納部１２で記憶されるようになってもよい。
【００３５】
受付部１３は、指示や情報を受け付ける。指示とは、例えば、テスト情報を生成する指示であるテスト情報生成指示である。また、指示とは、例えば、テスト情報を出力する指示であるテスト情報出力指示である。指示などの入力手段は、キーボードやマウスやメニュー画面によるもの等、何でも良い。受付部１３は、キーボード等の入力手段のデバイスドライバーや、メニュー画面の制御ソフトウェア等で実現され得る。
【００３６】
テスト情報取得部１４は、仕様記述情報が有する変数の宣言およびテスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得する。入力値とは、対象に与える値である。入力値は、変数の初期値や、設定値などでも良い。ここで、取得するとは、生成することも含む。また、取得するとは、記録媒体から読み出すことでも良い。
【００３７】
テスト情報取得部１４を構成するテスト元情報取得手段１４１は、仕様記述情報から、テスト元情報を変数と対応付けて取得する。テスト元情報取得手段１４１は、例えば、仕様記述情報に対して、字句解析および構文解析を行い、テスト元情報を変数と対応付けて取得する。また、テスト元情報取得手段１４１は、例えば、仕様記述情報に対して、予約語（例えば、”Var”、”testedwith”など）のパターンマッチング等を行い、テスト元情報を変数と対応付けて取得しても良い。つまり、テスト元情報取得手段１４１は、仕様記述情報から、予め決められた文字列（例えば、予約語）を用いて、テスト元情報を変数と対応付けて取得しても良い。
【００３８】
変数情報取得手段１４２は、仕様記述情報から、テスト元情報を有さない変数と当該変数の型を取得する。
【００３９】
テスト情報取得手段１４３は、テスト元情報取得手段１４１が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値を変数ごとに取得する。また、テスト情報取得手段１４３は、変数情報取得手段１４２が取得した変数と変数の型から入力値を変数ごとに取得する。
【００４０】
また、テスト情報取得手段１４３は、テスト元情報取得手段１４１が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得する。また、テスト情報取得手段１４３は、変数情報取得手段１４２が取得した変数と変数の型から入力値および出力値を変数ごとに取得しても良い。
【００４１】
また、テスト情報取得手段１４３は、テスト元情報取得手段１４１が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、すべての制約情報を満たすテストスイートを１以上取得する。また、テスト情報取得手段１４３は、変数情報取得手段１４２が取得した変数と変数の型から入力値および出力値を変数ごとに取得し、かつ、すべての制約情報を満たすテストスイートを１以上取得しても良い。
【００４２】
なお、テストスイートとは、１以上の入力値および１以上の出力値の組である。かかる場合、テスト情報取得手段１４３は、例えば、テスト元情報取得手段１４１が取得したテスト元情報と変数の型から、各変数の入力値の候補値を取得する。そして、テスト情報取得手段１４３は、１以上の各変数の入力値（状態遷移前の値）と出力値（状態遷移後の値）のすべての組み合わせを取得する。なお、この組み合わせがテストスイートの候補である。そして、テスト情報取得手段１４３は、テストスイートの候補を、すべての制約情報に適用し、すべての制約情報を満たすテストスイートを、利用するテストスイートとして抽出する。なお、１以上の制約情報が存在する場合に、当該１以上の制約情報に与える変数の値の組が、当該１以上の制約情報を満たすか否かを判断する処理は公知技術である。また、テスト情報取得手段１４３は、１以上のテストスイートの候補を取得してから、１以上の制約情報を１以上のテストスイートに適用して、制約情報を満たさないテストスイートを削除しても良い。また、テスト情報取得手段１４３は、テストスイートを取得する際に１以上の制約情報を適用しても良い。
【００４３】
また、制約情報とは、状態遷移情報または不変条件情報であることは好適である。状態遷移情報とは、１以上の変数の値の集合を有する状態である遷移前状態と遷移前状態に対して発生するイベントと遷移前状態の場合にイベントが発生した場合に移行する状態である遷移後状態とアクションとを有する情報である。また、不変条件情報は、１以上の変数の値の集合を有する第一状態と第一状態の場合に必ず採用される１以上の変数の値の集合を有する第二状態とを有する情報である。
【００４４】
テスト情報蓄積部１５は、テスト情報取得部１４が取得した１以上のテスト情報をテスト情報格納部１１に蓄積する。
【００４５】
テスト情報出力部１６は、テスト情報格納部１１のテスト情報を出力する。ここで、出力とは、ディスプレイへの表示、プロジェクターを用いた投影、プリンタへの印字、外部の装置への送信、記録媒体への蓄積、他の処理装置や他のプログラムなどへの処理結果の引渡しなどを含む概念である。テスト情報出力部１６は、ディスプレイ等の出力デバイスを含むと考えても含まないと考えても良い。テスト情報出力部１６は、出力デバイスのドライバーソフトまたは、出力デバイスのドライバーソフトと出力デバイス等で実現され得る。
【００４６】
テスト情報取得部１４、テスト元情報取得手段１４１、変数情報取得手段１４２、テスト情報取得手段１４３、およびテスト情報蓄積部１５は、通常、ＭＰＵやメモリ等から実現され得る。テスト情報取得部１４等の処理手順は、通常、ソフトウェアで実現され、当該ソフトウェアはＲＯＭ等の記録媒体に記録されている。但し、ハードウェア（専用回路）で実現しても良い。
【００４７】
次に、テスト仕様生成装置１の動作について、図２のフローチャートを用いて説明する。
【００４８】
（ステップＳ２０１）受付部１３は、テスト情報生成指示を受け付けたか否かを判断する。テスト情報生成指示を受け付ければステップＳ２０２に行き、テスト情報生成指示を受け付けなければステップＳ２０７に行く。
【００４９】
（ステップＳ２０２）テスト情報取得部１４は、仕様記述情報格納部１２から仕様記述情報を読み出す。
【００５０】
（ステップＳ２０３）テスト情報取得部１４は、仕様記述情報を解釈し、変数表を取得する。なお、仕様記述情報の解釈とは、通常、字句解析、構文解析等であり、プログラム言語の処置系（例えば、コンパイラやインタプリタ等）が行う公知の技術である。変数表を取得する変数表取得処理について、図３のフローチャートを用いて説明する。
【００５１】
（ステップＳ２０４）テスト情報取得部１４は、仕様記述情報を解釈し、命題論理式を取得する。命題論理式を取得する命題論理式取得処理について、図４のフローチャートを用いて説明する。ここでの仕様記述情報の解釈も、通常、字句解析、構文解析等であり、プログラム言語の処置系（例えば、コンパイラやインタプリタ等）が行う公知の技術である。
【００５２】
（ステップＳ２０５）テスト情報取得部１４は、変数表と命題論理式とを用いて、テスト情報を取得する。テスト情報を取得するテスト情報取得処理について、図５のフローチャートを用いて説明する。
【００５３】
（ステップＳ２０６）テスト情報蓄積部１５は、ステップＳ２０５で取得されたテスト情報を、テスト情報格納部１１に蓄積する。ステップＳ２０１に戻る。
【００５４】
（ステップＳ２０７）受付部１３は、テスト情報出力指示を受け付けたか否かを判断する。テスト情報出力指示を受け付ければステップＳ２０８に行き、テスト情報出力指示を受け付けなければステップＳ２０１に戻る。
【００５５】
（ステップＳ２０８）テスト情報出力部１６は、テスト情報格納部１１からテスト情報を読み出す。
【００５６】
（ステップＳ２０９）テスト情報出力部１６は、ステップＳ２０８で読み出したテスト情報を出力する。ステップＳ２０１に戻る。
【００５７】
なお、図２のフローチャートにおいて、電源オフや処理終了の割り込みにより処理は終了する。
【００５８】
次に、ステップＳ２０３の変数表取得処理について、図３のフローチャートを用いて説明する。
【００５９】
（ステップＳ３０１）変数情報取得手段１４２は、カウンタｉに１を代入する。
【００６０】
（ステップＳ３０２）変数情報取得手段１４２は、仕様記述情報からｉ番目の処理単位を読み出す。なお、一の処理単位とは、例えば、１行、一の終端子（例えば、“；”や予約語など）の次の文字列から次の終端子まで、特定の予約語の次の文字列から次の特定の予約語まで、などである。一の処理単位とは、変数の宣言か否かを判断する文字列の単位、または制約か否かを判断する文字列の単位等である。
【００６１】
（ステップＳ３０３）変数情報取得手段１４２は、ステップＳ３０３でｉ番目の処理単位を読み出せたか否かを判断する。ｉ番目の処理単位を読み出せればステップＳ３０４に行き、読み出せなければ上位処理にリターンする。
【００６２】
（ステップＳ３０４）変数情報取得手段１４２は、ｉ番目の処理単位が変数の宣言であるか否かを判断する。変数の宣言であればステップＳ３０５に行き、変数の宣言でなければステップＳ３１０に行く。なお、処理単位が変数の宣言であるか否かは、例えば、予約語”Var”を含む行か否か、予約語”Var”に続く非予約語であるか否か、変数のタイプ（予約語）を含む行か否か等により判断する。かかる処理単位が変数の宣言であるか否かを判断する処理も公知技術である。
【００６３】
（ステップＳ３０５）変数情報取得手段１４２は、ｉ番目の処理単位から変数の型を取得する。
【００６４】
（ステップＳ３０６）テスト元情報取得手段１４１は、ｉ番目の処理単位に、テスト元情報が存在するか否かを判断する。テスト元情報が存在すればステップＳ３０７に行き、テスト元情報が存在しなければステップＳ３１１に行く。テスト元情報が存在するか否かは、例えば、テスト元情報を特定する予約語（例えば、”testedwith”）を含むか否かにより行われる。
【００６５】
（ステップＳ３０７）テスト元情報取得手段１４１は、ｉ番目の処理単位からテスト元情報を取得する。なお、テスト元情報取得手段１４１は、例えば、テスト元情報を特定する予約語（例えば、”testedwith”）に対応するテスト元情報を取得する。
【００６６】
（ステップＳ３０８）変数情報取得手段１４２は、テスト元情報と型、またはテスト元情報を用いて、変数の１以上の入力値、または変数の１以上の入力値と変数の１以上の出力値を取得する。
【００６７】
（ステップＳ３０９）変数情報取得手段１４２は、変換表にレコードを追記する。レコードは、変数の１以上の入力値、または変数の１以上の入力値と変数の１以上の出力値を有する。
【００６８】
（ステップＳ３１０）変数情報取得手段１４２は、カウンタｉを１，インクリメントする。ステップＳ３０３に戻る。
【００６９】
（ステップＳ３１１）変数情報取得手段１４２は、型を用いて、変数の１以上の入力値、または変数の１以上の入力値と変数の１以上の出力値を取得する。ステップＳ３０９に行く。なお、変数情報取得手段１４２は、例えば、型と１以上の値との対応表を保持しており、かかる対応表を用いて、型から１以上の入力値、または１以上の入力値と１以上の出力値とを取得する。
【００７０】
なお、図３のフローチャートにおいて、例えば、デフォルトの変数の情報（例えば、後述する”null#true”など）からレコードを構成し、当該レコードを変数表に書き込んでも良い。かかる場合、変数情報取得手段１４２は、デフォルトの変数の情報を予め保持している。
【００７１】
次に、ステップＳ２０４の命題論理式取得処理について、図４のフローチャートを用いて説明する。
【００７２】
（ステップＳ４０１）テスト情報取得手段１４３は、カウンタｉに１を代入する。
【００７３】
（ステップＳ４０２）テスト情報取得手段１４３は、仕様記述情報からｉ番目の処理単位を読み出す。
【００７４】
（ステップＳ４０３）テスト情報取得手段１４３は、ステップＳ４０２でｉ番目の処理単位を読み出せたか否かを判断する。ｉ番目の処理単位を読み出せればステップＳ４０４に行き、読み出せなければ上位処理にリターンする。
【００７５】
（ステップＳ４０４）テスト情報取得手段１４３は、ｉ番目の処理単位が制約であるか否かを判断する。制約であればステップＳ４０５に行き、制約でなければステップＳ４０６に行く。なお、制約とは、仕様記述における、対象が満たさなければならない条件である。テスト情報取得手段１４３は、例えば、予約語（例えば、”Require”）に続く行であり、次の制約以外を示す予約語が出現するまでの行を、制約情報として判断する。ただし、制約情報の判断手法は問わない。
【００７６】
（ステップＳ４０５）テスト情報取得手段１４３は、ｉ番目の処理単位に対応する制約情報を、命題論理式に変換する。なお、制約情報を命題論理式に変換する技術は公知技術である。
【００７７】
（ステップＳ４０６）テスト情報取得手段１４３は、カウンタｉを１，インクリメントする。ステップＳ４０２に戻る。
【００７８】
次に、ステップＳ２０５のテスト情報取得処理について、図５のフローチャートを用いて説明する。
【００７９】
（ステップＳ５０１）テスト情報取得手段１４３は、カウンタｉに１を代入する。
【００８０】
（ステップＳ５０２）テスト情報取得手段１４３は、ｉ番目の入力値のセットを、変数表から取得する。テスト情報取得手段１４３は、１以上の各変数が入力値として採り得る値の中から、各変数の値を取得し、変数名と値の組を有する１以上の情報を取得する。この変数名と値の組を有する１以上の情報が、入力値のセットである。
【００８１】
（ステップＳ５０３）テスト情報取得手段１４３は、ステップＳ５０２でｉ番目の入力値のセットを取得できたか否かを判断する。ｉ番目の入力値のセットを取得できればステップＳ５０４に行き、取得できなければ上位処理にリターンする。
【００８２】
（ステップＳ５０４）テスト情報取得手段１４３は、カウンタｊに１を代入する。
【００８３】
（ステップＳ５０５）テスト情報取得手段１４３は、ｊ番目の出力値のセットを、変数表から取得する。テスト情報取得手段１４３は、１以上の各変数が出力値として採り得る値の中から、各変数の値を取得し、変数名と値の組を有する１以上の情報を取得する。この変数名と値の組を有する１以上の情報が、出力値のセットである。
【００８４】
（ステップＳ５０６）テスト情報取得手段１４３は、ステップＳ５０５でｊ番目の出力値のセットを取得できたか否かを判断する。ｊ番目の出力値のセットを取得できればステップＳ５０７に行き、取得できなければステップＳ５１６に行く。
【００８５】
（ステップＳ５０７）テスト情報取得手段１４３は、カウンタｋに１を代入する。
【００８６】
（ステップＳ５０８）テスト情報取得手段１４３は、ｋ番目の命題論理式を取得する。ここでの命題論理式は、ステップＳ２０４の命題論理式取得処理により取得された１以上の命題論理式の中のｋ番目の命題論理式である。
【００８７】
（ステップＳ５０９）テスト情報取得手段１４３は、ステップＳ５０８でｋ番目の命題論理式を取得できたか否かを判断する。ｋ番目の命題論理式を取得できればステップＳ５１０に行き、ｋ番目の命題論理式を取得できなければステップＳ５１３に行く。
【００８８】
（ステップＳ５１０）テスト情報取得手段１４３は、ｉ番目の入力値とｊ番目の出力値とを、ｋ番目の命題論理式に適用する。
【００８９】
（ステップＳ５１１）テスト情報取得手段１４３は、ｉ番目の入力値とｊ番目の出力値とが、ｋ番目の命題論理式を満たすか否かを判断する。ｋ番目の命題論理式を満たせばステップＳ５１２に行き、満たさなければステップＳ５１５に行く。
【００９０】
（ステップＳ５１２）テスト情報取得手段１４３は、カウンタｋを１，インクリメントする。ステップＳ５０８に戻る。
【００９１】
（ステップＳ５１３）テスト情報取得手段１４３は、ｉ番目の入力値とｊ番目の出力値とを有するテスト情報を構成する。
【００９２】
（ステップＳ５１４）テスト情報取得手段１４３は、ステップＳ５１３で構成したテスト情報を図示しないバッファに追記する。このバッファは、通常、一時的な記憶媒体である。
【００９３】
（ステップＳ５１５）テスト情報取得手段１４３は、カウンタｊを１，インクリメントする。ステップＳ５０５に戻る。
【００９４】
（ステップＳ５１６）テスト情報取得手段１４３は、カウンタｉを１，インクリメントする。ステップＳ５０２に戻る。
【００９５】
以下、本実施の形態におけるテスト仕様生成装置１の具体的な動作について説明する。
【００９６】
今、仕様記述情報格納部１２は、図６に示す仕様記述情報を格納している。図６において、（１）（２）は、変数の型の宣言である。（１）のデータの型“onoff_type”の変数は、値”ON”または”OFF”を採り得る。データの型“onoff_type”が値”ON”または”OFF”を採り得るという情報は、テスト仕様生成装置１が保持している。つまり、例えば、テスト仕様生成装置１は「onoff_type：on｜off」を保持している。また、（２）は、データの型”m_type”の初期値は”m”であることを示す。
【００９７】
また、図６において、（３）は、変数の宣言の例である。（３）において、テスト元情報の予約語”testedwith”により、テスト元情報｛off｝が存在することが分かる。テスト元情報｛off｝は、型“onoff_type”の変数”op”のテストの際に利用する値として、”off”のみであることを示す。つまり、このテスト元情報の記載により、仕様記述情報の作成者の、テストにおける意図が反映できる。なお、”op:onoff_type{off}”の”off”は、変数”op”の初期値が”off”であることを示す。
【００９８】
また、図６において、（４）も変数の宣言の例であるが、テスト元情報は有さない。そして、変数”lamp”の型は“onoff_type”であり、初期値は”off”である。かかる場合、変数”lamp”の値の中で、テストで利用する値は、変数”lamp”が採り得る値のすべて（ここでは、”on”と”off”）である。
【００９９】
また、図６の（５）は、型”m_type”の変数”ch”の宣言である。
【０１００】
また、図６の（６）（７）は、制約情報である。予約語“Function”、”Require”が、以降に続く文字列が制約情報であることを示す。また、（６）は、状態遷移情報である。（６）において、”op==on && lamp==off”は遷移前状態、”ch?m”はイベント、”lamp==on”は遷移後状態を示す。つまり、（６）は、”op==on && lamp==off”の場合に、イベント”ch?m”が発生すれば、”lamp==on”に状態が変化していなければならないという制約を示す。また、（７）は不変条件情報である。（７）において、”op==off -> lamp==off”は、”op==off”であれば、”lamp==off”であることを示す。つまり、”Ａ->Ｂ”は、「ＡならばＢ」であることを示す。
【０１０１】
かかる状況において、ユーザは、テスト仕様生成装置１に、テスト情報生成指示を入力した、とする。
【０１０２】
すると、受付部１３は、テスト情報生成指示を受け付ける。そして、テスト情報取得部１４は、仕様記述情報格納部１２から、図６の仕様記述情報を読み出す。
【０１０３】
次に、テスト情報取得部１４の変数情報取得手段１４２は、図６の仕様記述情報を解釈し、変数表を取得する。つまり、変数情報取得手段１４２は、まず、デフォルトの変数の情報”null#true”、”SubsystemCountUp#true”を、図示しない記録媒体（通常、変数情報取得手段１４２が保持する記録媒体）から取得する。そして、変数情報取得手段１４２は、取得した各変数の情報に変数の識別符号（以下、変数識別子という）を付してレコードを構成し、当該レコードを空の変数表に書き込む。なお、ここでは、変数識別子は、「１」から順次、インクリメントされる整数である、とする。つまり、変数情報取得手段１４２は、まず、レコード”１  null#true”、”２  SubsystemCountUp#true”を変数表に書き込む。
【０１０４】
次に、変数情報取得手段１４２は、図６の”Extern”、”Data onoff_type; // from main”、”Class B”、” Data m_type {m};”を順次、読み出し、変数の宣言ではない、と判断する。なお、ここでの処理単位は、例えば、行である、とする。
【０１０５】
次に、変数情報取得手段１４２は、図６の”Var op : onoff_type {off} testedwith {off};”を読み出す。そして、変数情報取得手段１４２は、予約語”Var”から、この処理単位が変数の宣言である、と判断する。なお、以降に続く処理単位に対して、変数ではない予約語が出現するまで、変数情報取得手段１４２は、変数の宣言であると判断する、とする。
【０１０６】
次に、変数情報取得手段１４２は、処理単位”Var op : onoff_type {off} testedwith {off};”から変数の型”onoff_type”を取得する。次に、テスト元情報取得手段１４１は、この処理単位からテスト元情報”testedwith{off}”を取得する。
【０１０７】
次に、変数情報取得手段１４２は、テスト元情報”testedwith{off}”を用いて、変数”op”の１以上の入力値、または変数の１以上の入力値と変数の１以上の出力値（次の状態の値）を取得する。つまり、変数情報取得手段１４２は、変数”op”の入力値”off”、および変数”op”の出力値”off”を取得する。つまり、テスト元情報”testedwith{off}”は、変数”op”のテストの値として利用されるのは”off”だけであり、”on”は利用されないことを示す。そして、変数情報取得手段１４２は、変数”op”の入力値”off”に変数識別子を付して、レコード”３  op#off”を構成する。なお、”３  op#off”のうちの” op#off”の前に”@”が存在しない場合、それは入力値であることを示す。入力値は、状態の遷移前の値である。また、変数情報取得手段１４２は、変数”op”の出力値”off”に変数識別子を付して、レコード”４  @op#off”を構成する。なお、”４  @op#off”のうちの”@”は出力値であることを示す。
【０１０８】
次に、変数情報取得手段１４２は、図６の”lamp :onoff_type {off};”を読み出す。そして、変数情報取得手段１４２は、この処理単位が変数の宣言である、と判断する。
【０１０９】
次に、変数情報取得手段１４２は、処理単位”lamp : onoff_type {off};”から変数の型”onoff_type”を取得する。次に、テスト元情報取得手段１４１は、この処理単位からテスト元情報を取得できない。
【０１１０】
次に、変数情報取得手段１４２は、型”onoff_type”を用いて、変数”lamp”の１以上の入力値{on，off}と変数”lamp”の１以上の出力値{on，off}を取得する。そして、変数情報取得手段１４２は、変数”lamp”の入力値”on”に変数識別子を付して、レコード”５  lamp#on”を構成する。また、変数情報取得手段１４２は、変数”lamp”の入力値”off”に変数識別子を付して、レコード”６  lamp#off”を構成する。また、変数情報取得手段１４２は、変数”lamp”の出力値”on”に変数識別子を付して、レコード”７  @lamp#on”を構成する。さらに、変数情報取得手段１４２は、変数”lamp”の出力値”off”に変数識別子を付して、レコード”８  @lamp#off”を構成する。そして、変数情報取得手段１４２は、これらのレコードを変換表に追記する。
【０１１１】
次に、変数情報取得手段１４２は、図６の”Channel ch : m_type;”を読み出す。そして、変数情報取得手段１４２は、予約語”Channel”から、この処理単位が変数の宣言である、と判断する。
【０１１２】
次に、変数情報取得手段１４２は、処理単位”Channel ch : m_type;”から変数の型” m_type”を取得する。次に、テスト元情報取得手段１４１は、この処理単位からテスト元情報を取得できない。
【０１１３】
次に、変数情報取得手段１４２は、型”m_type”を用いて、変数”ch”の入力値{m}を取得する。そして、変数情報取得手段１４２は、変数”ch”の入力値”m”に変数識別子を付して、レコード”９  ch?m”を構成する。そして、変数情報取得手段１４２は、変換表にこのレコードを追記する。なお、予約語”Channel”はイベントを示し、入力値のみ存在し、出力値が存在しないことは、予め変数情報取得手段１４２は知っている。
【０１１４】
以上の処理により、図７に示す変数表が得られた。変数表において、” c --- CNFNum to VarAssign table ---“、” c --- end ---“、および行頭の”c”は、ここでは重要な意味を持たない、とする。
【０１１５】
次に、テスト情報取得手段１４３は、図６の仕様記述情報を解釈し、以下のように命題論理式を取得する。
【０１１６】
つまり、テスト情報取得手段１４３は、例えば、処理単位”Var  op : onoff_type {off} testedwith{off};”を読み出し、当該処理単位から状態遷移前の命題論理式「op#off」と、状態遷移後の命題論理式「@op#off」とを得る。テスト情報取得手段１４３は、処理単位”Var  op : onoff_type {off} testedwith {off};”を解釈し、状態遷移前の変数”op”の値は常に”off”であり、状態遷移後の変数”op”の値は常に”off”であると決定する。なお、「op#off」は、状態遷移前の変数”op”の値が”off”であることを示す。また、「@op#off」は、状態遷移後の変数”op”の値が”off”であることを示す。
【０１１７】
そして、ここでは、テスト情報取得手段１４３は、命題論理式「op#off」に対して、図７の変数表を用いて、「op#off」に対応する変数識別子「３」を取得する。そして、「op#off」を「３  ０」に置き換える。なお、「３  ０」の「０」は、命題論理式の終端を示す。また、命題論理式「op#off」をコメントとして付加する。図８が、テスト情報取得手段１４３が取得した命題論理式の集合の例である。図８において、命題論理式はコメントアウトされ（行頭にcが付加され）、それと同意義の変数識別子の集合に置き換わっている。図８の（１）が「op#off」に対応し、（２）がそれと同意義の変数識別子の集合に対応する。同様に、図８の（３）が「@op#off」に対応し、（４）がそれと同意義の変数識別子の集合に対応する。なお、テスト情報取得手段１４３は、コメントアウトされた命題論理式を付加しなくとも良い。
【０１１８】
また、テスト情報取得手段１４３は、例えば、処理単位”op==on&&lamp==off:ch?m: lamp==on;”を読み出し、当該処理単位から命題論理式「op#on∧lamp#off∧ch?m→@lamp#on」を得る。つまり、テスト情報取得手段１４３は、”op==on”を「op#on」、”lamp==off”を「lamp#off」、”ch?m”を「ch?m」にし、”&&”を「∧」に変換し、遷移前状態イベントとを「∧」で連結する。そして、遷移後状態”lamp==on”を「@lamp#on」に変換し、「→」で連結する。以上の処理により、テスト情報取得手段１４３は、仕様記述情報から命題論理式を得る。
【０１１９】
次に、テスト情報取得手段１４３は、処理単位”op==on&&lamp==off:ch?m: lamp==on;”をコメントアウトし、上述のように、当該命題論理式「op#on∧lamp#off∧ch?m→@lamp#on」を変数識別子の集合に変換する処理を行う。ここで、「op#on」に対応する変数識別子が変数表に存在しないので、テスト情報取得手段１４３は、命題論理式「op#on∧lamp#off∧ch?m→@lamp#on」を変数識別子の集合に変換できない、と判断する。よって、テスト情報取得手段１４３は、図８の（５）の情報を得る。
【０１２０】
次に、テスト情報取得手段１４３は、処理単位”op==off -> lamp==off;”を読み出し、当該処理単位から状態遷移前の命題論理式「¬op#off∧lamp#off」と、状態遷移後の命題論理式「¬@op#off∧@lamp#off」とを得る。なお、「¬」は否定を示す。
【０１２１】
そして、テスト情報取得手段１４３は、処理単位”op==off -> lamp==off;”の遷移前の状態をコメントアウトし、図８の（６）を得る。
【０１２２】
そして、テスト情報取得手段１４３は、状態遷移前の命題論理式「¬op#off∧lamp#off」を変数識別子の集合に変換する処理を行い、「−３  ６  ０」を得る。そして、テスト情報取得手段１４３は、図８の（７）を得る。ここで「−３」の「−」は否定を示す。つまり、「¬op#off」から、変数表の「３（op#off）」をマイナスした値である「−３」を得る。また、テスト情報取得手段１４３は、「lamp#off」を変数表に適用し、「６」を得る。
【０１２３】
次に、テスト情報取得手段１４３は、処理単位”op==off -> lamp==off;”の遷移後の状態をコメントアウトし、図８の（８）を得る。そして、テスト情報取得手段１４３は、状態遷移後の命題論理式「¬@op#off∧@lamp#off」を変数識別子の集合に変換する処理を行い、「−４  ８  ０」を得る。そして、テスト情報取得手段１４３は、図８の（９）を得る。つまり、「¬@op#off」から、変数表の「４（@op#off）」をマイナスした値である「−４」を得る。また、テスト情報取得手段１４３は、「@lamp#off」を変数表に適用し、「８」を得る。
【０１２４】
以上のような処理を、仕様記述情報のすべての処理単位に対して行い、テスト情報取得手段１４３は、図８の乗法標準形（ＣＮＦ）のファイルを得る。
【０１２５】
次に、テスト情報取得手段１４３は、状態遷移前の変数”op”の採り得る値”off”と”on”、 状態遷移後の変数”@op”の採り得る値”off”と”on”、状態遷移前の変数”lamp”の採り得る値”off”と”on”、 状態遷移後の変数”@lamp”の採り得る値”off”と”on”、チャネルの変数の採り得る値”m”、デフォルトの”null”の採り得る値”true”と”false”、デフォルトのカウンタ”SubsystemCountUp”の採り得る値”true”と”false”、とすべての組み合わせ（入力値と出力値のセット）が、図８のすべての命題論理式（図８は、正確には命題論理式と同等の変数識別子の集合である）を満足するか否かを判断する。そして、テスト情報取得手段１４３は、すべての命題論理式を満足する入力値と出力値のセットを取得する。この入力値と出力値のセットが、テスト情報である。ただし、ここでは、テスト情報取得手段１４３は、入力値と出力値のセットを、変数表を参照して、数値列に変換する。ここで、テスト情報取得手段１４３が取得した数値列が、図９の（１）（２）（３）である。なお、図９（１）の「-1 2 3 4 -5 6 -7 8 -9」の「−１」は、変数表の「1 null#true」の否定を示す。また、図９（１）の「２」は、変数表の「2 SubsystemCountUp#true」を示す。また、図９（１）の「３」は、変数表の「3 op#off」を示す。
【０１２６】
次に、テスト情報取得手段１４３は、図９（１）から（３）の数値列を、（図７）を用いて、入力値と出力値のセットに変換し、図１０のテスト情報を得る。図１０がテスト情報の一例であり、ここではテストスイートである。なお、図１０において、actionの属性は存在しなくても良い。actionの属性は、状態遷移後に明示的に発生させるイベントが代入され得るが、ここでは、すべて”null”である。
【０１２７】
以下に、テスト情報取得部１４の動作の概念について、図１１を用いて、さらに説明する。図１１において、テスト情報取得部１４は、Ｔ１、Ｔ２、Ｔ３の３つの処理を行う。
【０１２８】
Ｔ１において、仕様記述情報（ここでは、特に、SENSという仕様記述言語で記述したファイルであるSENS記述ファイル）が入力され、CNFファイルが出力される。詳細には、SENS記述に現れる制約情報が乗法標準形（CNF）の命題論理式に変換され、その命題論理式を表す数列の組が出力される。処理の手順は以下の通りである。なお、以下の処理は、すべてテスト情報取得部１４が行う処理である。
【０１２９】
１．テスト情報取得部１４は、SENS記述中に現れる変数について、その変数が現時刻でどの値をとるかを原子命題で表現し、それら原子命題に対してユニークな整数値を割り当てる。この整数値は原子命題の通し番号であり、その原子命題の真偽値が真であることはその整数値の正の値で、偽であることは負の値で表現される。同様に次の時刻でその変数がどの値をとるかを原子命題で表し、その原子命題に対してもユニークな整数値を割り当てる。
【０１３０】
例えば、on,offの値を持つSENSの変数lampについて、テスト情報取得部１４は、現時刻でlampがonであることを表す命題をlamp#on,offであることを表す命題をlamp#offとし、それぞれ整数値５,６を割り当てる。同様に次の時刻でlampがonであることを表す命題を@lamp#on、offであることを表す命題を@lamp#offとし、それぞれ整数値７，８を割り当てる（図８参照）。
【０１３１】
２．テスト情報取得部１４は、SENS記述中に現れる制約情報を命題論理式に変換する。「事前条件：イベント：事後条件,アクション」の形で表現される制約情報は「事前条件∧イベント → 事後条件∧アクション」といった形の命題論理式に変換される。このとき事後条件に現れる変数については、次の時刻の表現として扱う。例えば、SENS記述に現れる「op==on && lamp==off : ch?m : lamp==on;」という記述は、命題論理式「op#on∧lamp#off∧ch?m → @lamp#on」に変換される。
【０１３２】
３．テスト情報取得部１４は、制約情報を表現した命題論理式を乗法標準形に変換する。例えば、命題論理式「op#on∧lamp#off∧ch?m → @lamp#on」を乗法標準形に変換すると「¬op#on∨¬lamp#off∨¬ch?m∨@lamp#on」となる。
【０１３３】
４．乗法標準形の節は、１．で原子命題に割り当てた整数値を使って数列で表現される。このとき否定のリテラルは負の数で表される。テスト情報取得部１４は、一つの節に対する数列を一行として、ファイルに出力する。例えば、節「¬op#on∨¬lamp#off∨¬ch?m∨@lamp#on」は、通常、数列に変換されるが、ここでは、テスト元情報により”op”は”off”のみしかテスト情報の対象とならないので、数列に変換できず、数列は出力されない。
【０１３４】
５．テスト情報取得部１４は、原子命題と整数値の対応表をファイルの末尾にコメントとして書き出す。
【０１３５】
次に、Ｔ２において、テスト情報取得部１４は、CNFファイルを受け付け、DNFファイルを出力する。つまり、CNFファイルが表現している命題論理式を満足する真偽値割り当ては、SAT-solver（公知技術によるソフトウェア）を用いてすべて探索される。処理の流れは以下の図１２の通りである。
【０１３６】
SAT-solverは値割り当てを加法標準形（DNF）で出力する。その値割り当てを、（ａ）数列表現でファイルに書き出し、（ｂ）同時にその論理否定をSAT-solverにフィードバックし、次の値割り当てを得る。これを値割り当てが出力されなくなるまで繰り返す。Ｔ２の出力ファイル中に現れる各数列は、CNFファイルが表現する論理式を満足する値割り当ての一つを表現している。
【０１３７】
次に、Ｔ３の処理を行う。Ｔ３において、SENS記述から作成したCNFファイルとDNFファイルを入力し、CSVファイルを出力する。
【０１３８】
DNFファイルの各数列をCNFファイル末尾の対応表を基に論理式と解釈し、SENSの変数とその値の割り当て表を表現するCSV形式に変換する。CSVの一行がテスト実行時の入力と、それに対応する期待される出力を表す。すなわちCSVの一行が一組のテストスイートを表す。例えば、DNFファイルの一行「-1 -2 3 4 -5 6 -7 8 9」を、命題論理式「op#off∧lamp#off∧ch?m∧@op#off∧@lamp#off」と解釈して、CSV形式「off, off, ch?m, off, off, null」に変換する（図１０の第二レコードを参照）。
【０１３９】
以上、本実施の形態によれば、対象の設計時にテスト設計のための情報を記載すれば、適切なテスト仕様に関する情報が自動生成できる。
【０１４０】
また、本実施の形態によれば、仕様記述情報の中にテスト元情報が記述できることにより、設計者の意図を反映したテスト情報の生成ができる。
【０１４１】
なお、本実施の形態における処理は、ソフトウェアで実現しても良い。そして、このソフトウェアをソフトウェアダウンロード等により配布しても良い。また、このソフトウェアをＣＤ−ＲＯＭなどの記録媒体に記録して流布しても良い。なお、このことは、本明細書における他の実施の形態においても該当する。なお、本実施の形態におけるテスト仕様生成装置を実現するソフトウェアは、以下のようなプログラムである。つまり、このプログラムは、記憶媒体に、テストで利用する情報であるテスト情報と、対象の仕様について記述する言語である仕様記述言語で記述された前記対象の仕様に関する情報であり、１以上の変数の宣言を含む情報であり、テスト情報を生成するためのテスト元情報を含む情報である仕様記述情報を格納しており、コンピュータを、前記変数の宣言および前記テスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得部と、前記テスト情報取得部が取得した１以上のテスト情報を前記テスト情報格納部に蓄積するテスト情報蓄積部として機能させるためのプログラム、である。
【０１４２】
また、上記プログラムにおいて、前記変数は、型を有し、前記仕様記述情報は、前記１以上の変数のうち、１以上の各変数に対応付けて、各変数が採り得る値の中で、テストで使用する値を特定する情報であるテスト元情報を有し、前記テスト情報取得部は、前記仕様記述情報から、前記テスト元情報を前記変数と対応付けて取得するテスト元情報取得手段と、前記仕様記述情報から、テスト元情報を有さない変数と当該変数の型を取得する変数情報取得手段と、前記テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値を変数ごとに取得し、かつ、前記変数情報取得手段が取得した変数と当該変数の型から入力値を変数ごとに取得するテスト情報取得手段を具備するものとして、コンピュータを機能させるためのプログラムであることは好適である。
【０１４３】
また、上記プログラムにおいて、前記テスト情報取得手段は、前記テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、前記変数情報取得手段が取得した変数と当該変数の型から入力値および出力値を変数ごとに取得するものとして、コンピュータを機能させるためのプログラムであることは好適である。
【０１４４】
また、上記プログラムにおいて、前記仕様記述情報は、１以上の変数の宣言、および制約に関する記述である１以上の制約情報を有し、前記テスト情報取得手段は、前記テスト元情報取得手段が取得したテスト元情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、前記変数情報取得手段が取得した変数と当該変数の型から入力値および出力値を変数ごとに取得し、かつ、前記すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するものとして、コンピュータを機能させるためのプログラムであることは好適である。
【０１４５】
また、上記プログラムにおいて、前記制約情報は、１以上の変数の値の集合を有する状態である遷移前状態と当該遷移前状態に対して発生するイベントと前記状態の場合に前記イベントが発生した場合に移行する状態である遷移後状態とを有する状態遷移情報、または１以上の変数の値の集合を有する第一状態と当該第一状態の場合に必ず採用される１以上の変数の値の集合を有する第二状態とを有する不変条件情報であるものとして、コンピュータを機能させるためのプログラムであることは好適である。
【０１４６】
（実施の形態２）
本実施の形態において、不適切なテストスイートの生成を防止できるテスト仕様生成装置２について説明する。本実施の形態において、第一に、状態遷移情報の前提部分を制約として、状態遷移の前提を満たさないテストスイートの生成を防止するテスト仕様生成装置２について説明する。第二に、イベントに関する制約を設け、指定したイベントを含むテストスイートの生成を防止するテスト仕様生成装置２について説明する。第三に、遷移前状態情報を削除し、残りの部分の論理否定を制約情報とするテスト仕様生成装置２について説明する。第四に、遷移後状態情報を削除し、残りの部分の論理否定を制約情報とするテスト仕様生成装置２について説明する。
【０１４７】
図１３は、本実施の形態におけるテスト仕様生成装置２のブロック図である。テスト仕様生成装置２は、テスト情報格納部１１、仕様記述情報格納部１２、受付部１３、テスト情報取得部２４、テスト情報蓄積部１５、テスト情報出力部１６を備える。
【０１４８】
テスト情報取得部２４は、イベント制約情報格納手段２４０、テスト元情報取得手段１４１、変数情報取得手段１４２、テスト情報取得手段２４３を備える。
【０１４９】
仕様記述情報格納部１２が格納している仕様記述情報は、ここでは、１以上の変数の宣言、および１以上の制約情報を有する。また、制約情報は、ここでは、例えば、遷移前状態とイベントと前記状態の場合に遷移後状態とを有する状態遷移情報である。状態遷移情報は、アクションを有しても良い。また、制約情報は、例えば、不変条件情報である。
【０１５０】
テスト情報取得部２４は、変数の宣言を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得する。また、テスト情報取得部２４は、変数の宣言とテスト元情報を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得することは好適である。また、ここでのテスト情報は、通常、テストスイートである。
【０１５１】
イベント制約情報格納手段２４０は、１以上のイベント制約情報を格納し得る。イベント制約情報は、イベントに関する制約を示す情報である。イベント制約情報は、例えば、「¬null」、「¬t?clear」などである。「¬null」は、イベントはnullではないことを示す。また、「¬t?clear」は、イベントは「t?clear」ではないことを示す。
【０１５２】
テスト情報取得部２４は、通常、ＭＰＵやメモリ等から実現され得る。テスト情報取得部２４の処理手順は、通常、ソフトウェアで実現され、当該ソフトウェアはＲＯＭ等の記録媒体に記録されている。但し、ハードウェア（専用回路）で実現しても良い。
【０１５３】
テスト情報取得手段２４３は、仕様記述情報から、変数情報取得手段１４２が取得した変数と当該変数の型から入力値および出力値を変数ごとに取得し、かつ、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する。また、テスト情報取得手段２４３は、仕様記述情報から、各テスト元情報に対応する変数の１以上の入力値および出力値を変数ごとに取得し、かつ、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得しても良い。
【０１５４】
テスト情報取得手段２４３は、１以上の前提情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。ここで、前提情報とは、１以上の制約情報が有する遷移前状態とイベントとの組である。前提情報は、遷移前状態のみでも良い。また、通常、１以上の前提情報の論理和が制約情報となる。仕様記述情報が有する元の制約情報が「(op==on∧null)-> t!start;  (op==on∧t?ring)-> arg1.ch!m∧arg2.ch!m;」である場合、テスト情報取得手段２４３は、当該制約情報の前提情報「(op==on∧null)∨(op==on∧t?ring)」を取得し、制約情報に追加する。ここで、「(op==on∧null)-> t!start」は、変数「op」が「on」かつ「null」であればチャネル「t」にメッセージ「start」を送信する、ことを示す。また、「(op==on∧t?ring)-> arg1.ch!m∧arg2.ch!m;」は変数「op」が「on」かつチャネル「t」が「ring」を受信すれば、チャネル「arg1.ch」にメッセージ「m」かつチャネル「arg2.ch」にメッセージ「m」を送信することを示す。
【０１５５】
また、テスト情報取得手段２４３は、１以上のイベント制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。ここで、イベント制約情報は、イベント制約情報格納手段２４０のイベント制約情報である。
【０１５６】
また、テスト情報取得手段２４３は、既に取得したテストスイート（解と言っても良い。）に対応する制約情報から、１以上の第二制約情報を取得し、当該１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。ここで、第二制約情報は、既に取得したテストスイートの情報が有する遷移前状態情報を削除したうえで、残りの部分の論理否定をとることにより構成される情報である。また、第二制約情報は、制約情報が有する遷移前状態およびイベントを削除したうえで、残りの部分（遷移後状態）の論理否定をとることにより構成される情報であっても良い。例えば、解「op#off, null#true, @op#off」が得られた場合、テスト情報取得手段２４３は、第二制約情報「@op#offでないもの」（¬「@op#off」）を、制約情報として追加する。なお、遷移前状態を削除することは、制約情報から、遷移前状態以外の部分を取得することと同意義である。
【０１５７】
また、第二制約情報は、制約情報が有する遷移後状態情報を削除して、かつ、当該制約情報が有する情報であり、前記遷移後状態以外の部分の論理否定により構成される情報であっても良い。また、第二制約情報は、制約情報が有するアクションおよび遷移後状態を削除して、かつ、当該制約情報が有する情報であり、前記削除した部分以外の部分（遷移前状態）の論理否定により構成される情報であっても良い。例えば、解「op#off,null#true,@op#off」が得られた場合、テスト情報取得手段２４３は、第二制約情報「op#offでない∧イベントがnullでない」（¬(op#off||null#true））を、制約情報として追加する。なお、遷移後状態を削除することは、制約情報から、遷移後状態以外の部分を取得することと同意義である。
【０１５８】
テスト情報取得手段２４３は、通常、ＭＰＵやメモリ等から実現され得る。テスト情報取得手段２４３の処理手順は、通常、ソフトウェアで実現され、当該ソフトウェアはＲＯＭ等の記録媒体に記録されている。但し、ハードウェア（専用回路）で実現しても良い。
【０１５９】
次に、本実施の形態におけるテスト仕様生成装置２の具体的な動作について説明する。以下、４つの具体例について説明する。
【０１６０】
（具体例１）
具体例１は、１以上の前提情報をも制約情報として用いて、無用なテストスイートの抑制を図る場合である。
【０１６１】
今、仕様記述情報格納部１２は、図１４に示す仕様記述情報を格納している。図１４の仕様記述情報は、図６の仕様記述情報と比較して、（３）の「testedwith{off}」を有しない。図１４において、図６と同様、制約情報は（６）（７）である。
【０１６２】
かかる状況において、ユーザは、テスト仕様生成装置１に、テスト情報生成指示を入力した、とする。
【０１６３】
すると、受付部１３は、テスト情報生成指示を受け付ける。そして、テスト情報取得部１４は、仕様記述情報格納部１２から、図１４の仕様記述情報を読み出す。
【０１６４】
次に、テスト情報取得部１４の変数情報取得手段１４２は、図１４の仕様記述情報を解釈し、変数表を取得する。つまり、変数情報取得手段１４２は、まず、デフォルトの変数の情報”null#true”、”SubsystemCountUp#true”を、図示しない記録媒体から取得する。そして、変数情報取得手段１４２は、取得した各変数の情報に変数識別子を付してレコードを構成し、当該レコードを空の変数表に書き込む。
【０１６５】
次に、変数情報取得手段１４２は、図１４の”Extern”、”Data onoff_type; // from main”、”Class B”、” Data m_type {m};”を順次、読み出し、変数の宣言ではない、と判断する。
【０１６６】
次に、変数情報取得手段１４２は、図６の”Var op : onoff_type {off};”を読み出す。そして、変数情報取得手段１４２は、予約語”Var”から、この処理単位が変数の宣言である、と判断する。なお、以降に続く処理単位に対して、変数ではない予約語が出現するまで、変数情報取得手段１４２は、変数の宣言であると判断する、とする。
【０１６７】
次に、変数情報取得手段１４２は、処理単位”Var op : onoff_type {off};”から変数の型”onoff_type”を取得する。次に、テスト元情報取得手段１４１は、この処理単位からテスト元情報を取得できない。
【０１６８】
次に、変数情報取得手段１４２は、変数の型”onoff_type”から、変数”op”の入力値”on”と”off”、および変数”op”の出力値”on”と”off”を取得する。そして、変数情報取得手段１４２は、変数”op”の入力値”on”に変数識別子を付して、レコード”３  op#onを構成する。また、変数情報取得手段１４２は、変数”op”の入力値”off”に変数識別子を付して、レコード”４  op#off”を構成する。また、変数情報取得手段１４２は、変数”op”の出力値”on”に変数識別子を付して、レコード”５  @op#on”を構成する。また、変数情報取得手段１４２は、変数”op”の出力値”off”に変数識別子を付して、レコード”６  @op#off”を構成する。
【０１６９】
次に、変数情報取得手段１４２は、図６の”lamp :onoff_type {off};”を読み出す。そして、変数情報取得手段１４２は、この処理単位が変数の宣言である、と判断する。
【０１７０】
次に、変数情報取得手段１４２は、処理単位”lamp : onoff_type {off};”から変数の型”onoff_type”を取得する。次に、テスト元情報取得手段１４１は、この処理単位からテスト元情報を取得できない。
【０１７１】
次に、変数情報取得手段１４２は、型”onoff_type”を用いて、変数”lamp”の１以上の入力値{on，off}と変数”lamp”の１以上の出力値{on，off}を取得する。そして、変数情報取得手段１４２は、変数”lamp”の入力値”on”に変数識別子を付して、レコード”７  lamp#on”を構成する。また、変数情報取得手段１４２は、変数”lamp”の入力値”off”に変数識別子を付して、レコード”８  lamp#off”を構成する。また、変数情報取得手段１４２は、変数”lamp”の出力値”on”に変数識別子を付して、レコード”９  @lamp#on”を構成する。さらに、変数情報取得手段１４２は、変数”lamp”の出力値”off”に変数識別子を付して、レコード”１０  @lamp#off”を構成する。そして、変数情報取得手段１４２は、これらのレコードを変換表に追記する。
【０１７２】
次に、変数情報取得手段１４２は、図１４の”Channel ch : m_type;”を読み出す。そして、変数情報取得手段１４２は、予約語”Channel”から、この処理単位が変数の宣言である、と判断する。
【０１７３】
次に、変数情報取得手段１４２は、処理単位”Channel ch : m_type;”から変数の型” m_type”を取得する。次に、テスト元情報取得手段１４１は、この処理単位からテスト元情報を取得できない。
【０１７４】
次に、変数情報取得手段１４２は、型”m_type”を用いて、変数”ch”の入力値{m}を取得する。そして、変数情報取得手段１４２は、変数”ch”の入力値”m”に変数識別子を付して、レコード”１１  ch?m”を構成する。そして、変数情報取得手段１４２は、変換表にこのレコードを追記する。なお、予約語”Channel”はイベントを示し、入力値のみ存在し、出力値が存在しないことは、予め変数情報取得手段１４２は知っている。
【０１７５】
以上の処理により、図１５に示す変数表が得られた。
【０１７６】
次に、テスト情報取得手段２４３は、図１４の仕様記述情報を解釈し、以下のように命題論理式を取得する。
【０１７７】
つまり、テスト情報取得手段２４３は、例えば、処理単位”Var  op : onoff_type {off};”を読み出し、当該処理単位から状態遷移前の変数に関する命題論理式「op#on||op#off」と「not(op#on)||not(op#off)」と、状態遷移後変数に関する命題論理式「@op#on||@op#off」と「not(@op#on)||not(@op#off)」とを得る。
【０１７８】
そして、テスト情報取得手段２４３は、図１５の変数表を用いて、例えば、命題論理式「op#on||op#off」に対して、変数識別子の集合「３  ４  ０」を得る。なお、「０」は命題論理式の終端を示す。また、テスト情報取得手段２４３は、図１５の変数表を用いて、例えば、命題論理式「not(op#on)||not(op#off)」に対して、変数識別子の集合「−３  −４  ０」を得る。なお、「−」は「否定」を示す。つまり、「not(op#on)」は変数識別子「−３」となる。また、テスト情報取得手段２４３は、図１５の変数表を用いて、命題論理式「@op#on||@op#of」に対して、変数識別子の集合「５  ６  ０」を得る。さらに、テスト情報取得手段２４３は、図１５の変数表を用いて、命題論理式「not(@op#on)||not(@op#off)」に対して、変数識別子の集合「−５  −６  ０」を得る。また、テスト情報取得手段２４３は、上記の命題論理式をコメント（行頭にcを付加）として付加する。そして、テスト情報取得手段２４３は、図１６の（１）（２）（３）（４）を得る。
【０１７９】
また、テスト情報取得手段２４３は、例えば、処理単位”op==on&&lamp==off:ch?m: lamp==on;”を読み出し、当該処理単位から命題論理式「op#on∧lamp#off∧ch?m→@lamp#on」を得る。つまり、テスト情報取得手段１４３は、”op==on”を「op#on」、”lamp==off”を「lamp#off」、”ch?m”を「ch?m」にし、”&&”を「∧」に変換し、遷移前状態イベントとを「∧」で連結する。そして、遷移後状態”lamp==on”を「@lamp#on」に変換し、「→」で連結する。以上の処理により、テスト情報取得手段２４３は、仕様記述情報から命題論理式を得る。
【０１８０】
次に、テスト情報取得手段２４３は、当該命題論理式「op#on∧lamp#off∧ch?m→@lamp#on」を同値な論理式である「¬op#on ∨ ¬lamp#off ∨ ¬ch?m ∨ @lamp#on」に変形し、図１５の変数表を用いて、変数識別子の集合に変換する処理を行う。そして、テスト情報取得手段２４３は、「９  −１１  −３  −８  ０」を得る。よって、テスト情報取得手段２４３は、図１６の（５）の情報を得る。
【０１８１】
テスト情報取得手段２４３は、以上のような処理を、すべての処理単位に対して行い、図１６の命題論理式の集合を得る。つまり、実施の形態１で述べた処理系Ｔ１に対して、図１４の仕様記述情報を与えれば、図１６の命題論理式の集合が得られる。なお、図１６の命題論理式の集合はSAT-solverへの入力である。
【０１８２】
次に、テスト情報取得手段２４３は、１以上の前提情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得する。つまり、テスト情報取得手段２４３は、図１４の仕様記述情報の制約「op==on && lamp==off : ch?m : lamp==on;」の前提情報「op==on && lamp==off  &&  ch?m」を、仕様記述情報の制約情報として追加する。また、テスト情報取得手段２４３は、図１５の変数表を参照して、「 op == on」に対応する変数３、「lamp == off」に対応する変数８、「ch?m」に対応する変数１１を拾い出し、図１６に、（６）の３行を追加する。
また、状態遷移に関する制約が二つ以上存在するときには、前提情報のいずれかを満たすという制約を追加する。例えば「op==on && lamp==off : ch?m : lamp==on;」と「op==on && lamp==on : null : true;」が制約として存在する場合、テスト情報取得手段２４３は、前提情報「op==on && lamp==off && ch?m」と「op==on && lamp==on && null」とから制約「(op==on && lamp==off && ch?m) || (op==on && lamp==on && null)」を作成する。そして、テスト情報取得手段２４３は、前記制約を、当該制約と同値な論理式「(op==on || op==on) && (op==on || lamp==on) && (op==on ||null) && (lamp==off || op==on) && (lamp==off || lamp==on) && (lamp==off || null) && (ch?m || op==on) && (ch?m || lamp==on) && (ch?m ||null)」に変換したうえで図１５の変数表を参照して、以下の９行の情報を得る。そして、テスト情報取得手段２４３は、９行をＣＮＦファイルに追加する。
３  ３  ０
３  ７  ０
３  １  ０
８  ３  ０
８  ７  ０
８  １  ０
１１  ３  ０
１１  ７  ０
１１  １  ０
【０１８３】
そして、ここで、テスト情報取得手段２４３が上記の１以上の前提情報をも制約情報として用いる処理を行わない場合、例えば、図１６の命題論理式の集合から「op == off , lamp == off, ch?m, @op==on, @lamp == on」というテストスイートが得られる。このテストスイートは、論理式の真偽値の定義上では、図１４の仕様記述情報に記載されている制約「op==on && lamp==off : ch?m : lamp==on;」と「op==off -> lamp==off」を満たすが、当該制約に現れる前提情報が有する遷移前条件「op == on && lamp == off」を満たしていない。そこで、テスト情報取得手段２４３は、図１６の（６）を適用し、上記のテストスイートを解としない。
【０１８４】
以上のように、テスト情報取得手段２４３は、仕様記述情報から事前条件とイベント発生に相当する記述（前提情報）を抽出し、SAT-solverの入力形態に変換して制約を追加することを機械的に実行する。
【０１８５】
（具体例２）
具体例２は、イベント制約情報をも制約情報として用いて、無用なテストスイートの抑制を図る場合である。
【０１８６】
今、仕様記述情報格納部１２は、図１４に示す仕様記述情報を格納している。また、イベント制約情報格納手段２４０は「¬null」を格納している、とする。ここで、「¬null」は「イベントが null でない」ことを示す。つまり、テストの実施計画によっては、イベント発生を伴うテストスイートのみに注目したい場合がある。このとき、イベントを伴わないテストスイートを生成することは冗長である。そこで、イベント制約情報格納手段２４０に「¬null」を格納することによって、無用なテストスイートの発生を抑制する。
【０１８７】
テスト情報取得手段２４３は、イベント制約情報格納手段２４０から「¬null」を読み出す。そして、テスト情報取得手段２４３は、「¬null」を制約として追加する。つまり、テスト情報取得手段２４３は、図１５の変数表を参照し、「null#true」に対応する変数「１」を拾い出し、否定を表す「−」の符号を付加して、図１６の末尾に（７）の一行を追加する。
【０１８８】
そして、テスト情報取得手段２４３が上記の制約情報として「¬null」を用いる処理を行わない場合、例えば、図１６の命題論理式の集合から「op == off , lamp == off, ch?m, @op==on, @lamp == on」というテストスイートが得られる。このテストスイートは、論理式の真偽値の定義上では、図１４の仕様記述情報に記載されている制約「op==on && lamp==off : ch?m : lamp==on;」と「op==off -> lamp==off」を満たすが、当該制約に現れる条件「¬(null#true)」を満たしていない。そこで、テスト情報取得手段２４３は、図１６の（７）を適用し、上記のテストスイートを解としない。
【０１８９】
以上より、テスト情報取得手段２４３は、図１４の仕様を満たし、かつ「イベントが null でない」を満たすテストスイートを探索することとなる。
【０１９０】
また、null 以外についても特定のイベント発生を伴うテストスイートの探索を同様の処理で抑制することができる。例えば、タイマのカウントアップを伴うテストスイートの出力を抑制する際には、テスト情報取得手段２４３は、「SubsystemCountUp」に対応する変数「２」を拾い出して、制約情報「-２  ０」を追加すればよい。なお、かかる場合、イベント制約情報「¬SubsystemCountUp」がイベント制約情報格納手段２４０に格納されている、とする。
【０１９１】
（具体例３）
具体例３は、遷移前状態情報を削除することにより、無用なテストスイートの抑制を図る場合である。具体例３の動作を図１８に示す。
【０１９２】
図１６の命題論理式の集合（CNFファイル）から（６）（７）を除いた命題論理式の集合を、実施の形態１で述べたＴ２で処理すると、DNFファイルが出力される。つまり、従来技術におけるテスト情報取得手段は、図１６の命題論理式の集合から（６）（７）を除いた命題論理式の集合から、図１７に示すような値割り当てを取得する。なお、従来技術におけるテスト情報取得手段は、本実施の形態におけるテスト仕様生成装置２のテストスイート生成の防止機能を有さない。
【０１９３】
図１７の一行目の解（ａ）「-1 -2  3 -4  5 -6 -7  8  9 -10  11」は、図１５の変数表を参照すると、「¬null#true ∧¬S ubsys temCountUp#true ∧ op#on ∧ ¬op#off ∧ @op#on ∧ ¬@op#off ∧ ¬lamp#on ∧ lamp#off ∧ @lamp#on ∧ ¬@lamp#off ∧ ch?m」となる。つまり，図１７の一行目の解のうち「-1, -2, 3, -4, -7, 8, 11」が遷移前状態情報と発生イベントの情報(op==on かつ lamp==off かつ ch?m)である。また、「5, -6, 9, -10」が遷移後状態の情報(@op==on かつ @lamp==on)である。
【０１９４】
また、テスト情報取得手段２４３は、その論理否定「null#true ∨S ubsys temCountUp#true ∨ ¬op#on ∨ op#off ∨ ¬@op#on ∨ @op#off ∨ lamp#on ∨ ¬lamp#off ∨ ¬@lamp#on ∨ @lamp#off ∨ ¬ch?m」を符号化した数列「1 2 -3 4 -5 6 7 -8 -9 10 -11 0」を取得し、SAT-solverにフィードバックし、その結果、二つ目の解（ｂ）を計算する。ここで、テスト情報取得手段２４３は、フィードバックの際に、得られた最初の解の否定ではなく、遷移後状態「5, -6, 9, -10」(@op==on かつ @lamp==on)の否定を取得する。つまり、テスト情報取得手段２４３は、テストスイートに対応する情報が有する遷移前状態とイベントの情報を削除して、かつ、当該制約情報が有する情報であり、削除した以外の部分の論理否定により構成された情報を取得する。具体的には、テスト情報取得手段２４３は、制約情報「(@op==on かつ @lamp==on) でないもの」を取得する。つまり、テスト情報取得手段２４３は、事後状態が（ａ）とは異なる解となるテストスイートを取得する。図１７の（ｂ）は事後状態に相当する部分が「5 -6 9 -10」で（ａ）と同一であり、制約情報「(@op==on かつ @lamp==on) でないもの」を満たさない。従って、テスト情報取得手段２４３は、図１７の（ｂ）に対応するテストスイートを、最終的に出力しない。
【０１９５】
一方、図１７の（ｃ）は事後状態に相当する部分が「5 -6 -9 10」であり、制約情報「(@op==on かつ @lamp==on) でないもの」を満たす。従って、テスト情報取得手段２４３は、図１７の（ｃ）に対応するテストスイートを、最終的に出力する。以上より、テスト情報取得手段２４３は、結果として、事後状態に重複のないテストスイートの網羅的なリストを得ることができる。
【０１９６】
（具体例４）
具体例４は、事後状態情報を削除することにより、無用なテストスイートの抑制を図る場合である。
【０１９７】
具体例３と同様に、図１６の命題論理式の集合（CNFファイル）を、実施の形態１で述べたＴ２で処理すると、図１７に示すような値割り当てが得られる。
【０１９８】
また、図１７の一行目の解（ａ）「-1 -2  3 -4  5 -6 -7  8  9 -10  11」は、図１５の変数表を参照すると、「¬null#true ∧¬S ubsys temCountUp#true ∧ op#on ∧ ¬op#off ∧ @op#on ∧ ¬@op#off ∧ ¬lamp#on ∧ lamp#off ∧ @lamp#on ∧ ¬@lamp#off ∧ ch?m」となる。つまり「-1, -2, 3, -4, -7, 8, 11」が事前状態情報と発生イベントの情報(op==on かつ lamp==off かつ ch?m)である。
【０１９９】
そして、テスト情報取得手段２４３は、事前状態情報と発生イベントの論理否定「(op==on かつ lamp==off かつ ch?m)の否定」を取得する。そして、テスト情報取得手段２４３は、元の制約をすべて満たし、かつ「 (op==on かつ lamp==off かつ ch?m) でないもの」を満たすテストスイートを取得する。つまり、図１７の（ｂ）が「 (op==on かつ lamp==off かつ ch?m) でないもの」を満たすとして、テスト情報取得手段２４３は、図１７の（ｂ）をテストスイートとして採用する。以上により、テスト情報取得手段２４３は、結果として、事前状態に重複のないテストスイートの網羅的なリストを得る。
【０２００】
以上、本実施の形態によれば、不適切なテストスイートの生成を防止できる。
【０２０１】
さらに、本実施の形態におけるテスト仕様生成装置を実現するソフトウェアは、以下のようなプログラムである。つまり、このプログラムは、記憶媒体に、テストで利用する情報であるテスト情報と、対象の仕様について記述する言語である仕様記述言語で記述された前記対象の仕様に関する情報であり、１以上の変数の宣言を含む情報である仕様記述情報を格納しており、コンピュータを、前記変数の宣言を用いて、１以上の各変数の入力値を少なくとも有する１以上のテスト情報を取得するテスト情報取得部と、前記テスト情報取得部が取得した１以上のテスト情報を前記テスト情報格納部に蓄積するテスト情報蓄積部として機能させるためのプログラム、である。
【０２０２】
また、上記プログラムにおいて、前記仕様記述情報は、１以上の変数の宣言、および制約に関する記述である１以上の制約情報を有し、前記テスト情報取得手段は、前記変数情報取得手段が取得した変数と当該変数の型から入力値および出力値を変数ごとに取得し、かつ、前記すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得するプログラムである。
【０２０３】
また、上記プログラムにおいて、前記制約情報は、１以上の変数の値の集合を有する状態である遷移前状態と当該遷移前状態に対して発生するイベントと前記状態の場合に前記イベントが発生した場合に移行する状態である遷移後状態とを有する状態遷移への制約情報であることは好適である。
【０２０４】
また、上記プログラムにおいて、前記テスト情報取得手段は、前記１以上の制約情報が有する遷移前状態とイベントとの組である１以上の前提情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。
【０２０５】
また、上記プログラムにおいて、前記テスト情報取得部は、イベントに関する制約を示す１以上のイベント制約情報を格納し得るイベント制約情報格納手段をさらに具備し、前記テスト情報取得手段は、前記１以上のイベント制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。
【０２０６】
また、上記プログラムにおいて、前記テスト情報取得手段は、既に取得したテストスイートに対応する制約情報から、当該制約情報が有する遷移前状態とイベントに関する情報を削除し、かつ、当該遷移前状態以外の当該制約情報が有する部分の論理否定を構成した１以上の第二制約情報を取得し、当該１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。
【０２０７】
また、上記プログラムにおいて、前記テスト情報取得手段は、前記１以上の各制約情報から、各制約情報が有する遷移後状態を削除し、かつ、前記各制約情報が有する部分であり、当該遷移後状態以外の部分の論理否定を構成した１以上の第二制約情報を取得し、当該１以上の第二制約情報をも制約情報として用いて、すべての制約情報を満たすように、１以上の入力値および１以上の出力値の組であるテストスイートを１以上取得することは好適である。
【０２０８】
また、図１９は、本明細書で述べたプログラムを実行して、上述した実施の形態のテスト仕様生成装置等を実現するコンピュータの外観を示す。上述の実施の形態は、コンピュータハードウェア及びその上で実行されるコンピュータプログラムで実現され得る。図１９は、このコンピュータシステム３４０の概観図であり、図２０は、コンピュータシステム３４０の内部構成を示す図である。
【０２０９】
図１９において、コンピュータシステム３４０は、ＦＤドライブ３４１１、ＣＤ−ＲＯＭドライブ３４１２を含むコンピュータ３４１と、キーボード３４２と、マウス３４３と、モニタ３４４とを含む。
【０２１０】
図２０において、コンピュータ３４１は、ＦＤドライブ３４１１、ＣＤ−ＲＯＭドライブ３４１２に加えて、ＭＰＵ３４１３と、ＣＤ−ＲＯＭドライブ３４１２及びＦＤドライブ３４１１に接続されたバス３４１４と、ブートアッププログラム等のプログラムを記憶するためのＲＯＭ３４１５とに接続され、アプリケーションプログラムの命令を一時的に記憶するとともに一時記憶空間を提供するためのＲＡＭ３４１６と、アプリケーションプログラム、システムプログラム、及びデータを記憶するためのハードディスク３４１７とを含む。ここでは、図示しないが、コンピュータ３４１は、さらに、ＬＡＮへの接続を提供するネットワークカードを含んでも良い。
【０２１１】
コンピュータシステム３４０に、上述した実施の形態のテスト仕様生成装置等の機能を実行させるプログラムは、ＣＤ−ＲＯＭ３５０１、またはＦＤ３５０２に記憶されて、ＣＤ−ＲＯＭドライブ３４１２またはＦＤドライブ３４１１に挿入され、さらにハードディスク３４１７に転送されても良い。これに代えて、プログラムは、図示しないネットワークを介してコンピュータ３４１に送信され、ハードディスク３４１７に記憶されても良い。プログラムは実行の際にＲＡＭ３４１６にロードされる。プログラムは、ＣＤ−ＲＯＭ３５０１、ＦＤ３５０２またはネットワークから直接、ロードされても良い。
【０２１２】
プログラムは、コンピュータ３４１に、上述した実施の形態のテスト仕様生成装置等の機能を実行させるオペレーティングシステム（ＯＳ）、またはサードパーティープログラム等は、必ずしも含まなくても良い。プログラムは、制御された態様で適切な機能（モジュール）を呼び出し、所望の結果が得られるようにする命令の部分のみを含んでいれば良い。コンピュータシステム３４０がどのように動作するかは周知であり、詳細な説明は省略する。
【０２１３】
また、上記プログラムを実行するコンピュータは、単数であってもよく、複数であってもよい。すなわち、集中処理を行ってもよく、あるいは分散処理を行ってもよい。
【０２１４】
また、上記各実施の形態において、各処理（各機能）は、単一の装置（システム）によって集中処理されることによって実現されてもよく、あるいは、複数の装置によって分散処理されることによって実現されてもよい。
【０２１５】
本発明は、以上の実施の形態に限定されることなく、種々の変更が可能であり、それらも本発明の範囲内に包含されるものであることは言うまでもない。
【産業上の利用可能性】
【０２１６】
以上のように、本発明にかかるテスト仕様生成装置は、対象の設計時にテスト設計のための情報を記載すれば適切なテスト仕様に関する情報が自動生成できる、という効果を有し、テスト支援装置等として有用である。
【符号の説明】
【０２１７】
１、２  テスト仕様生成装置
１１  テスト情報格納部
１２  仕様記述情報格納部
１３  受付部
１４、２４  テスト情報取得部
１５  テスト情報蓄積部
１６  テスト情報出力部
１４１  テスト元情報取得手段
１４１  テスト情報元取得手段
１４２  変数情報取得手段
１４３、２４３  テスト情報取得手段
【図１】
2012128120.tif 000003
【図２】
2012128120.tif 000004
【図３】
2012128120.tif 000005
【図４】
2012128120.tif 000006
【図５】
2012128120.tif 000007
【図６】
2012128120.tif 000008
【図７】
2012128120.tif 000009
【図８】
2012128120.tif 000010
【図９】
2012128120.tif 000011
【図１０】
2012128120.tif 000012
【図１１】
2012128120.tif 000013
【図１２】
2012128120.tif 000014
【図１３】
2012128120.tif 000015
【図１４】
2012128120.tif 000016
【図１５】
2012128120.tif 000017
【図１６】
2012128120.tif 000018
【図１７】
2012128120.tif 000019
【図１８】
2012128120.tif 000020
【図１９】
2012128120.tif 000021
【図２０】
2012128120.tif 000022
【国際調査報告】
2012128120.tif 000023
2012128120.tif 000024
2012128120.tif 000025
2012128120.tif 000026