(57)【特許請求の範囲】
【請求項１】
コンピューティング装置がソフトウェア・プログラムを試験する方法であって：
前記ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に記号的な源セット要素を割り当てて、前記記号的な源セット要素に基づいてデータ構造を生成する段階であって、前記データ構造が、前記記号的な源セット要素の一つまたは複数の間の合併を含む源セットを含み、前記データ構造が、前記源セットをブーリアン関数にエンコードすることによって生成される源セット関数を含み、前記源セット関数が、前記記号的な源セット要素を表わすブーリアン変数および配列のインデックスを表わすブーリアン変数を含む配列源セット関数を含む、段階と；
前記ソフトウェア・プログラムの前記入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行する段階と；
前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行する段階とを含む、
方法。
【請求項２】
前記データ構造が図においてグラフで表現される、請求項１記載の方法。
【請求項３】
前記図が、二分決定図、縮小された順序付けられた二分決定図、共有された縮小された順序付けられた二分決定図、零抑制された決定図、二分モーメント図、自由二分決定図、パリティー決定図、代数的決定図または複数末端二分決定図のうちの一つを含む単一の図である、請求項２記載の方法。
【請求項４】
コンピューティング装置がソフトウェア・プログラムを試験する方法であって：
前記ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に記号的な源セット要素を割り当てて、前記記号的な源セット要素に基づいてデータ構造を生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行する段階と；
前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行し、各記号的な源セット要素にブーリアン変数を割り当てて各入力変数についての源セット関数を生成する段階とを含み、
前記源セット関数が、前記記号的な源セット要素を表わすブーリアン変数および配列のインデックスを表わすブーリアン変数を含む配列源セット関数を含む、
方法。
【請求項５】
前記現在命令についての源セット関数を計算する段階をさらに含む、請求項４記載の方法。
【請求項６】
前記現在命令が非配列命令を含み、前記現在命令についての源セット関数を計算する段階が、前記現在命令のオペランドに関連付けられた源セット関数の合併を計算することを含む、請求項５記載の方法。
【請求項７】
前記現在命令が、源セット関数に関連付けられたデータを配列インデックスをもつ配列に書き込む配列書き込み命令を含み、前記現在命令についての源セット関数を計算する段階が：
前記配列インデックスを表わすブーリアン変数と前記書き込みデータに関連付けられた前記源セット関数のブーリアン変数との間のブーリアンAND演算を計算し；
前記配列の各要素に関連付けられた源セット関数の間のブーリアンOR演算を計算することを含む、
請求項５記載の方法。
【請求項８】
前記現在命令が、源セット関数に関連付けられたデータを記号的な配列インデックスをもつ配列に書き込む配列書き込み命令を含み、前記現在命令についての源セット関数を計算する段階が：
前記記号的な配列インデックスと前記配列の前記源セット関数のブーリアン変数とのブーリアンAND演算を計算し；
前記配列の各要素に関連付けられた源セット関数の間のブーリアンOR演算を計算することを含む、
請求項５記載の方法。
【請求項９】
前記現在命令が、配列インデックスをもつ配列からデータを読む配列読み取り命令を含み、前記現在命令についての源セット関数を計算する段階が、前記配列に関連付けられた前記源セット関数の前記配列インデックスに具体的な値を割り当てることを含む、請求項５記載の方法。
【請求項１０】
前記現在命令が、記号的な配列インデックスによって配列からデータを読む配列読み取り命令を含み、前記現在命令についての源セット関数を計算する段階が、前記記号的な配列インデックスに関連付けられたブーリアン変数を前記配列インデックスに関連付けられたブーリアン変数に割り当てることを含む、請求項５記載の方法。
【請求項１１】
前記データ源解析を実行することがさらに、前記現在命令が、前記ソフトウェア・プログラムの前記一つまたは複数の入力変数に割り当てられた前記具体的な値に基づいて満足されることができない条件文を含むかどうかを判定することを含む、請求項４記載の方法。
【請求項１２】
前記現在命令が前記ソフトウェア・プログラムの前記一つまたは複数の入力変数に割り当てられた前記具体的な値に基づいて満足されることができない条件文を含むと判定することに応答して、前記ソフトウェア・プログラムについての試験カバー範囲要求が満たされたかどうかを判定する段階と；
前記試験カバー範囲要求が満たされていないと判定するのに応答して、前記条件文を制御する入力変数を特定し、特定された入力変数を記号的にすることによって前記試験ドライバを向上させる段階とをさらに含む、
請求項１１記載の方法。
【請求項１３】
前記ソフトウェア・プログラムについての前記試験カバー範囲要求が満たされていると判定するのに応答して、前記ソフトウェア・プログラムについての具体的な試験の組を生成する段階をさらに含む、請求項１２記載の方法。
【請求項１４】
前記データ構造が、二分決定図、縮小された順序付けられた二分決定図、共有された縮小された順序付けられた二分決定図、零抑制された決定図、二分モーメント図、自由二分決定図、パリティー決定図、代数的決定図または複数末端二分決定図のうちの一つを含む単一の図においてグラフで表現される、請求項４記載の方法。
【請求項１５】
コンピュータ可読命令が記憶されている非一時的なコンピュータ可読媒体であって、前記コンピュータ可読命令は、
ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に記号的な源セット要素を割り当てて、前記記号的な源セット要素に基づいてデータ構造を生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行する段階と；
前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行する段階とを含む
動作を実行するまたは該動作の実行を制御するようプロセッサによって実行可能であり、
前記データ構造が：
前記記号的な源セット要素の一つまたは複数の間の合併を含む源セット；
前記源セットをブーリアン関数にエンコードすることによって生成される源セット関数であって、前記ブーリアン関数は前記記号的な源セット要素を表わすブーリアン変数を含む、源セット関数；および
配列源セット関数であって、前記配列源セット関数の前記記号的な源セット要素を表わすブーリアン変数および前記配列源セット関数のインデックスを表わすブーリアン変数を含む、配列源セット関数を含む、
非一時的なコンピュータ可読媒体。
【請求項１６】
前記データ構造が、二分決定図、縮小された順序付けられた二分決定図、共有された縮小された順序付けられた二分決定図、零抑制された決定図、二分モーメント図、自由二分決定図、パリティー決定図、代数的決定図または複数末端二分決定図のうちの一つを含む単一の図においてグラフで表現される、請求項１５記載の非一時的なコンピュータ可読媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本稿で論じられる実施形態は、データ源解析に基づく逐次反復的な試験生成に関する。
【背景技術】
【０００２】
電子装置の使用が増すにつれ、それらの装置上で実行されるソフトウェア・プログラムの数も増す。典型的には、ソフトウェア・プログラムが開発されるとき、該ソフトウェア・プログラムが該ソフトウェア・プログラムについての所定の要件のすべてを満たすことを保証する助けとなるために、該ソフトウェア・プログラムは検証される。ソフトウェア・プログラムがすべての所定の要件を満たすかどうかを判定するための試験ケースを開発することは、困難で、時間がかかることがある。
【０００３】
ソフトウェア・アプリケーションは、任意の数のプログラム（たとえば、クラス、関数、プロシージャ、サブルーチン、モジュールまたはコード・ブロック）を含むことがあり、各プログラムは個々に試験または有効確認されうる。プログラムは手動または自動で試験または有効確認されうる。前者の場合、人（たとえばソフトウェア試験エンジニア）が手動でプログラムのための試験ケースを、該プログラムの設計仕様に基づいて設計し、試験ケースのもとで該プログラムを実行し、試験ケースに一致しないプログラム挙動または出力があるかどうか検査してもよい。後者の場合、コンピュータ・ソフトウェアまたはハードウェアとして実装されるソフトウェア試験ツールが試験対象プログラムについての試験ケースを生成し、それらの試験ケースをシミュレートしながら試験対象プログラムを実行し、試験ケースに一致しないプログラム挙動または出力があるかどうか検査してもよい。現代のソフトウェアのまさに複雑さのため、試験ケースの手動での生成または設計は、プログラムを完全に試験するためには不十分となる。
【０００４】
プログラムは、該プログラムの入力変数に試験入力値を割り当てることによって形式的に試験され、有効確認されうる。それらの入力変数から帰結する出力値が解析されて、挙動を判別し、プログラムを有効確認してもよい。プログラムを試験するために使われる試験入力値を自動的に生成するために、記号的実行が使われてもよい。たとえば、ソフトウェア試験ツールは、具体的な値の代わりに記号的な値を利用することによってどの入力がプログラムの各部分を実行させるかを判別し、プログラム中の各条件付き分枝について可能な帰結を同定するための記号的な表現および制約条件を生成するために、記号的実行を使うことがある。
【０００５】
記号的実行とは、抽象的な解釈のケースとして、実際の値ではなく記号的〔シンボリック〕な値を追跡することによるプログラムの解析をいう。それは、プログラムへの入力を記号変数として扱う、明示的でない状態モデル検査技法である。それは、記号変数を用いてプログラム中の有限の経路を実行することによって複雑な方程式を生成し、次いでソルバを用いて該複雑な方程式を解いて、エラー・シナリオがもしあればそれを取得する。明示的な状態モデル検査とは対照的に、記号的実行は、いくつかの実施形態では、解析対象プログラムにおける、すべての可能な入力値と、すべての可能な入力値のすべての可能な使用ケースとを割り出すことができることがある。このように、記号的実行は、解析対象プログラムを網羅的に有効確認しうる。
【０００６】
本願で特許請求される主題は、何らかの欠点を解決するまたは上記のような環境でのみ動作する実施形態に限定されるものではない。むしろ、この背景は、本稿に記載されるいくつかの実施形態が実施されうる一つの例示的な技術領域を例解するために与えられているだけである。
【発明の概要】
【課題を解決するための手段】
【０００７】
ある実施形態のある側面によれば、方法が、ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成することを含んでいてもよい。本方法は、ソフトウェア・プログラムの入力変数に記号的な源セット要素を割り当てて、該記号的な源セット要素に基づいてデータ構造を生成することをも含んでいてもよい。本方法は、前記ソフトウェア・プログラムの入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行することをも含んでいてもよい。本方法は、前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行することをも含んでいてもよい。
【０００８】
前記実施形態の目的および利点は、少なくとも、請求項において具体的に指摘される要素、特徴および組み合わせによって、実現され、達成されるであろう。
【０００９】
上記の概括的な記述および以下の詳細な記述はいずれも例示的であり、特許請求される発明を制約するものではないことを理解しておくものとする。
【図面の簡単な説明】
【００１０】
例示的実施形態は、付属の図面の使用を通じて、さらなる具体性および詳細さをもって記述され、説明される。
【図１】試験対象の例示的プログラムと、該例示的プログラムを試験するための試験ドライバの三つのバージョンとを示す図である。
【図２】図１の例示的プログラムと、入力およびプログラム変数に関連付けられた源セットを含む対応するデータ構造とを示す図である。
【図３】図１の例示的プログラムと、入力およびプログラム変数に関連付けられた源セット関数を含む対応するデータ構造とを示す図である。
【図４】図３のデータ構造の、共有される縮小された順序付けされた二分決定図を示す図である。
【図５】ソフトウェア・プログラムを試験する例示的方法のフローチャートを示す図である。
【図６】データ源解析を用いた記号的実行の例示的方法のフローチャートである。
【図７】源セット関数計算の例示的方法のフローチャートである。
【図８】データ源解析に基づく逐次反復的な試験生成のために構成されている例示的なコンピューティング装置を示すブロック図である。
【発明を実施するための形態】
【００１１】
本稿での用法では、「データ源」または「源」は、プログラムの入力変数を指す；「源セット要素」は、プログラムの入力変数に割り当てられる記号変数である；「データ源セット」または「源セット」は、一緒になってプログラムのある実行経路における値を決定する、一つまたは複数の源セット要素の和集合である；記号「∧」は一つまたは複数のブーリアン変数の間のブーリアン「AND」演算を表わす；記号「∨」は一つまたは複数のブーリアン変数の間のブーリアン「OR」演算を表わす；記号
【数１】
0006701799.tif 000002
は一つまたは複数のブーリアン変数に対するブーリアン補演算を表わす；「源セット関数」は、一つまたは複数のブーリアン演算によって互いに関係付けられた一つまたは複数のブーリアン変数を含む。
【００１２】
データ源解析とは、変数の値を決定する入力変数（またはその源セット要素）を特定するプロセスをいう。プログラムのデータ源解析に基づく逐次反復的な試験生成は、プログラムの試験カバー範囲を逐次反復的に改善しうる。しかしながら、データ源解析に基づく単純な逐次反復的な試験生成は、多大なメモリおよび計算時間を費消しうる追加的なデータ構造を利用することがある。たとえば、データ構造に含まれる源セットの数の多さから、高い空間オーバーヘッドが帰結することがありうる。データ構造に含まれる源セットの数は、O((値記憶の数)×(プログラム状態の数))によって定義されてもよい。ここで、Oは「ビッグO記法」を指し、これは、処理時間または作業空間要求の点で、アルゴリズムが入力サイズの変化にどのように応答するかに従ってアルゴリズムを分類するために計算機科学において一般的に使われている。値記憶は、入力変数、プログラム変数、配列変数を含む値の任意の記憶を含みうる。プログラム状態の数は、プログラム中の経路の数までであり、該経路の数を含んでいてもよい。よって、10から約100までの範囲の典型的なプログラムについての源セット・サイズでは、ヒープおよびスタック・メモリを含むプログラムのメモリ・サイズは、非常に大きいことがある（たとえば1MB以上）。同様に、O((実行される命令の数)×(状態の数))として定義されうる源セット操作の数の多さから、高い時間オーバーヘッドが帰結しうる。ここで、Oはやはり「ビッグO記法」を指す。例示的な源セット操作は、二つ以上の源セットの合併、二つ以上の源セットの等価性検査および二つ以上の源セットの包含検査を含んでいてもよいが、それに限られない。さらに、データ源解析に基づく単純な逐次反復的な試験生成は、記号的な配列インデックスをサポートせず、配列の各要素に別個の源セットが関連付けられる。このように、単純な逐次反復的試験生成を利用する配列アクセス命令の記号的実行の間、配列の任意の要素がアクセスされることができると想定され、配列のすべての源セット要素の合併を取ることによって、配列全体がスカラーと見なされる。これは、データ源解析プロセスの精度を有意に劣化させることがありうる。
【００１３】
よって、データ源解析に基づく逐次反復的な試験生成へのより洗練されたアプローチが望まれていることがありうる。このプロセスに付随する空間および時間のオーバーヘッドを軽減するためである。本稿で論じられる実施形態では、源セットをブーリアン関数においてエンコードすることによってデータ構造の源セットを表現し、操作し、それらのブーリアン源セット関数を単一の図またはグラフにおいて表現することによって、空間および時間オーバーヘッドが軽減されうる。ブーリアン源セット関数のグラフ表現は、二分決定図、縮小された順序付けられた二分決定図（reduced  ordered  binary  decision  diagram）、共有された縮小された順序付けられた二分決定図（shared  reduced  ordered  binary  decision  diagram）、零抑制された決定図（zero-suppressed  decision  diagram）、二分モーメント図（binary  moment  diagram）、自由二分決定図（free  binary  decision  diagram）、パリティー決定図（parity  decision  diagram）、代数的決定図（algebraic  decision  diagram）または複数末端二分決定図（multiple  terminal  binary  decision  diagram）を使って達成されてもよい。このように、異なるブーリアン関数の間の共通のサブ構造を単一のグラフにおいて共有することによって空間オーバーヘッドを軽減するために、源セットは、単一のグラフにおいて最大限共有されてもよい。さらに、単一のグラフにおける源セットの操作は、時間オーバーヘッドを軽減することにより、より効率的でもありうる。たとえば、単一のグラフにおいて表現されている二つの源セットの等価性検査に関連する時間オーバーヘッドはO(1)でありうる。これについては下記でより詳細に論じる。さらに、ブーリアン源セット関数を単一のグラフで表現することは、記号的配列インデックスが、単一のグラフにおけるブーリアン源セット関数としてエンコードされることを許容しうる。そのため、データ源解析は、配列アクセス命令が記号的に実行されるときに精度劣化を受けないことがある。
【００１４】
以下の記述では、開示される主題の議論を容易にするために例として詳細が記述される。開示される実施形態は、単に例として与えられるのであって、あらゆる可能な実施形態を網羅するものではない。いくつかの実施形態は、付属の図面を参照して説明される。
【００１５】
図１は、試験対象の例示的ソフトウェア・プログラム１００（以下、「例示的プログラム」または「プログラム」）を、該プログラム１００を試験するよう構成された試験ドライバの三つのバージョン１２０、１３０、１４０とともに示している。図１に示される例示的プログラム１００は、コード行１０１においてfunction_under_testと名付けられた関数として定義されている。より一般には、一つまたは複数のクラス、プロシージャ、関数、サブルーチン、モジュール、コード・ブロックなどを含んでいてもよいプログラムを含む任意のプログラムが試験されうる。例示的プログラム１００は、コード行１０２、１０３、１０４において整数入力変数として定義されている、入力変数x、y、zを受領するよう構成されている。例示的プログラム１００は、プログラム１００の本体にさまざまなプログラム変数を含む。それには、それぞれコード行１０６、１０７、１０８、１１０、１１３および１１５において定義されているp、q、r、a、t、uが含まれる。例示的プログラム１００は、コード行１０９、１１４、１１６に見出される条件文をも含んでいる。
【００１６】
例示的プログラム１００を試験するために、コード行１２１においてtest_1と名付けられる初期試験ドライバ１２０が、形成されてもよい。これは、プログラム１００の入力変数（x、y、z）に具体的な値を割り当て、次いでプログラム１００を評価して、これらの初期の具体的な値が例示的プログラム１００の実行経路の全部または実質的な数をトリガーできるかどうかが判定されることによる。この例では、選択され、入力変数x、y、zに割り当てられる具体的な値は、コード行１２３、１２４、１２５において見られるように、0である。より一般には、任意の好適な具体的な値が選択され、初期の試験ドライバ１２０における入力変数に割り当てられてもよい。
【００１７】
プログラム１００は、コード行１２６における関数コールによって試験ドライバ１２０によって試験されてもよい。例示的プログラム１００の各命令は、該命令が条件文を含むかどうかを判定するために評価されてもよい。少なくとも一つの実施形態では、例示的プログラム１００の各命令は、プログラムの現在命令を解析するためにプログラム・カウンタ（図示せず）を利用し、プログラムの次の命令を解析するためにプログラム・カウンタをインクリメントすることにより、順に逐次反復的に評価されてもよい。現在命令が条件文を含む場合、条件文は、入力値に割り当てられた具体的な値によって該条件文が満たされうるかどうかを判定するために解析されてもよい。たとえば、コード行１０９が変数rによって決定される条件文を含むことが判別されることがありうる。変数rは、データ源解析を使ってさらに評価されて、どの入力変数がrの値を決定するかを識別してもよい。この例では、r＝p−z＝x*2−zである。このように、rは入力変数xおよびzに依存する。しかしながら、xおよびzは0という具体的な値を割り当てられているので、rも0に等しく、コード行１０９における条件は満たされることができない。よって、初期の試験ドライバ１２０は、識別された入力変数xおよびzを、試験ドライバの第二のバージョン１３０のコード行１３３および１３５に示されるように記号的にすることによって、更新または向上されてもよい。この第二のバージョンはコード行１３１においてtest_2と名付けられている。
【００１８】
試験ドライバの第二のバージョン１３０は、xおよびzについての記号的な値およびyについての0の具体的な値を用いて再びプログラム１００を試験してもよい。例示的プログラム１００の各命令は、該命令が条件文を含むかどうかおよび該条件文が入力変数の記号的および／または具体的な値によって満たされうるかどうかを判定するために、評価されてもよい。この反復工程では、xおよびzが今や記号的なので、コード行１０９における条件文は満たされうる。しかしながら、コード行１１４における条件文は変数tに依存し、t＝a[1]＝q＝p＋yである。このように、tはyに依存し、コード行１１４における条件は満たされることができない。よって、初期の試験ドライバの第二のバージョン１３０は、識別された入力変数yを、試験ドライバの第三のバージョン１４０のコード行１４４に示されるように記号的にすることによって、更新または向上されてもよい。この第三のバージョンはコード行１４１においてtest_3と名付けられている。試験ドライバ１４０の第三のバージョンは、x、y、zについての記号的な値を用いて、満たされることのできない何らかの条件文があるかどうかを判定するために再びこのプログラムを試験してもよい。
【００１９】
このようにして、逐次反復的な試験生成は、例示的プログラム１００の実行経路の全部またはかなりの数が試験されうることを保証するよう、データ源解析を使って例示的プログラム１００に対して実行されてもよい。たとえば、試験ドライバの第三のバージョン１４０が例示的プログラム１００の実行経路の全部を試験できることがありうる。
【００２０】
データ源解析の単純なプロセスについてここで、図２を参照して説明する。図２は、図１の例示的プログラム１００と、単純なデータ源解析の間に生成される対応するデータ構造２００とを示している。データ構造２００は、源セット２０２、２０４、２０６、２０８、２１０、２１２、２１４、２１６、２１８、２２０、２２２、２２４、２２６、２２８、２３０、２３２（以下、「源セット２０２〜２３２」）を含んでいてもよい。これらはそれぞれ変数x、y、z、p、q、r、a、t、uおよびプログラム１００の命令において定義されるそれらの関連する値に関連付けられ、入力変数x、y、zを用いて書かれてもよい。
【００２１】
第一のステップでは、コード行１０２、１０３、１０４が読まれてもよく、記号的な源セット要素S1、S2、S3が生成され、プログラム１００の各入力変数x、y、zに割り当てられ、それぞれの源セット２０２、２０４、２０６に格納されてもよい。次いでコード行１０６が読まれてもよく、プログラム変数pが、記号的な源セット要素S1を割り当てられている入力変数xに依存することが判別されてもよい。こうして、S1はpに関連付けられ、源セット２０８に格納されてもよい。次いでコード行１０７が読まれてもよく、プログラム変数qが、記号的な源セット要素S1およびS2を割り当てられている入力変数xおよびyに依存することが判別されてもよい。こうして、S1およびS2の和集合がqに関連付けられ、源セット２１０に格納されてもよい。コード行１０８が読まれてもよく、プログラム変数rが、記号的な源セット要素S1およびS3を割り当てられている入力変数xおよびzに依存することが判別されてもよい。こうして、S1およびS3の和集合がrに関連付けられ、源セット２１２に格納されてもよい。コード行１１１および１１２が読まれてもよく、これらのプログラム命令がqおよびrの値をそれぞれ配列aの第二および第三の要素に書き込む配列書き込み命令を定義していることが判別されてもよい。こうして、S1およびS2の和集合が配列aの第二の要素に関連付けられ、源セット２１６に格納されてもよい。同様に、S1およびS3の和集合が配列aの第三の要素に関連付けられ、源セット２１８に格納されてもよい。
【００２２】
プログラム実行状態のこの点において、第一の配列要素および第四の配列要素は空の源セット２１４および２２０をもつ。さらに、配列aの各要素は、一意的な源セットに関連付けられている。コード行１１３が読まれてもよく、このプログラム命令が、配列aにアクセスして第二の配列要素の値を変数tに格納する配列読み取り命令を定義していることが判別されてもよい。こうして、S1およびS2の和集合がtに関連付けられ、源セット２２２に格納されてもよい。コード行１１５が読まれてもよく、このプログラム命令が、配列aにアクセスして該配列のある要素の値を変数uに格納する配列読み取り命令を定義していることが判別されてもよい。しかしながら、配列インデックスxが記号的であり未知なので、任意の配列要素が選ばれてuに割り当てられることができると想定され、S1、S2、S3の和集合がuに関連付けられ、源セット２２４に格納されてもよい。この想定は、この単純なデータ源解析プロセスの精度を劣化させうる。コード行１１７が読まれてもよく、この命令が、記号変数yに依存する記号的な配列インデックス書き込み命令を定義していることが判別されてもよい。しかしながら、配列インデックスyは記号的であり、未知なので、任意の配列要素が選ばれうると想定され、qが選ばれた配列要素に書き込まれうる。こうして、S1、S2、S3の和集合がプログラム実行状態のこの点において各配列要素に関連付けられてもよく、源セット２２６、２２８、２３０、２３２に格納されてもよい。
【００２３】
図２のデータ構造は、いかにデータ源解析に基づく単純な逐次反復的な試験生成が膨大なメモリおよび計算時間を費消しうるかを例解している。たとえば、多くの源セットをもつ大きなプログラムは、膨大な量のメモリを消費しうる。同様に、源セットの間の合併、等価性検査および包含検査のような源セット操作の数の多さから、大きな時間オーバーヘッドが帰結しうる。さらに、データ源解析に基づく単純な逐次反復的な試験生成は、記号的な配列インデックスをサポートしない。このことは、配列の任意の要素がアクセスされることができるという想定を強制し、データ源解析の精度の有意な劣化につながりうる。
【００２４】
本稿に記載される少なくとも一つの実施形態に基づく、データ源解析の、より洗練されたプロセスについて、ここで図３を参照して説明する。図３は、図１の例示的プログラム１００と、該より洗練されたデータ源解析プロセスの間に生成される対応するデータ構造３００とを示している。
【００２５】
データ構造３００は、源セット関数３０２、３０４、３０６、３０８、３１０、３１２、３１４、３１６、３１８、３２０（以下、「源セット関数３０２〜３２０」）を含んでいてもよい。これらはそれぞれ変数x、y、z、p、q、r、a、t、uおよびプログラム１００の命令において定義されるそれらの関連する値に関連付けられ、入力変数x、y、zを用いて書かれてもよい。源セット関数３０２〜３２０は、図２に示される源セット２０２〜２３２から、源セットをブーリアン関数にエンコードすることによって導出されてもよい。たとえば、源セット関数３０２、３０４、３０６において示されるように、ブーリアン変数s1、s2、s3がそれぞれ源セット要素S1、S2、S3に割り当てられてもよい。さらに、源セット関数３０２〜３２０のブーリアン変数は、二つ以上の源セット要素の合併を表わすためにブーリアンAND演算を通じて互いに関係付けられていてもよい。たとえば、源セット関数３１０は、ブーリアンAND演算を通じてs1∧s2として互いに関係付けられており、図２の源セット２１０{S1,S2}における源セット要素S1およびS2の合併に対応するブーリアン変数s1およびs2を含む。同様に、源セット関数３１２は、ブーリアンAND演算を用いてs1∧s2として関係付けられており、図２の源セット２１２{S1,S3}における源セット要素S1およびS3の合併に対応するブーリアン変数s1およびs3を含む。
【００２６】
一般に、源セットがS＝{Ss1,Ss2,…,Ssn}として定義される場合、源セットの源セット関数へのブーリアン関数エンコードはf(s)＝ss1∧ss2∧…∧ssnとなる。ここで、siは、それぞれの源セット要素Siを表わすブーリアン変数である。
【００２７】
源セット関数は、互いと一緒に操作されてもよい。たとえば、二つの源セットの合併を計算するために、それらの対応する源セット関数のブーリアンANDをf＝(f1∧f2)として計算してもよい。もう一つの例として、二つの源セットの包含は、
【数２】
0006701799.tif 000003
を計算し、この値が偽であるかどうかを調べることによって計算されてもよい。
【００２８】
さらに、単一の源セット関数が、上記の単純なデータ源解析の例において見たように配列の各要素に関連付けられた一意的な源セットではなく、配列に関連付けられてもよい。たとえば、配列についての源セット関数はfA(i,s)として定義されてもよい。ここで、iは配列インデックスをエンコードするブーリアン変数のベクトルi＝(i1,i2,…,im)である。たとえば、三要素の配列があり、それらの配列要素についての源セットが{S1}、{S1,S2}および{S2,S3}であるとする。二つのブーリアン変数または二つのビットi1およびi2が、三要素配列についての配列インデックスをエンコードするために使用されうる。このように、配列についての源セット関数は
【数３】
0006701799.tif 000004
と表現されてもよい。各配列要素についての個々の源セット関数は、配列の源セット関数から取り出されてもよい。たとえば、第二の配列要素についての源セット関数は、(i1,i2)＝(1,0)を源セット関数に割り当てることによって取り出されてもよい。すると、該源セット関数はfA(1,0,s)＝s1∧s2として集約される。一般に、k番目の配列要素についての源セット関数は、fA(k,s)またはfA(i,s)＝∨((i＝k)∧fk(s))によって計算されてもよい。
【００２９】
図３の源セット関数３１４は、配列aについての源セット関数
【数４】
0006701799.tif 000005
を示している。これは配列の第二の要素について一つ、配列の第三の要素について一つで、二つの源セット関数を含んでいる。各配列要素についての源セット関数は、配列インデックス(i1,i2)の、配列の各源セット関数とのブーリアンANDを計算することによって生成される。次いで、配列全体についての源セット関数は、配列の各要素の各源セット関数の間でブーリアンORを適用することによって計算される。
【００３０】
図３の源セット関数３１６は、配列インデックス(i1,i2)＝(1,0)を割り当てることによって配列源セット関数３１４から導出されてもよい。それにより配列源セット関数３１４は先述したようにs1∧s2に集約される。
【００３１】
図３の源セット関数３１８は、配列インデックス(i1,i2)＝(x1,x2)を割り当てることによって配列源セット関数３１４から導出されてもよい。こうして、図２に関して述べた単純なデータ源解析アプローチとは対照的に、このより洗練されたデータ源解析アプローチで配列にアクセスするために記号的な配列インデックスを使うことは、データ源解析の精度の劣化につながらないことがある。
【００３２】
図３の源セット関数３２０は、配列インデックス(i≠y)の、配列源セット関数３１４とのブーリアンANDを取り、次いで配列インデックス(i＝y)の、「q」についての源セット関数（s1∧s2）とのブーリアンANDを取り、これら二つの源セット関数の間のブーリアンORを計算することによって、配列源セット関数３１４から導出されてもよい。この例では、配列インデックス（i≠y）は
【数５】
0006701799.tif 000006
に変換されてもよく、配列インデックス（i＝y）は
【数６】
0006701799.tif 000007
に変換されてもよい。このように、プログラム実行状態のこの点での配列a全体についての源セット関数３２０は、
【数７】
0006701799.tif 000008
と定義されてもよい。
【００３３】
変数x、y、z、p、r、q、a、t、uについての源セット関数３０２〜３２０は、源セット関数を効率的に表現し、操作するために、それぞれのブーリアン変数を用いて単一の二分決定図グラフ構造において表現されてもよい。図４は、図３の源セット関数３０２〜３２０を表わす、共有される短縮された順序付けられた二分決定図（SROBDD）４００の一つの限定しない例を示す。しかしながら、図３の源セット関数３０２〜３２０の、あるいは他の源セット関数のグラフ表現は、他のグラフを使って達成されてもよい。該他のグラフには、二分決定図、縮小された順序付けられた二分決定図（reduced  ordered  binary  decision  diagram）、SROBDD、零抑制された決定図（zero-suppressed  decision  diagram）、二分モーメント図（binary  moment  diagram）、自由二分決定図（free  binary  decision  diagram）、パリティー決定図（parity  decision  diagram）、代数的決定図（algebraic  decision  diagram）、複数末端二分決定図（multiple  terminal  binary  decision  diagram）などが含まれる。
【００３４】
図４の例示的なSROBDD  ４００は、異なるブーリアン源セット関数が同様のサブ構造を共有することを許容することによって、空間オーバーヘッドを軽減しうる。さらに、SROBDD  ４００は、源セット関数の間の計算を単純にすることによって、時間オーバーヘッドをも軽減しうる。たとえば、源セット関数qと源セット関数tの等価性検査は、qおよびtが同じ初期子ノードを共有するかどうかを判定することによる一つの単純な計算において実行されうる。この場合、qおよびtは同じ初期子ノード４０２を共有し、よって互いに等価である。
【００３５】
図５は、本稿に記載される少なくとも一つの実施形態に従って構成された、ソフトウェア・プログラム（以下「プログラム」または「試験対象プログラム」）を試験する方法５００のフローチャートを示している。一般に、またいくつかの実施形態において、プログラムを試験する方法５００は、本稿に記載されるような逐次反復式の試験生成を含んでいてもよい。方法５００は、全体的または部分的に、たとえばコンピュータまたはプロセッサによって実行されてもよい。方法５００はブロック５０２「開始」において開始されてもよく、ブロック５１４「終了」において終了してもよい。ブロック５０２にはブロック５０４が続いてもよい。
【００３６】
ブロック５０４（「初期試験ドライバを生成し、入力変数に具体的な値を割り当て」）では、初期試験ドライバが生成されてもよく、具体的な値が選択され、試験対象プログラムの入力変数に割り当てられてもよい。任意の好適な具体的な値が随意に選択され、初期試験ドライバにおける入力変数に割り当てられてもよい。ブロック５０４にはブロック５０６が続いてもよい。
【００３７】
ブロック５０６（「データ源解析を用いた記号的実行」）では、初期試験ドライバは、記号的実行およびデータ源解析とともに使われて、プログラムの入力変数に割り当てられた具体的な値に基づいてプログラム実行経路の全部または実質的な数が実行されうるか否かを解析してもよい。入力変数に割り当てられた具体的な値に基づいてあるプログラム実行経路が実行され得ないことが判別されると、方法５００は、ブロック５１０を参照してより詳細に論じるように試験ドライバを向上させうる。ブロック５０６にはブロック５０８が続いてもよい。
【００３８】
ブロック５０８（「試験カバー範囲要求を満足？」）では、試験カバー範囲要求が満たされたかどうかを判定するためにプログラムが解析されてもよい。試験カバー範囲要求は、試験カバー範囲要求を満たすために解析される必要のあるプログラム実行経路の所定の数または割合を含んでいてもよい。少なくとも一つの実施形態では、試験カバー範囲要求は、試験対象プログラムのすべてのプログラム実行経路として定義されてもよい。他の実施形態では、試験カバー範囲要求は、解析される必要のある、すべてのプログラム実行経路のうちのある割合、たとえば75%または他の何らかの割合として定義されてもよい。さらに他の実施形態では、試験カバー範囲要求は時間制限によって定義されてもよい。時間制限に基づいて、いくつのプログラム実行経路が実行されうるかを決定してもよい。
【００３９】
ブロック５０８に続いて、方法５００は、試験カバー範囲要求が満たされたかどうかに依存して分岐してもよい。試験カバー範囲要求が満たされてないと判定される場合（図５のブロック５０８で「No」）、方法５００はブロック５１０に進んでもよい。試験カバー範囲要求が満たされていると判定される場合（図５のブロック５０８で「Yes」）、方法５００はブロック５１２に進んでもよい。
【００４０】
ブロック５１０（「識別された源変数を記号的にすることで試験ドライバを向上」）では、試験カバー範囲要求が満たされてないとの判定に応答して、ある種の入力変数を識別し、これらの入力変数を記号的にすることによって試験ドライバを向上させることによって、試験ドライバが向上されてもよい。たとえば、プログラムの条件文が、該条件文を真にし、該条件文に係るプログラム経路（単数または複数）を実行するためにある種の値をもつ必要があるある種の入力変数に依存することがある。該条件文を制御する入力変数を見出すためにデータ源解析が利用されてもよく、これらの入力変数が、向上された試験ドライバにおいて記号的にされてもよい。ブロック５１０には逐次反復のためにブロック５０６が続いてもよい。
【００４１】
ブロック５１２（「具体的な試験の組を生成」）では、試験カバー範囲要求が満たされたとの判定に応答して、プログラムを試験するために具体的な試験の組が生成されてもよい。ブロック５１２にはブロック５１４「終了」が続いてもよく、そこで方法５００は終了してもよい。
【００４２】
本稿に記載されるいくつかの実施形態は、コンピュータ可読命令が記憶されている非一時的なコンピュータ可読媒体を含む。命令は、図５の方法５００を実行するまたは該実行を制御するためにプロセッサによって実行可能であってもよい。
【００４３】
当業者は、この、および本稿に開示される他のプロセスおよび方法のために、該プロセスおよび方法において実行される機能が異なる順序で実装されてもよいことを理解するであろう。さらに、概説されたステップおよび動作は例として与えられているのみである。ステップおよび動作のいくつかは、開示される実装の本質を損なうことなく、任意的であったり、より少数のステップおよび動作に組み合わされたり、あるいは追加的なステップおよび動作に展開されたりしてもよい。
【００４４】
図６は、本稿に開示される少なくとも一つの実施形態に基づいて構成された、データ源解析を用いた記号的実行の例示的方法６００のフローチャートである。少なくとも一つの実施形態において、方法６００は、図５のブロック５０６（「データ源解析を用いた記号的実行」）に対応してもよい。方法６００は、全体的または部分的に、たとえばコンピュータまたはプロセッサによって実装されてもよい。方法６００はブロック６０２「開始」において開始されてもよく、ブロック６１８「終了」において終了してもよい。ブロック６０２にはブロック６０４が続いてもよい。
【００４５】
ブロック６０４（「現在命令を記号的に実行」）では、プログラムの現在命令は、プログラムの入力変数に割り当てられた記号的な源セット要素に基づいて記号的に実行されてもよい。ブロック６０４にはブロック６０６が続いてもよい。
【００４６】
ブロック６０６（「データ源？」）では、現在命令が解析されて、現在命令がデータ源（たとえば入力変数）を定義しているかどうかを判定する。ブロック６０６に続いて、方法６００は、現在命令がデータ源を定義しているかどうかに依存して分岐してもよい。現在命令がデータ源を定義していると判定される場合（図６のブロック６０６で「Yes」）、方法６００はブロック６０８に進んでもよい。現在命令がデータ源を定義していないと判定される場合（図６のブロック６０６で「No」）、方法６００はブロック６１０に進んでもよい。
【００４７】
ブロック６０８（「新しいブーリアン変数で新しい源セット関数を生成」）では、現在命令がデータ源を定義しているとの判定に応答して、現在命令について、該データ源についての新しいブーリアン変数を生成することによって、新しい源セット関数が生成されてもよい。
【００４８】
ブロック６１０（「新しい源セット関数を計算」）では、現在命令がデータ源を定義していないとの判定に応答して、現在命令について、新しい源セット関数が生成されてもよい。これは、該新しい源セット関数に係る前記一つまたは複数のブーリアン変数を識別し、前記一つまたは複数のブーリアン変数の間のブーリアン演算を定義することによる。ブロック６１０にはブロック６１２が続いてもよい。
【００４９】
ブロック６１２（「新しい源セット関数を命令と関連付け」）では、新しい源セット関数が、それが導出されるもとになった命令と関連付けられてもよい。ブロック６１２にはブロック６１４が続いてもよい。
【００５０】
ブロック６１４（「プログラム・カウンタをインクリメント」）では、プログラム・カウンタがインクリメントされてもよく、現在命令ポインタが解析のためのプログラム中の次の命令に進んでもよい。ブロック６１４にはブロック６１６が続いてもよい。
【００５１】
ブロック６１６（「プログラムの終わり？」）では、プログラムの終わりに達したかどうかを判定するためにプログラムが解析されてもよい。ブロック６１６に続いて、方法６００は、プログラムの終わりに達したかどうかに依存して分岐してもよい。プログラムの終わりに達していないと判定される場合（図６のブロック６１６で「No」）、方法６００は逐次反復のためにブロック６０４に進んでもよい。プログラムの終わりに達していると判定される場合（図６のブロック６１６で「Yes」）、方法６００はブロック６１８「終了」に進んでもよく、そこで方法６００は終了し、少なくとも一つの実施形態では、方法５００のブロック５０８に続いてもよい。
【００５２】
本稿に記載されるいくつかの実施形態は、コンピュータ可読命令が記憶されている非一時的なコンピュータ可読媒体を含む。命令は、図６の方法６００を実行するまたは該実行を制御するためにプロセッサによって実行可能であってもよい。
【００５３】
図７は、本稿に開示される少なくとも一つの実施形態に基づいて構成された、源セット関数計算の方法７００の例示的な流れ図である。少なくとも一つの実施形態において、方法７００は、図６のブロック６１０（「新しい源セット関数を計算」）に対応してもよい。方法７００は、全体的または部分的に、たとえばコンピュータまたはプロセッサによって実装されてもよい。方法７００はブロック７０２「開始」において開始されてもよく、ブロック７１６「終了」において終了してもよい。ブロック７０２にはブロック７０４が続いてもよい。
【００５４】
ブロック７０４（「配列書き込み？」）では、現在命令が配列書き込み命令を定義しているかどうかを判定するために現在命令が解析されてもよい。ブロック７０４に続いて、方法７００は、現在命令が配列書き込み命令を定義しているかどうかに依存して分岐してもよい。現在命令が配列書き込み命令を定義していると判定される場合（図７のブロック７０４で「Yes」）、方法７００はブロック７０６に進んでもよい。現在命令が配列書き込み命令を定義していないと判定される場合（図７のブロック７０４で「No」）、方法７００はブロック７１０に進んでもよい。
【００５５】
ブロック７０６（「書き込みデータに関連付けられた配列インデックスと源セット関数とのブーリアンANDを計算」）では、現在命令が配列書き込み命令を定義しているとの判定に応答して、配列の各要素について配列インデックスと源セット関数とのブーリアンANDが計算されてもよい。ブロック７０６にはブロック７０８が続いてもよい。
【００５６】
ブロック７０８（「配列に関連付けられた源セット関数を用いたブーリアンORを計算」）では、配列の各要素についての各源セット関数のブーリアンORが計算されて、配列源セット関数を完成させてもよい。ブロック７０８にはブロック７１６「終了」が続いてもよく、そこで方法７００は終了し、少なくとも一つの実施形態では、方法６００のブロック６１２に続いてもよい。
【００５７】
ブロック７１０（「配列読み取り？」）では、現在命令が配列書き込み命令を定義していないとの判定に応答して、現在命令が配列読み取り命令を定義しているかどうかを判定するために現在命令が解析されてもよい。ブロック７１０に続いて、方法７００は、現在命令が配列読み取り命令を定義しているかどうかに依存して分岐してもよい。現在命令が配列読み取り命令を定義していると判定される場合（図７のブロック７１０で「Yes」）、方法７００はブロック７１２に進んでもよい。現在命令が配列読み取り命令を定義していないと判定される場合（図７のブロック７１０で「No」）、方法７００はブロック７１４に進んでもよい。
【００５８】
ブロック７１２（「配列に関連付けられた源セット関数に配列インデックスを割り当て」）では、現在命令が配列読み取り命令を定義しているとの判定に応答して、配列源セット関数に配列インデックスが割り当てられてもよい。配列インデックスが具体的な値を割り当てられる場合、配列源セット関数は集約されてもよく、該配列の一つの要素について単一の源セット関数が帰結しうる。配列インデックスが記号変数を割り当てられる場合、記号変数が配列源セット関数におけるブーリアン配列インデックス変数を置換してもよい。ブロック７１２にはブロック７１６「終了」が続いてもよく、そこで方法７００は終了し、少なくとも一つの実施形態では、方法６００のブロック６１２に続いてもよい。
【００５９】
ブロック７１４（「オペランドに関連付けられた源セット関数の合併を計算」）では、現在命令が読み取りまたは書き込み命令を定義しておらず、非配列命令を定義しているとの判定に応答して、現在命令のオペランドに関連付けられたブーリアン変数の間にブーリアンAND演算を適用することによって、源セット関数の合併が計算されてもよい。ブロック７１４にはブロック７１６「終了」が続いてもよく、そこで方法７００は終了し、少なくとも一つの実施形態では、方法６００のブロック６１２に続いてもよい。
【００６０】
本稿に記載されるいくつかの実施形態は、コンピュータ可読命令が記憶されている非一時的なコンピュータ可読媒体を含む。命令は、図７の方法７００を実行するまたは該実行を制御するためにプロセッサによって実行可能であってもよい。
【００６１】
図８は、本稿に記載される少なくともいくつかの実施形態に基づいて構成された、データ源解析に基づく逐次反復的な試験生成のために構成されている例示的なコンピューティング装置８００を示すブロック図である。基本的構成８０２では、コンピューティング装置８００は典型的には一つまたは複数のプロセッサ８０４およびシステム・メモリ８０６を含む。プロセッサ８０４とシステム・メモリ８０６との間で通信するためにメモリ・バス８０８が使用されてもよい。
【００６２】
所望される構成に依存して、プロセッサ８０４は、これに限られないが、マイクロプロセッサ（μP）、マイクロコントローラ（μC）、デジタル信号プロセッサ（DSP）またはそれらの任意の組み合わせを含む任意の型のものであってもよい。プロセッサ８０４は、レベル１キャッシュ８１０およびレベル２キャッシュ８１２のような一つまたは複数レベルのキャッシュ、プロセッサ・コア８１４およびレジスタ８１６を含んでいてもよい。プロセッサ・コア８１４は、算術論理ユニット（ALU:  arithmetic  logic  unit）、浮動小数点ユニット（FPU:  floating  point  unit）、デジタル信号処理コア（DSPコア）またはそれらの任意の組み合わせを含んでいてもよい。例示的なメモリ・コントローラ８１８は、プロセッサ８０４と一緒に使用されてもよいし、あるいはいくつかの実装では、メモリ・コントローラ８１８はプロセッサ８０４の内部の部分であってもよい。
【００６３】
所望される構成に依存して、システム・メモリ８０６は、これに限られないが、揮発性メモリ（RAMなど）、不揮発性メモリ（ROM、フラッシュ・メモリなど）またはそれらの任意の組み合わせを含む任意の型のものであってよい。システム・メモリ８０６は、オペレーティング・システム８２０、一つまたは複数のアプリケーション８２２およびプログラム・データ８２４を含んでいてもよい。アプリケーション８２２は、逐次反復的な試験生成を実行するよう構成sらえた逐次反復試験アルゴリズム８２６を含んでいてもよい。プログラム・データ８２４は、試験対象プログラムおよび関連するROBDD  ８２８（図８では「プログラムおよびROBDD  ８２８」）または本稿に記載されるような試験対象プログラムと関連付けられた他の単一の二分決定図グラフ構造を含んでいてもよい。いくつかの実施形態では、アプリケーション８２２は、本稿に記載されたように図５〜図７の方法５００、６００、７００が提供されうるようオペレーティング・システム８２０上でプログラム・データ８２４とともに動作するよう構成されていてもよい。
【００６４】
コンピューティング装置８００は、基本的な構成８０２と関連する何らかの装置およびインターフェースとの間の通信を容易にするため、追加的な特徴または機能ならびに追加的なインターフェースを有していてもよい。たとえば、バス／インターフェース・コントローラ８３０が、記憶インターフェース・バス８３４を介して基本的な構成８０２と一つまたは複数のデータ記憶装置８３２との間の通信を容易にするために使われてもよい。データ記憶装置８３２はリムーバブル型記憶装置８３６、非リムーバブル型記憶装置８３８またはそれらの組み合わせであってもよい。リムーバブル型記憶装置および非リムーバブル型記憶装置の例は、少しだけ挙げれば、フレキシブル・ディスク・ドライブおよびハードディスク・ドライブ（HDD）のような磁気ディスク装置、コンパクト・ディスク（CD）ドライブまたはデジタル多用途ディスク（DVD）ドライブのような光学式ディスク・ドライブ、半導体ドライブ（SSD:  solid  state  drive）およびテープ・ドライブを含む。例示的なコンピュータ記憶媒体は、コンピュータ可読命令、データ構造、プログラム・モジュールまたは他のデータのような情報の記憶のために任意の方法または技術で実装される、揮発性および不揮発性、リムーバブル型および非リムーバブル型媒体を含んでいてもよい。
【００６５】
システム・メモリ８０６、リムーバブル型記憶装置８３６および非リムーバブル型記憶装置８３８はコンピュータ記憶媒体または非一時的なコンピュータ可読媒体の例である。コンピュータ記憶媒体はこれに限られないが、RAM、ROM、EEPROM、フラッシュ・メモリまたは他のメモリ技術、CD-ROM、デジタル多用途ディスク（DVD）または他の光学式記憶、磁気カセット、磁気テープ、磁気ディスク記憶または他の磁気記憶装置または所望される情報を記憶するために使用できコンピューティング装置８００によってアクセスできる他の任意の媒体を含んでいてもよい。そのような任意のコンピュータ記憶媒体または非一時的なコンピュータ可読媒体はコンピューティング装置８００の一部であってもよい。
【００６６】
コンピューティング装置８００は、さまざまなインターフェース装置（たとえば、出力装置８４２、周辺インターフェース８４４および通信装置８４６）から基本的な構成８０２への、バス／インターフェース・コントローラ８３０を介した通信を容易にするためにインターフェース・バス８４０をも含んでいてもよい。出力装置８４２は、グラフィック処理ユニット８４８およびオーディオ処理ユニット８５０を含む。これらは、一つまたは複数のA/Vポート８５２を介してディスプレイまたはスピーカーのようなさまざまな外部装置に通信するよう構成されていてもよい。周辺インターフェース８４４は、シリアル・インターフェース・コントローラ８５４またはパラレル・インターフェース・コントローラ８５６を含む。これらは、一つまたは複数のI/Oポート８５８を介して入力装置（たとえばキーボード、マウス、ペン、音声入力装置、タッチ入力装置など）、センサーまたは他の周辺装置（たとえばプリンタ、スキャナなど）のような外部装置と通信するよう構成されていてもよい。通信装置８４６はネットワーク・コントローラ８６０を含み、該ネットワーク・コントローラ８６０は、一つまたは複数の通信ポート８６４を介して、ネットワーク通信リンクを通じて、一つまたは複数の他のコンピューティング装置８６２との通信を容易にするよう構成されていてもよい。
【００６７】
ネットワーク通信リンクは、通信媒体の一例でありうる。通信媒体は、典型的には、コンピュータ可読命令、データ構造、プログラム・モジュールまたは搬送波もしくは他の転送機構のような変調されたデータ信号の形の他のデータによって具現されてもよく、任意の情報送達媒体を含んでいてもよい。「変調されたデータ信号」は、その特性の一つまたは複数が、当該信号内に情報をエンコードするような仕方で設定または変更される信号であってもよい。限定ではなく例として、通信媒体は、有線ネットワークまたは直接有線（direct-wired）接続のような有線媒体および音響、電波周波数（RF:  radio  frequency）、マイクロ波、赤外線（IR）および他の無線媒体のような無線媒体を含んでいてもよい。本稿で使われる「コンピュータ可読媒体」の用語は、記憶媒体および通信媒体の両方を含みうる。
【００６８】
コンピューティング装置８００は、スマートフォン、携帯情報端末（PDA）または特定用途向けデバイスといった小型形状因子のポータブル（またはモバイル）電子装置であってもよい。コンピューティング装置８００はまた、ラップトップ・コンピュータおよび非ラップトップ・コンピュータの構成の両方を含むパーソナル・コンピュータとして、あるいはラックマウント式のサーバー・コンピュータおよびブレード・サーバー・コンピュータ構成の両方を含むサーバー・コンピュータとして実装されてもよい。
【００６９】
本稿におけるあらゆる例および条件付きの言辞は読者が本発明および当該技術を発達させるために発明者によって寄与される概念を理解するのを助ける教育上の目的のために意図されており、そのように個別的に挙げられている例および条件に限定することなく解釈されるものとする。本発明の実施形態について詳細に記述してきたが、本発明の精神および範囲から外れることなく、それにさまざまな変更、置換および改変ができることは理解しておくべきである。
【００７０】
以上の実施例を含む実施形態に関し、さらに以下の付記を開示する。
（付記１）
ソフトウェア・プログラムを試験する方法であって：
前記ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に記号的な源セット要素を割り当てて、前記記号的な源セット要素に基づいてデータ構造を生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行する段階と；
前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行する段階とを含む、
方法。
（付記２）
前記データ構造が、前記記号的な源セット要素の一つまたは複数の間の合併を含む源セットを含む、付記１記載の方法。
（付記３）
前記データ構造が、前記源セットをブーリアン関数にエンコードすることによって生成される源セット関数を含み、前記ブーリアン関数は前記記号的な源セット要素を表わすブーリアン変数を含む、付記２記載の方法。
（付記４）
前記源セット関数が、前記記号的な源セット要素を表わすブーリアン変数および配列のインデックスを表わすブーリアン変数を含む配列源セット関数を含む、付記３記載の方法。
（付記５）
前記データ構造が図においてグラフで表現される、付記３記載の方法。
（付記６）
前記図が、二分決定図、縮小された順序付けられた二分決定図、共有された縮小された順序付けられた二分決定図、零抑制された決定図、二分モーメント図、自由二分決定図、パリティー決定図、代数的決定図または複数末端二分決定図のうちの一つを含む単一の図である、付記５記載の方法。
（付記７）
ソフトウェア・プログラムを試験する方法であって：
前記ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に記号的な源セット要素を割り当てて、前記記号的な源セット要素に基づいてデータ構造を生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行する段階と；
前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行し、各記号的な源セット要素にブーリアン変数を割り当てて各入力変数についての源セット関数を生成する段階とを含む、
方法。
（付記８）
前記現在命令についての源セット関数を計算する段階をさらに含む、付記７記載の方法。
（付記９）
前記現在命令が非配列命令を含み、前記現在命令についての源セット関数を計算する段階が、前記現在命令のオペランドに関連付けられた源セット関数の合併を計算することを含む、付記８記載の方法。
（付記１０）
前記現在命令が、源セット関数に関連付けられたデータを配列インデックスをもつ配列に書き込む配列書き込み命令を含み、前記現在命令についての源セット関数を計算する段階が：
前記配列インデックスを表わすブーリアン変数と前記書き込みデータに関連付けられた前記源セット関数のブーリアン変数との間のブーリアンAND演算を計算し；
前記配列の各要素に関連付けられた源セット関数の間のブーリアンOR演算を計算することを含む、
付記８記載の方法。
（付記１１）
前記現在命令が、源セット関数に関連付けられたデータを記号的な配列インデックスをもつ配列に書き込む配列書き込み命令を含み、前記現在命令についての源セット関数を計算する段階が：
前記記号的な配列インデックスと前記配列の前記源セット関数のブーリアン変数とのブーリアンAND演算を計算し；
前記配列の各要素に関連付けられた源セット関数の間のブーリアンOR演算を計算することを含む、
付記８記載の方法。
（付記１２）
前記現在命令が、配列インデックスをもつ配列からデータを読む配列読み取り命令を含み、前記現在命令についての源セット関数を計算する段階が、前記配列に関連付けられた前記源セット関数の前記配列インデックスに具体的な値を割り当てることを含む、付記８記載の方法。
（付記１３）
前記現在命令が、記号的な配列インデックスによって配列からデータを読む配列読み取り命令を含み、前記現在命令についての源セット関数を計算する段階が、前記記号的な配列インデックスに関連付けられたブーリアン変数を前記配列インデックスに関連付けられたブーリアン変数に割り当てることを含む、付記８記載の方法。
（付記１４）
前記データ源解析を実行することがさらに、前記現在命令が、前記ソフトウェア・プログラムの前記一つまたは複数の入力変数に割り当てられた前記具体的な値に基づいて満足されることができない条件文を含むかどうかを判定することを含む、付記７記載の方法。
（付記１５）
前記現在命令が前記ソフトウェア・プログラムの前記一つまたは複数の入力変数に割り当てられた前記具体的な値に基づいて満足されることができない条件文を含むと判定することに応答して、前記ソフトウェア・プログラムについての試験カバー範囲要求が満たされたかどうかを判定する段階と；
前記試験カバー範囲要求が満たされていないと判定するのに応答して、前記条件文を制御する入力変数を特定し、特定された入力変数を記号的にすることによって前記試験ドライバを向上させる段階とをさらに含む、
付記１４記載の方法。
（付記１６）
前記ソフトウェア・プログラムについての前記試験カバー範囲要求が満たされていると判定するのに応答して、前記ソフトウェア・プログラムについての具体的な試験の組を生成する段階をさらに含む、付記１５記載の方法。
（付記１７）
前記データ構造が、二分決定図、縮小された順序付けられた二分決定図、共有された縮小された順序付けられた二分決定図、零抑制された決定図、二分モーメント図、自由二分決定図、パリティー決定図、代数的決定図または複数末端二分決定図のうちの一つを含む単一の図においてグラフで表現される、付記７記載の方法。
（付記１８）
コンピュータ可読命令が記憶されている非一時的なコンピュータ可読媒体であって、前記命令は、
ソフトウェア・プログラムの入力変数に具体的な値を割り当てることによって試験ドライバを生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に記号的な源セット要素を割り当てて、前記記号的な源セット要素に基づいてデータ構造を生成する段階と；
前記ソフトウェア・プログラムの前記入力変数に割り当てられた前記具体的な値および記号的な源セット要素に基づいて前記ソフトウェア・プログラムの現在命令を記号的に実行する段階と；
前記ソフトウェア・プログラムが一つまたは複数の所定の要件を満たすかどうかを試験するために、前記現在命令の記号的実行に基づいて前記ソフトウェア・プログラムの前記現在命令に対してデータ源解析を実行する段階とを含む
動作を実行するまたは該動作の実行を制御するようプロセッサによって実行可能である、
非一時的なコンピュータ可読媒体。
（付記１９）
前記データ構造が：
前記記号的な源セット要素の一つまたは複数の間の合併を含む源セット；
前記源セットをブーリアン関数にエンコードすることによって生成される源セット関数であって、前記ブーリアン関数は前記記号的な源セット要素を表わすブーリアン変数を含む、源セット関数；および
配列源セット関数であって、前記配列源セット関数の前記記号的な源セット要素を表わすブーリアン変数および前記配列源セット関数のインデックスを表わすブーリアン変数を含む、配列源セット関数を含む、
付記１８記載の非一時的なコンピュータ可読媒体。
（付記２０）
前記データ構造が、二分決定図、縮小された順序付けられた二分決定図、共有された縮小された順序付けられた二分決定図、零抑制された決定図、二分モーメント図、自由二分決定図、パリティー決定図、代数的決定図または複数末端二分決定図のうちの一つを含む単一の図においてグラフで表現される、付記１８記載の非一時的なコンピュータ可読媒体。
【符号の説明】
【００７１】
５００  方法
５０２  開始
５０４  初期試験ドライバを生成し、入力変数に具体的な値を割り当て
５０６  データ源解析を用いた記号的実行
５０８  試験カバー範囲要求を満足？
５１０  識別された源変数を記号的にすることで試験ドライバを向上
５１２  具体的な試験の組を生成
５１４  終了
６００  方法
６０２  開始
６０４  現在命令を記号的に実行
６０６  データ源？
６０８  新しいブーリアン変数で新しい源セット関数を生成
６１０  新しい源セット関数を計算
６１２  新しい源セット関数を命令と関連付け
６１４  プログラム・カウンタをインクリメント
６１６  プログラムの終わり？
６１８  終了
７００  方法
７０２  開始
７０４  配列書き込み？
７０６  配列インデックスと書き込みデータに関連付けられた源セット関数とのブーリアンANDを計算
７０８  配列に関連付けられた源セット関数のブーリアンORを計算
７１０  配列読み取り？
７１２  配列に関連付けられた源セット関数に配列インデックスを割り当て
７１４  オペランドに関連付けられた源セット関数の合併を計算
８００  コンピューティング装置
８０２  基本的構成
８０４  プロセッサ
８０６  システム・メモリ
８０８  メモリ・バス
８１０  L1キャッシュ
８１２  L2キャッシュ
８１４  プロセッサ・コア
８１６  レジスタ
８１８  メモリ・コントローラ
８２２  アプリケーション
８２４  プログラム・データ
８２６  逐次反復的試験アルゴリズム
８２８  プログラムおよびROBDD
８３０  バス／インターフェース・コントローラ
８３２  記憶装置
８３４  記憶インターフェース・バス
８３６  リムーバブル記憶
８３８  非リムーバブル記憶
８４０  インターフェース・バス
８４２  出力装置
８４４  周辺インターフェース
８４６  通信装置
８４８  グラフィック処理ユニット
８５０  オーディオ処理ユニット
８５２  A/Vポート
８５４  シリアル・インターフェース・コントローラ
８５６  パラレル・インターフェース・コントローラ
８５８  I/Oポート
８６０  ネットワーク・コントローラ
８６２  他のコンピューティング装置
８６４  通信ポート
【図１】
0006701799.tif 000009
【図２】
0006701799.tif 000010
【図３】
0006701799.tif 000011
【図４】
0006701799.tif 000012
【図５】
0006701799.tif 000013
【図６】
0006701799.tif 000014
【図７】
0006701799.tif 000015
【図８】
0006701799.tif 000016