(57)【要約】      （修正有）【課題】ソフトウェアプログラムの不適切な又は冗長なコードフラグメントのシンボリック実行を減少しうる検証ツールを提供する。【解決手段】ソフトウェアプログラムのＦＵＡ（Ｆｕｎｃｔｉｏｎ  Ｕｎｄｅｒ  Ａｎａｌｙｓｉｓ）パスを生成する３０４。ＦＵＡパスがＦＵＡに対する新しいカバー率を生成するか否かを判定する３０６。ＦＵＡパスが新しいカバー率を生成することに応じて、ＦＵＡパスからＦＵＡパスステートメントを選択する３０８。ＦＵＡのカバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能であるか否かをカバーされているＦＵＡコードフラグメントの集合に少なくとも部分的に基づいて判定する３１０。カバーされていないコードフラグメントが選択されたパスステートメントから到達可能であることに応じて、選択されたＦＵＡパスステートメントをカバーされているステートメントの集合に追加する３１２。【選択図】図３Ａ
2015219907.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアプログラムの少なくとも一部分を受信し、前記受信された前記ソフトウェアプログラムの一部分は解析中の関数（ＦＵＡ）を含み、
前記受信された前記ソフトウェアプログラムの一部分に含まれる一つ又は複数の関数を通るパスに少なくとも部分的に基づいてＦＵＡパスを生成し、
前記ＦＵＡパスが前記ＦＵＡに対する新しいカバー率を生成するか否かを判定し、
前記ＦＵＡパスが新しいカバー率を生成することに応じて、前記ＦＵＡパスからＦＵＡパスステートメントを選択し、
前記ＦＵＡのカバーされていないコードフラグメントが前記選択されたＦＵＡパスステートメントから到達可能であるか否かをカバーされているＦＵＡコードフラグメントの集合に少なくとも部分的に基づいて判定し、
前記カバーされていないコードフラグメントが前記選択されたＦＵＡパスステートメントから到達可能であることに応じて、前記選択されたＦＵＡパスステートメントをカバーされているステートメントの集合に追加すること、
を含む、ソフトウェアプログラム検証方法。
【請求項２】
前記ＦＵＡパスが新しいカバー率を生成しないことに応じて、前記受信された前記ソフトウェアプログラムの一部分に含まれる部分パスの集合を更新することをさらに含む、請求項１に記載のソフトウェアプログラム検証方法。
【請求項３】
前記ＦＵＡパスが追加のＦＵＡパスステートメントを含むか否かを判定し、
前記ＦＵＡパスが前記追加のＦＵＡパスステートメントを含むことに応じて、前記ＦＵＡパスから前記追加のＦＵＡパスステートメントを選択し、
前記ＦＵＡの他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であるか否かを判定し、
前記他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であることに応じて、前記選択された追加のＦＵＡパスステートメントを前記カバーされているステートメントの集合に追加すること、
をさらに含む、請求項１に記載のソフトウェアプログラム検証方法。
【請求項４】
前記ＦＵＡパスが他のＦＵＡパスステートメントを含まないことに応じて、カバーされているＦＵＡフラグメントの集合を更新し、
前記ＦＵＡがカバーされているか否かを判定し、
前記ＦＵＡがカバーされていないことに応じて、部分パスの集合を更新すること、
をさらに含む、請求項３に記載のソフトウェアプログラム検証方法。
【請求項５】
資源制約があるか又は前記受信された前記ソフトウェアプログラムの一部分に他のパスがないか否かを判定し、
資源制約があること又は他のパスがないことに応じて、前記ＦＵＡのシンボリック実行を停止すること、
をさらに含む、請求項４に記載のソフトウェアプログラム検証方法。
【請求項６】
資源制約がないこと又は存続パスがあることに応じて、
前記部分パスの集合内に存続する他のパスを選択し、
前記選択されたパスに含まれたパスステートメントを選択し、
前記選択されたパスステートメントがカバーされているか否かを前記カバーされているステートメントの集合に少なくとも部分的に基づいて判定し、
前記選択されたパスステートメントがカバーされていないことに応じて、前記選択されたパスステートメントをシンボリックに実行し、
前記選択されたパスステートメントがカバーされていることに応じて、ＦＵＡパスを生成するために前記選択されたパスステートメントを使用すること、
をさらに含む、請求項５に記載のソフトウェアプログラム検証方法。
【請求項７】
前記ＦＵＡパスが追加のＦＵＡパスステートメントを含むか否かを判定し、
前記ＦＵＡパスが前記追加のＦＵＡパスステートメントを含まないことに応じて、
カバーされているＦＵＡフラグメントの集合を更新し、
前記ＦＵＡがカバーされているか否かを判定し、
前記ＦＵＡがカバーされていることに応じて、前記ＦＵＡのシンボリック実行を停止すること、
をさらに含む、請求項１に記載のソフトウェアプログラム検証方法。
【請求項８】
前記ＦＵＡが新しいカバー率を生成しないことに応じて、前記ＦＵＡパスが追加のＦＵＡパスステートメントを含むか否かを判定し、
前記ＦＵＡパスが前記追加のＦＵＡパスステートメントを含むことに応じて、前記追加のＦＵＡパスステートメントを選択し、
前記ＦＵＡの他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であるか否かを判定し、
前記他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であることに応じて、前記選択された追加のＦＵＡパスステートメントを前記カバーされているステートメントの集合に追加すること、
をさらに含む、請求項１に記載のソフトウェアプログラム検証方法。
【請求項９】
前記ＦＵＡのカバー率は、関数カバー率、ステートメントカバー率、分岐カバー率、パスカバー率、ラインカバー率、判定カバー率、条件カバー率、状態カバー率、修正された条件又は判定カバー率（ＭＣＤＣ）、並びにパラメータ値カバー率のうちの一つ又は複数に従って評価される、請求項１に記載のソフトウェアプログラム検証方法。
【請求項１０】
前記ＦＵＡパスが新しいカバー率を生成することに応じて、ＦＵＡ解析レポートを生成するために前記ＦＵＡパスを解析することをさらに含む、請求項１に記載のソフトウェアプログラム検証方法。
【請求項１１】
ソフトウェアプログラムの少なくとも一部分を受信し、前記受信された前記ソフトウェアプログラムの一部分は解析中の関数（ＦＵＡ）を含み、
前記受信された前記ソフトウェアプログラムの一部分に含まれた一つ又は複数の関数を通るパスに少なくとも部分的に基づいてＦＵＡパスを生成し、
前記ＦＵＡパスが前記ＦＵＡに対する新しいカバー率を生成するか否かを判定し、
前記ＦＵＡパスが新しいカバー率を生成することに応じて、前記ＦＵＡパスからＦＵＡパスステートメントを選択し、
前記ＦＵＡのカバーされていないコードフラグメントが前記選択されたＦＵＡパスステートメントから到達可能であるか否かをカバーされているコードフラグメントの集合に少なくとも部分的に基づいて判定し、
前記カバーされていないコードフラグメントが前記選択されたＦＵＡパスステートメントから到達可能であることに応じて、前記選択されたＦＵＡパスステートメントをカバーされているステートメントの集合に追加すること、
を含む動作を行うためのプロセッサによって実行可能なプログラミングコードをコード化されて有する非一時的なコンピュータ読取り可能媒体。
【請求項１２】
前記動作は、前記ＦＵＡパスが新しいカバー率を生成しないことに応じて、前記受信された前記ソフトウェアプログラムの一部分に含まれる部分パスの集合を更新することを含む、請求項１１に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１３】
前記動作は
前記ＦＵＡパスが追加のＦＵＡパスステートメントを含むか否かを判定し、
前記ＦＵＡパスが前記追加のＦＵＡパスステートメントを含むことに応じて、前記ＦＵＡパスから前記追加のＦＵＡパスステートメントを選択し、
前記ＦＵＡの他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であるか否かを判定し、
前記他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であることに応じて、前記選択された追加のＦＵＡパスステートメントを前記カバーされているステートメントの集合に追加すること、
をさらに含む、請求項１１に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１４】
前記動作は
前記ＦＵＡパスが他のＦＵＡパスステートメントを含まないことに応じて、カバーされているＦＵＡフラグメントの集合を更新し、
前記ＦＵＡがカバーされているか否かを判定し、
前記ＦＵＡがカバーされていないことに応じて、部分パスの集合を更新すること、
をさらに含む、請求項１３に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１５】
前記動作は
資源制約があるか又は前記受信された前記ソフトウェアプログラムの一部分に他のパスがないか否かを判定し、
資源制約があること又は他のパスがないことに応じて、前記ＦＵＡのシンボリック実行を停止すること、
をさらに含む、請求項１４に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１６】
前記動作は、資源制約がないこと又は存続パスがあることに応じて、
前記部分パスの集合内に存続する他のパスを選択し、
前記選択されたパスに含まれたパスステートメントを選択し、
前記選択されたパスステートメントがカバーされているか否かを前記カバーされているステートメントの集合に少なくとも部分的に基づいて判定し、
前記選択されたパスステートメントがカバーされていないことに応じて、前記選択されたパスステートメントをシンボリックに実行し、
前記選択されたパスステートメントがカバーされていることに応じて、ＦＵＡパスを生成するために前記選択されたパスステートメントを使用すること、
をさらに含む、請求項１５に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１７】
前記動作は
前記ＦＵＡパスが追加のＦＵＡパスステートメントを含むか否かを判定し、
前記ＦＵＡパスが前記追加のＦＵＡパスステートメントを含まないことに応じて、
カバーされているＦＵＡフラグメントの集合を更新し、
前記ＦＵＡがカバーされているか否かを判定し、
前記ＦＵＡがカバーされていることに応じて、前記ＦＵＡのシンボリック実行を停止すること、
をさらに含む、請求項１１に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１８】
前記動作は
前記ＦＵＡが新しいカバー率を生成しないことに応じて、前記ＦＵＡパスが追加のＦＵＡパスステートメントを含むか否かを判定し、
前記ＦＵＡパスが前記追加のＦＵＡパスステートメントを含むことに応じて、前記追加のＦＵＡパスステートメントを選択し、
前記ＦＵＡの他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能か否かを判定し、
前記他のカバーされていないフラグメントが前記選択された追加のＦＵＡパスステートメントから到達可能であることに応じて、前記選択された追加のＦＵＡパスステートメントを前記カバーされているステートメントの集合に追加すること、
をさらに含む、請求項１１に記載の非一時的なコンピュータ読取り可能媒体。
【請求項１９】
前記ＦＵＡのカバー率は、関数カバー率、ステートメントカバー率、分岐カバー率、パスカバー率、ラインカバー率、判定カバー率、条件カバー率、状態カバー率、修正された条件又は判定カバー率（ＭＣＤＣ）、並びにパラメータ値カバー率のうちの一つ又は複数に従って評価される、請求項１１に記載の非一時的なコンピュータ読取り可能媒体。
【請求項２０】
前記動作は、前記ＦＵＡパスが新しいカバー率を生成することに応じて、ＦＵＡ解析レポートを生成するために前記ＦＵＡパスを解析することをさらに含む、請求項１１に記載の非一時的なコンピュータ読取り可能媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本明細書で説明される実施の形態は、ソフトウェアプログラムの検証（ｓｏｆｔｗａｒｅ  ｐｒｏｇｒａｍ  ｖｅｒｉｆｉｃａｔｉｏｎ）におけるパス実行減少（ｐａｔｈ  ｅｘｅｃｕｔｉｏｎ  ｒｅｄｕｃｔｉｏｎ）に関する。
【発明の概要】
【発明が解決しようとする課題】
【０００２】
電子機器の使用が増加するにつれて、それらの機器で実行されるソフトウェアプログラムの数も増加する。通常、ソフトウェアプログラムが開発される場合には、そのソフトウェアプログラムがソフトウェアプログラムに対する所定の要件のすべてを満たすことを確保する（ａｓｓｕｒｅ）のを役立つ（ｈｅｌｐ）ことが検証される。ソフトウェアプログラムがすべての所定の要件を満たすか否かを判定するためにテストケースを開発することは、困難でかつ時間がかかることがありうる。
【０００３】
ここで請求される主題は、任意の難点を解決する又は上記のような環境においてだけ動作する実施の形態には限定されない。むしろ、この背景技術は、ここで説明されるいくつかの実施の形態が実施されうる一つの例示の技術領域を示すために提供されるにすぎない。
【課題を解決するための手段】
【０００４】
一つの実施の形態の一つの態様によれば、ソフトウェアプログラムの検証のための方法は、ソフトウェアプログラムの少なくとも一部分を受信することを含む。受信されたソフトウェアプログラムの一部分は解析中の関数（ＦＵＡ：Ｆｕｎｃｔｉｏｎ  Ｕｎｄｅｒ  Ａｎａｌｙｓｉｓ）を含みうる。この方法は、受信されたソフトウェアプログラムの一部分に含まれる一つ又は複数の関数を通るパスに少なくとも部分的に基づいてＦＵＡパスを生成することを含みうる。この方法は、ＦＵＡパスがＦＵＡに対する新しいカバー率（ｃｏｖｅｒａｇｅ）を生成するか否かを判定することを含みうる。ＦＵＡパスが新しいカバー率を生成することに応じて、この方法はＦＵＡパスからＦＵＡパスステートメント（ＦＵＡ  ｐａｔｈ  ｓｔａｔｅｍｅｎｔ）を選択することを含みうる。この方法は、選択されたＦＵＡパスステートメントから到達可能（ｒｅａｃｈａｂｌｅ）か否かをＦＵＡのカバーされていないコードフラグメント（ｃｏｄｅ  ｆｒａｇｍｅｎｔ）がカバー（ｃｏｖｅｒ）されているＦＵＡコードフラグメントの集合（ｓｅｔ）に少なくとも部分的に基づいて判定することを含みうる。カバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能であることに応じて、この方法は選択されたＦＵＡパスステートメントをカバーされているステートメントの集合に追加することを含みうる。
【０００５】
実施の形態の目的及び利益は、少なくとも請求項において特に指摘される要素、特徴、及び組み合わせによって実現されかつ達成されるであろう。
【０００６】
上記の一般的な説明及び下記の詳細な説明は両方とも例示及び説明のためのものであり、請求されるように、発明を限定するものではない。
【０００７】
例示実施の形態が、添付図面の使用によりさらなる具体性及び詳細をもって記載されかつ説明されるであろう。
【図面の簡単な説明】
【０００８】
【図１】例示のソフトウェアプログラムの検証ツール（検証ツール）を示す図である。
【図２】図１の検証ツールとして実装されうる例示のコンピューティングデバイスを示す図である。
【図３Ａ】ソフトウェアプログラムの検証の例示の方法のフローチャートである図である。
【図３Ｂ】ソフトウェアプログラムの検証の例示の方法のフローチャートである図である。
【図４】図１の検証ツールによって解析されうる例示のクラスを示す図である。
【図５】図４のクラスをシンボリックに実行するように構成されうるシンボリックドライバーを示す図である。
【図６】図４のクラスに含まれる解析中の関数の制御フローグラフを示す図である。
【図７】図４のクラスのシンボリック実行ツリーを示す図である。
【発明を実施するための形態】
【０００９】
ここで説明されるいくつかの実施の形態は一般的にソフトウェアプログラムの検証に関する。いくつかの実施の形態では、ソフトウェアプログラムの検証ツール（検証ツール）はソフトウェアプログラムを解析しかつ検証するように構成されうる。例えば、検証ツールはソフトウェアプログラムの一つ又は複数のクラスで解析中の関数（ｆｕｎｃｔｉｏｎ  ｕｎｄｅｒ  ａｎａｌｙｓｉｓ）（ＦＵＡ）を解析するように構成されうる。検証ツールは、クラスのパスに少なくとも部分的に基づいて一つ又は複数のＦＵＡパスを生成しうる。検証ツールは、ＦＵＡパスのそれぞれがＦＵＡに対する新しいカバー率を生成するか否かを判定しうる。ＦＵＡパスの一つが新しいカバー率を生成することに応じて、検証ツールは一つのＦＵＡパスステートメントをＦＵＡパスから選択しうる。検証ツールは、選択されたＦＵＡパスステートメントから到達可能であるか否かをＦＵＡのカバーされていないコードフラグメントがカバーされているＦＵＡコードフラグメントの集合に少なくとも部分的に基づいて判定しうる。カバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能であることに応じて、検証ツールは、選択されたＦＵＡパスステートメントをカバーされているステートメントの集合に追加しうる。カバーされているステートメントの集合及びカバーされているＦＵＡコードステートメントの集合は、クラスの続いて解析されるパス及び続いて解析されるＦＵＡパスにおいて使用される。例えば、カバーされているステートメントが続いて解析されるパスの一つまたは複数が既にカバーされていることを示す場合には、検証ツールは続いて解析されるパスをシンボリックに実行することができない。追加的に又は代替的に、カバーされているＦＵＡコードフラグメントの集合が、続いて解析されるＦＵＡパスの一つ又は複数が既にカバーされていることを示す場合には、検証ツールはＦＵＡパスのさらなる解析を行うことができない。この実施の形態及び他の実施の形態は添付図面を参照して説明されるであろう。
【００１０】
図１は、例示のソフトウェアプログラムの検証ツール（検証ツール）１００のブロック図を示す。検証ツール１００は、ソフトウェアプログラム１０２及び／又はそれのある部分を、それらの欠陥（ｄｅｆｅｃｔｓ）を識別するために、検証しかつ解析するように構成されうる。一般に、検証ツール１００は、ソフトウェアプログラム１０２の一つ又は複数の実行を含む検証を行うように構成されうる。コードフラグメントは、パス又は部分パスと呼ばれうるシーケンスで実行されうる。ソフトウェアプログラム１０２のコードフラグメントの実行の間に、コードフラグメントの欠陥が現示されかつ識別されうる。
【００１１】
検証ツール１００は、シンボリック実行エンジン１０４を含みうる。シンボリック実行エンジン１０４は、シンボリック変数を使用してソフトウェアプログラム１０２のコードフラグメント又はそれのある部分をシンボリックに実行するように構成されうる。ソフトウェアプログラム１０２のシンボリック実行の間に、シンボリック実行エンジン１０４は、シンボリック変数に対する制約１０６の集合を蓄積しうる。制約１０６の集合は、どちらのパス（例えば、コードフラグメントのどちらのシーケンス）がソフトウェアプログラム１０２において実行されるかを指示するエクスプレッション（ｅｘｐｒｅｓｓｉｏｎ）を含みうる。例えば、制約１０６の集合のうちの一つの制約が真（ｔｒｕｅ）である場合には、ソフトウェアプログラム１０２は第１のパスに沿って進行し、そしてその制約が偽（ｆａｌｓｅ）である場合にはソフトウェアプログラム１０２は第２のパスに沿って進行しうる。
【００１２】
制約１０６の集合は、ソルバーモジュール（ｓｏｌｖｅｒ  ｍｏｄｕｌｅ）１０８に伝達されうる。ソルバーモジュール１０８は次に、特定の値（ｖａｌｕｅ）１１０に対する制約１０６の集合を解決（ｓｏｌｖｅ）しうる。シンボリック変数が特定の値１１０に等しい場合には、ソフトウェアプログラム１０２はソフトウェアプログラム１０２のパスを通じて進行する。特定の値１１０は値テストエンジン（Ｖａｌｕｅ  Ｔｅｓｔ  Ｅｎｇｉｎｅ）１１２に伝達されうる。値テストエンジン１１２は、特定の値１１０を使用してソフトウェアプログラム１０２又はそれのある部分を実行しうる。値テストエンジン１１２は、ソフトウェアプログラム１０２の欠陥を示すテスト結果１１４を出力しうる。
【００１３】
検証ツール１００に含まれる又はそれによって利用されるメトリック（ｍｅｔｒｉｃ）はカバー率（ｃｏｖｅｒａｇｅ）を含みうる。カバー率は、検証ツール１００によって行われる検証プロセスの間に実行される及び／又は解析されるソフトウェアプログラム１０２のコードフラグメントの総数の一部分を示しうる。高いカバー率は、ソフトウェアプログラム１０２又はそれの上記部分が完全に解析されることを示しうる。低いカバー率は、ソフトウェアプログラム１０２又はそれの上記部分が完全には解析されないことを示しうる。検証ツール１００は、カバー率の一つ又は複数のタイプを最大化するように構成されうる。カバー率のタイプは、ステートメントカバー率、分岐カバー率、判定カバー率、条件カバー率、状態カバー率、パラメータ値カバー率、パスカバー率、修正条件又は判定カバー率（ＭＣＤＣ：Ｍｏｄｉｆｉｅｄ  ｃｏｎｄｉｔｉｏｎ／ｄｅｃｉｓｉｏｎ  ｃｏｖｅｒａｇｅ）、並びにラインカバー率（ｌｉｎｅ  ｃｏｖｅｒａｇｅ）を含みうるが、それらに限定されない。
【００１４】
カバー率を最大化することに加えて、検証ツール１００は、ソフトウェアプログラム１０２の検証の間に実行されるコードフラグメントの数を最小化するように構成されうる。解析の間に実行されるコードフラグメントの数を最小化することにより、検証ツール１００は、ソフトウェアプログラム１０２が解析される効率を増加しうる。具体的には、検証ツール１００は、不適切及び／又は冗長でありうるコードフラグメントの実行を減少するように構成されうる。
【００１５】
例えば、あらゆるコードフラグメントはシンボリックに実行されうる。あらゆるコードフラグメントを実行することにより、カバー率は高くなりうる。しかし、ソフトウェア検証は、同じコードフラグメントを複数回実行したこともありうるし又は関心のあるコードフラグメントの特定の集合の補助となるソフトウェアプログラム１０２の部分を実行したこともありうる。対照的に、検証ツール１００は、ソフトウェアプログラム１０２の適切なコードフラグメントのカバー率を最大化しながら、不適切な及び／又は冗長なコードフラグメントのシンボリック実行を減少しうる。
【００１６】
具体的には、ソフトウェアプログラム１０２はクラス１１６を含みうる。クラス１１６は、解析中の関数（ｆｕｎｃｔｉｏｎ  ｕｎｄｅｒ  ａｎａｌｙｓｉｓ）（ＦＵＡ）１１８、環境セットアップ１２０、及び呼び出された関数１２２を含みうる。ＦＵＡ１１８は、検証ツール１００によって行われる解析の間に関心のあるクラス１１６又はソフトウェアプログラム１０２の一部分を含みうる。例えば、ＦＵＡ１１８は、欠陥が識別されつつあるクラス１１６又はソフトウェアプログラム１０２の部分でありうる。環境セットアップ１２０は、クラス１１６の変数に値を割り当てる又は一般にＦＵＡ１１８のコンテキスト（ｃｏｎｔｅｘｔ）を設定する一つ又は複数のコンストラクタ（ｃｏｎｓｔｒｕｃｔｏｒｓ）を含みうる。呼び出された関数１２２は、呼び出される又はさもなければＦＵＡ１１８に含まれるメンバー関数を含みうる。
【００１７】
シンボリック実行エンジン１０４は、ＦＵＡ１１８をシンボリックに実行するように及びＦＵＡ１１８のカバー率を最大にするように構成されうる。さらに、シンボリック実行エンジン１０４は、ＦＵＡ１１８に含まれる冗長なコードフラグメントの実行を減少しかつ環境セットアップ１２０及び／又は呼び出された関数１２２に含まれるコードフラグメントの実行を減少するように構成されうる。
【００１８】
シンボリック実行エンジン１０４は、シンボリック実行モジュール１５０及びカバー率解析モジュール１５２を含みうる。シンボリック実行モジュール１５０は、カバー率解析モジュール１５２によって行われうるカバー率解析に関連してクラス１１６のシンボリック実行を行うように構成されうる。シンボリック実行モジュール１５０及びカバー率解析モジュール１５２は、クラス１１６の部分的に探索されたパスの各延長がＦＵＡ１１８のカバー率を改善するか否かを判定するように構成されうる。クラスの部分的に探索されたパスの拡張（ｅｘｔｅｎｓｉｏｎ）がＦＵＡ１１８のカバー率を改善しないことに応じて、クラス１１６の部分的に探索されたパスのシンボリック実行が停止されうる。したがって、ＦＵＡ１１８のカバー率を改善しないクラス１１６のパスは完全にシンボリックに実行されえない。
【００１９】
いくつかの実施の形態では、シンボリック実行モジュール１５０及びカバー率解析モジュール１５２は、ソフトウェアプログラム１０２で又は特にいくつかの実施の形態ではクラスでＦＵＡ１１８を受信しうる。シンボリック実行モジュール１５０及びカバー率解析モジュール１５２は、クラスに含まれたパスの部分集合をシンボリックに実行するように接続しうる。パスの部分集合は、ＦＵＡ１１８のカバー率を増加するステートメント及びコードフラグメントを含むことができかつ冗長な（ｒｅｄｕｎｄａｎｔ）又は不適切な（ｉｒｒｅｌｅｖａｎｔ）コードフラグメントを省略することができる。
【００２０】
例えば、カバー率解析モジュール１５２はＦＵＡパスを生成しうる。ＦＵＡパスは、ＦＵＡ１１８のコードフラグメントのシーケンスを含みうる。クラス１１６の一つ又は複数の部分的に探索されたパスは、単一のＦＵＡパスにマップ（ｍａｐ）しうる。ＦＵＡパスの生成は、クラス１１６のパス又は部分パス及び／又は下記の選択されたパス又は選択された部分パスのステートメントに少なくとも部分的に基づきうる。
【００２１】
カバー率解析モジュール１５２は、ＦＵＡパスがＦＵＡ１１８に対する新しいカバー率を生成するか否かを判定しうる。例えば、カバー率解析モジュール１５２は、ＦＵＡパスがＦＵＡ１１８に含まれたコードフラグメントの非冗長な（ｎｏｎ−ｒｅｄｕｎｄａｎｔ）及び／又は適切な（ｒｅｌｅｖａｎｔ）シーケンスを含むことを判定しうる。ＦＵＡパスが新しいカバー率を生成しないことに応じて、カバー率解析モジュール１５２はクラス１１６に含まれた部分パスの集合１３０を更新しうる。
部分パスの集合１３０を更新することは、ＦＵＡパスを生成するために使用されたパス又は部分パスを削除すること又は他の場合にはパス又は部分パスが探索されたことを示すことを含みうる。部分パスの集合は、シンボリック実行エンジン１０４あるいは他のアクセス可能なモジュール又はエンジンに含まれうるデータベース１５４に含まれうる。
【００２２】
ＦＵＡパスがＦＵＡ１１８に対する新しいカバー率を生成することに応じて、カバー率解析モジュール１５２はＦＵＡパスにおける一つ又は複数のステートメントを評価しうる。例えば、カバー率解析モジュール１５２はＦＵＡパスから第１のステートメントを選択しうる。カバー率解析モジュール１５２は、ＦＵＡ１１８のカバーされていないＦＵＡコードフラグメントが第１の選択されたステートメントから到達可能であるか否かを判定しうる。その判定は、例えば、ＦＵＡ１１８及び／又はカバーされているＦＵＡコードフラグメントの集合１３４に基づきうる。ＦＵＡコードフラグメントが第１の選択されたステートメントから到達可能であることに応じて、カバー率解析モジュール１５２は、第１の選択されたステートメントをカバーされているステートメントの集合１３２に追加しうる。カバーされていないＦＵＡコードフラグメントが第１の選択されたＦＵＡパスステートメントから到達可能でないことに応じて、カバー率解析モジュール１５２はＦＵＡパスの次のＦＵＡパスステートメントに移動しうる。カバー率解析モジュール１５２は、ＦＵＡパスの各ＦＵＡパスステートメントに対する評価を継続しうる。
【００２３】
ＦＵＡパスステートメントのそれぞれが評価された後で、カバー率解析モジュール１５２は、カバーされているＦＵＡカバーフラグメントの集合１３４を更新しうる。例えば、カバー率解析モジュール１５２は、どのＦＵＡコードフラグメントをＦＵＡパスがカバーするかを示しうる。カバー率解析モジュール１５２は次に、ＦＵＡ１１８が完全にカバーされるか否かを判定しうる。例えば、ＦＵＡカバーフラグメントのそれぞれがＦＵＡパス又はＦＵＡパスの組み合わせによってカバーされる場合には、カバー率解析モジュール１５２は、ＦＵＡが完全にカバーされることを判定しうる。ＦＵＡ１８が完全にカバーされることに応じて、カバー率解析モジュール１５２は、ＦＵＡ１１８及びクラス１１６のシンボリック実行を停止しうる。ＦＵＡ１１８が完全にカバーされることに応じて、カバー率解析モジュール１５２は部分パスの集合１３０を更新しうる。例えば、部分パスの集合１３０を更新することは、部分パスの集合１３０からＦＵＡパスを生成するために使用されるパス又は部分パスを削除すること及び／又はさもなければパス又は部分パスが完全に探索されていることを示すことを含みうる。部分パスの集合１３０を更新することによって、ＦＵＡパスを生成するために使用されるパスあるいは部分パスは続いて解析されること及び／又はシンボリックに実行されることができない。
【００２４】
さらに、シンボリック実行モジュール１５０は、資源制約（ｒｅｓｏｕｒｃｅ  ｃｏｎｓｔｒａｉｎｔ）があるか否か又はクラス１１６に他の（ｎｏ  ｍｏｒｅ）探索されていないパス又は部分パスがないか否かを判定しうる。資源制約は、例えば、計算スペース又は処理能力に対する制限を含みうる。他の探索されていないパス又は部分パスがないという判定は、部分パスの集合１３０に基づきうる。例えば、部分パスの集合１３０が他の部分的に探索されたパスを含まない場合には、探索されていないパス又は部分パスがそれ以上存在しないと判定されうる。資源制約が存在すること又は部分的に他の部分的に探索されたパスがないことに応じて、シンボリック実行モジュール１５０は、ＦＵＡ１１８およびクラス１１６のシンボリック実行を停止しうる。
【００２５】
資源制約がないこと又は他の探索されていないパスがあることに応じて、シンボリック実行モジュール１５０は、クラス１１６のパス又は部分パスを選択しうる。シンボリック実行モジュール１５０は、選択されたパスに含まれたパスステートメントを選択しうる。シンボリック実行モジュール１５０は、選択されたパスステートメントがカバーされているか否かをカバーされているステートメントの集合１３２に少なくとも部分的に基づいて判定しうる。選択されたパスステートメントがカバーされていないことに応じて、シンボリック実行モジュール１５０は、選択されたパスステートメントをシンボリックに実行しうる。選択されたパスステートメントがカバーされていることに応じて、シンボリック実行モジュール１５０は、選択されたパスステートメントをシンボリックに実行しえない。追加的に又は代替的に、選択されたパス及び／又は選択されたパスステートメントは他のＦＵＡパスを生成するために使用されうる。シンボリック実行モジュール１５０は、他のＦＵＡパスをカバー率解析モジュール１５２につなぎうる。カバー率解析モジュール１５２は、ここで説明されるようにＦＵＡ１１８のカバー率に対するＦＵＡパスステートメントを評価しうる。
【００２６】
上記のプロセスは一つ又は複数の停止条件が存在するまで継続しうる。停止条件は一つ又は複数を含みうるＦＵＡ１１８は完全にカバーされている。また、部分パスの集合１３０によって示されるようにクラス１１６には、他の探索されていない又は部分的に探索されたパス、資源制約の存在又はプレゼンス（ｐｒｅｓｅｎｃｅ）はない。
【００２７】
したがって、シンボリック実行エンジン１０４は、シンボリックに実行されるクラス１１６のパス及び／又は部分パスの数を減少しうる。具体的には、この又は他の実施の形態では、ＦＵＡパスがＦＵＡ１１８のカバー率を増加しないことに応じて、ＦＵＡパスを生成するために使用されるパス又は部分パスは部分パスの集合１３０から削除されるかあるいは部分パスの集合１３０内で探索されるように示されうる。さらに、カバーされているＦＵＡコードフラグメントの集合１３４は、ＦＵＡパスがＦＵＡ１１８の新しいカバー率を提供するか否かを判定するために使用される。したがって、既にカバーされているＦＵＡパス又は既にカバーされているＦＵＡコードフラグメントにマップする部分的にカバーされているパスのシンボリック実行はありえない。さらに、選択されたパスのパスステートメントがカバーされているか否かの判定は、カバーされているステートメントの集合１３２に基づきうる。したがって、先にカバーされているパスステートメントはシンボリックに実行されえない。
【００２８】
本開示の範囲から逸脱することなしに、検証ツール１００に対する修正、追加、又は省略がなされうる。具体的には、図１に示された実施の形態は、一つのクラス１１６、一つのＦＵＡ１１８、一つの環境セットアップ１２０、及び一つの呼び出された関数１２２を有する一つのソフトウェアプログラム１０２を含む。しかし、本開示は、一つ又は複数のソフトウェアプログラム１０２に適用されることができ、そのソフトウェアプログラム１０２の一つ又は複数は一つ又は複数のクラス１１６、一つ又は複数のＦＵＡ１１８、一つ又は複数の環境セットアップ１２０、一つ又は複数の呼び出された関数１２２、又はそれらの任意の組み合わせを含みうる。
【００２９】
さらに、ここで説明される実施の形態における種々のコンポーネントの分離は、その分離がすべての実施の形態において生ずることを示すものではない。さらに、説明されるコンポーネントは単一のコンポーネントに統合されあるいは複数のコンポーネントに分離されうることが本開示の利益と共に理解されうる。
【００３０】
シンボリック実行エンジン１０４、シンボリック実行モジュール１５０、カバー率解析モジュール１５２、値テストエンジン１１２、及びソルバーモジュール１０８は、ソフトウェアプログラムの検証のためのコード及びルーチン（ｒｏｕｔｉｎｅｓ）を含みうる。いくつかの実施の形態では、シンボリック実行エンジン１０４、シンボリック実行モジュール１５０、カバー率解析モジュール１５２、値テストエンジン１１２、及びソルバーモジュール１０８のうちの一つ又は複数は、例えば、一つ又は複数のコンピューティングデバイス上に格納されうる。いくつかの実施の形態では、検証ツール１００又はそれの任意のコンポーネントは、フィールドプログラマブルゲートアレイ（ＦＰＧＡ）又は特定用途向け集積回路（ＡＳＩＣ）を含むハードウェアを使用して実装されうる。いくつかの他の事例では、検証ツール１００又はそれの任意のコンポーネントは、ハードウェアとソフトウェアの組み合わせを使用して実装されうる。
【００３１】
検証ツール１００及び／又はそれの任意のコンポーネント（例えば、１０４、１５０、１５２、１５４、１１２、及び１０８）は、ここで説明される機能性を提供するためのデータ及び／又はコンピュータ命令を記憶するメモリ又は他の非一時的なコンピュータ媒体に格納されうる。メモリは、ダイナミックランダムアクセスメモリ（ＤＲＡＭ）デバイス、スタティックランダムアクセスメモリ（ＳＲＡＭ）デバイス、フラッシュメモリ、又はいくつかの他のメモリデバイスを含みうるストレージに含まれうる。いくつかの実施の形態では、ストレージはまたハードディスクドライブ、フレキシブルディスクドライブ、ＣＤ  ＲＯＭデバイス、ＤＶＤ  ＲＯＭデバイス、ＤＶＤ  ＲＡＭデバイス、ＤＶＤ  ＲＷデバイス、フラッシュメモリデバイス、又はより永続的なベースで情報を記憶するためのマスストレージデバイスのような不揮発性メモリ又は同様の永続ストレージデバイスを含む。
【００３２】
図２をここで参照すると、シンボリック実行モジュール１５０及びカバー率解析モジュール１５２の例がさらに詳細に示されている。図２は、シンボリック実行モジュール１５０、カバー率分析モジュール１５２、プロセッサ２２４、メモリ２２２、及び通信ユニット２２６を含むコンピューティングデバイス２５０のブロック図である。コンピューティングデバイス２５０のコンポーネントは、バス２２０によって通信可能に接続されうる。いくつかの実施の形態では、コンピューティングデバイス２５０は、図１の検証ツール１００を含むハ−ドウェアサーバー又はハ−ドウェアデバイスを含みうる。
【００３３】
図１及び図２を組み合わせて参照すると、プロセッサ２２４は、演算論理ユニット（ＡＬＵ）、マイクロプロセッサ、汎用コントローラ、又は計算及びソフトウェアプログラム解析を行うためのある他のプロセッサアレイを含みうる。プロセッサ２２４は、他のコンポーネント（例えば、１５０、１５２、２２６、及び２２２）との通信のためにバス２２０に接続されうる。プロセッサ２２４は一般に、データ信号を処理し、かつ複合命令セットコンピュータ（ＣＩＳＣ）アーキテクチャ、縮小命令セットコンピュータ（ＲＩＳＣ）アーキテクチャ、又は命令セットの組み合わせを実行するアーキテクチャを含む種々のコンピューティングアーキテクチャを含みうる。図２は単一のプロセッサ２２４を含むが、複数のプロセッサがコンピューティングデバイス２５０に含まれうる。他のプロセッサ、オペレーティングシステム、及び物理的構成が可能でありうる。
【００３４】
メモリ２２２は、プロセッサ２２４によって実行されうる及び／又は操作されうる命令及び／又はデータを記憶するように構成されうる。メモリ２２２は、他のコンポーネントとの通信のためにバス２２０に接続されうる。命令及び／又はデータは、ここで説明される技術又は方法を行うためのコードを含みうる。メモリ２２２は、ＤＲＡＭデバイス、ＳＲＡＭデバイス、フラッシュメモリ、又はある他のメモリデバイスを含みうる。いくつかの実施の形態では、コンピューティングデバイス２５０はまた、ハードディスクドライブ、フレキシブルディスクドライブ、ＣＤ  ＲＯＭデバイス、ＤＶＤ  ＲＯＭデバイス、ＤＶＤ  ＲＡＭデバイス、ＤＶＤ  ＲＷデバイス、フラッシュメモリデバイス、又はより恒常的に（ｐｅｒｍａｎｅｎｔ  ｂａｓｉｓ）情報を記憶するための他のマスストレージデバイスを含む不揮発性メモリ又は同様の永続ストレージデバイス及び媒体を含む。
【００３５】
図示された実施の形態では、メモリ２２２はデータベース１５４を含む。データベース１５４は、カバーされているステートメントの集合１３２、部分パスの集合１３０、カバーされているＦＵＡコードフラグメントの集合１３４、及びＦＵＡ解析レポート２３２を格納するように及び／又はそれらへのアクセスを可能にするように構成されうる。例えば、カバー率解析モジュール１５２及びシンボリック実行モジュール１５０は、カバーされているステートメントの集合１３２、部分パスの集合１３０、カバーされているＦＵＡコードフラグメントの集合１３４、及びＦＵＡ解析レポート２３２のうちの一つ又は複数にバス２２０によってアクセスしうる。カバー率解析モジュール１５２及びシンボリック実行モジュール１５０は、カバーされているステートメントの集合１３２、部分パスの集合１３０、カバーされているＦＵＡコードフラグメントの集合１３４、及びＦＵＡ解析レポート２３２のコンテンツを更新しうる。例えば、カバー率解析モジュール１５２及びシンボリック実行モジュール１５０は、カバーされているステートメントの集合１３２からのパスステートメントを削除又は追加しあるいはさもなければパスステートメントがカバーされているステートメントの集合１３２内でカバーされていることを示しうる。カバー率解析モジュール１５２及びシンボリック実行モジュール１５０は、特定のパスステートメントがカバーされているステートメントの集合１３２に含まれるか又はカバーされているステートメントの集合１３２においてカバーされているように示されるかを判定するためにカバーされているステートメントの集合１３２に続いてアクセスしうる。
【００３６】
いくつかの実施の形態では、データベース１５４又はカバーされているステートメントの集合１３２、部分パスの集合１３０、ＦＵＡ解析レポート２３２、カバーされているＦＵＡコードフラグメントの集合１３４、それらの部分、又はそれらのいくつかの組み合わせのようなそれのある部分は、コンピューティングデバイス２５０から遠隔に位置づけ（ｌｏｃａｔｅｄ  ｒｅｍｏｔｅｌｙ）られうる。データベース１５４又はそれの遠隔に位置づけられた部分は、コンピューティングデバイス２５０又はそれに含まれたモジュール（例えば、カバー率解析モジュール１５２及びシンボリック実行モジュール１５０）によってアクセスされうる。
【００３７】
通信ユニット２２６は、他のシステム又はサーバーにデータを送信しかつ他のシステム又はサーバーからデータを受信するように構成されうる。通信ユニット２２６はバス２２０に接続されうる。いくつかの実施の形態では、通信ユニット２２６は、通信ネットワークへの又は他の通信チャネルへの直接の物理的接続のためのポートを含む。例えば、通信ユニット２２６は、有線通信のためのＵＳＢ、ＳＤ、ＣＡＴ−５、又は同様のポートを含みうる。いくつかの実施の形態では、通信ユニット２２６は、ＩＥＥＥ８０２．１１、ＩＥＥＥ８０２．１６、ブルートゥース（ＢＬＥＴＯＯＴＨ）（登録商標）、又は他の適当な無線通信方法を含む一つ又は複数の無線通信方法を使用して通信チャネルによりデータを交換するための無線トランシーバーを含む。
【００３８】
いくつかの実施の形態では、通信ユニット２２６は、有線ポート及び／又は無線トランシーバーを含む。通信ユニット２２６はまた、トランスミッションコントロールプロトコル／インターネットプロトコル（ＴＣＰ／ＩＰ：Ｔｒａｎｓｍｉｓｓｉｏｎ  Ｃｏｎｔｒｏｌ  Ｐｒｏｔｏｃｏｌ／Ｉｎｔｅｒｎａｅｔ  Ｐｒｏｔｏｃｏｌ）、ＨＴＴＰ、ＨＴＴＰセキュア（ＨＴＴＰＳ）、及びシンプルメールトランスファープロトコル（ＳＭＴＰ：Ｓｉｍｐｌｅ  Ｍａｉｌ  Ｔｒａｎｓｆｅｒ  Ｐｒｏｔｏｃｏｌ）を含む標準ネットワークプロトコルを使用してファイル及び／又は他のデータの配信のための他の従来の接続を提供しうる。代替的に又は追加的に、通信ユニット２２６は、ショートメッセージサービス（ＳＭＳ：Ｓｈｏｒｔ  Ｍｅｅａｇｅ  Ｓｅｒｖｉｃｅ）、マルチメディアメッセージングサービス（ＭＭＳ：Ｍｕｌｔｉｍｅｄｉａ  Ｍｅｓａｇｉｎｇ  Ｓｅｒｖｉｃｅ）、ハイパーテキストトランスファープロトコル（ＨＴＴＰ：Ｈｙｐｅｒｔｅｘｔ  Ｔｒａｎｓｆｅｒ  Ｐｒｏｔｏｃｏｌ）、直接データ接続、ワイヤレスアプリケーションプロトコル（ＷＡＰ：Ｗｉｒｅｌｅｓｓ  Ａｐｐｌｉｃａｔｉｏｎ  Ｐｒｏｔｏｃｏｌ）、Ｅ−メール、又は他の適当なタイプの電子通信経由を含むセルラー通信ネットワークによってデータを送受信するためのセルラー通信ネットワークを含みうる。
【００３９】
図２の実施の形態では、シンボリック実行モジュール１５０は、通信モジュール２３４、選択モジュール２０４、判定モジュール２０６、生成モジュール２０８、実行モジュール２１０、及び更新モジュール２１２を含みうる。カバー率解析モジュール１５２は、カバー率判定モジュール２１４、ステートメント選択モジュール２１６、追加モジュール２１８、カバー率更新モジュール２２８、及び解析モジュール２３０を含みうる。通信モジュール２３４、選択モジュール２０４、判定モジュール２０６、生成モジュール２０８、実行モジュール２１０、更新モジュール２１２、カバー率判定モジュール２１４、ステートメント選択モジュール２１６、追加モジュール２１８、カバー率更新モジュール２２８、及び解析モジュール２３０は全体としてモジュール２４０と呼ばれる。
【００４０】
モジュール２４０のそれぞれは、一つ又は複数の動作を行うように構成された一つ又は複数のルーチンを含むソフトウェアとして実装されうる。モジュール２４０は、下記の機能性を提供するためにプロセッサ２２４によって実行可能な命令の集合を含みうる。いくつかの事例では、モジュール２４０は、コンピューティングデバイス２５０のメモリ２２２に格納されるかあるいは少なくとも一時的にロード（ｌｏａｄ）されることができ、プロセッサ２２４によってアクセス可能でかつ実行可能でありうる。モジュール２４０の一つ又は複数は、コンピューティングデバイス２５０のプロセッサ２２４及びコンポーネントとのバス２２０を介した協働及び通信のために適合（ａｄａｐｔｅｄ）されうる。
【００４１】
通信モジュール２３４は、シンボリック実行モジュール１５０及び／又はカバー率解析モジュール１５２とコンピューティングデバイス２５０の他のコンポーネント（例えば、２２４、２２２、及び２２６）との間の通信を処理するように構成されうる。通信モジュール２３４は、データを通信ユニット２２６によって外部のシステムに送信及び受信するように構成されうる。いくつかの事例では、通信モジュール２３４は、それらのコンポーネントからのデータを通信ユニット２２６によって受信するように及び／又は転送するように他のモジュール（例えば、２０４、２０６、２０８、２１０、２１２、２１４、２１６、２１８、２２８、及び２３０）と協働しうる。例えば、シンボリック実行エンジン１５０の通信モジュール２３４は、ソフトウェアプログラム１０２の一部分を受信するように構成されうる。受信されたソフトウェアプログラム１０２の一部分はクラス１１６を含みうる。クラス１１６は、ＦＵＡ１１８、環境セットアップ１２０、及び呼び出された関数１２２を含みうる。通信モジュール２３４は、クラス１１６に含まれたパス及び部分パスをカバー率解析モジュール１５２及びデータベース１５４に伝達するように構成されうる。さらに、通信モジュール２３４は、クラス１１６およびＦＵＡ１１８をカバー率解析モジュール１５２に伝達するように構成されうる。これらの及び他の実施の形態では、ＦＵＡ１１８、環境セットアップ１２０、及び呼び出された関数１２２は、カバー率解析モジュール１５２及び／又はシンボリック実行モジュール１５０によってアクセス可能でありうる。
【００４２】
選択モジュール２０４は、クラス１１６の一つのパス又は部分パスを選択するように構成されうる。選択モジュール２０４は、部分パスの集合１３０からパスまたは部分パスを選択するように構成されうる。例えば、部分パスの集合１３０から削除されるパス又は部分パスは選択されえない。追加的に又は代替的に、部分パスの集合１３０内で探索されたとして示されるパス又は部分パスは選択されえない。従って、選択されるパス又は部分パスは、シンボリックに実行されても又はさもなければ部分パスの集合１３０から探索されたとして示されてもいないパス又は部分パスの一つでありうる。選択モジュール２０４は次に、選択されたパス又は部分パスからパスステートメントを選択しうる。選択されたパスステートメントは判定モジュール２０６に伝達されうる。
【００４３】
判定モジュール２０６は、カバー率、資源制約の存在、及び部分パスの集合１３０におけるパス又は部分パスの存在に関する判定を行うように構成されうる。判定モジュール２０６は、選択されたパスステートメントを選択モジュール２０４から受信しうる。判定モジュール２０６は次に、選択されたパスステートメントがカバーされているか否かを判定しうる。いくつかの実施の形態では、判定モジュール２０６は、判定をカバーされているステートメントの集合１３２に少なくとも部分的に基づきうる。例えば、他のパスステートメントが、選択されたパスステートメントをもカバーするカバーされたステートメントの集合１３２に含まれうる。判定モジュール２０６は、カバーされているステートメントの集合１３２にアクセスすることができ、選択されたパスステートメントがカバーされている又はカバーされていないことを示すデータを読み取ることができる。選択されたパスステートメントがカバーされていることに応じて、判定モジュール２０６は、選択されたパスステートメントがカバーされていないことを示す信号を実行モジュール２１０に伝達しうる。選択されたパスステートメントがカバーされていることに応じて、判定モジュール２０６は、選択されたパスステートメントがカバーされていることを示す信号を生成モジュール２０８に伝達しうる。
【００４４】
実行モジュール２１０は、選択されたパスステートメントをシンボリックに実行するように構成されうる。実行モジュール２１０は次に、シンボリック実行の完了を示す信号を更新モジュール２１２に伝達しうる。更新モジュール２１２は次に部分パスの集合１３０を更新しうる。例えば、更新モジュール２１２は、部分パスの集合１３０に含まれるパス又は部分パスから選択されたパスステートメントを削除しうる。追加的に又は代替的に、更新モジュール２１２は、選択されたパスステートメントが実行されたこと及び／又は探索されたことを示すように部分パスの集合１３０を更新しうる。
【００４５】
判定モジュール２０６は次に、実行されても、削除されても、あるいはさもなければ探索されたとして示されてもいない部分パスの集合１３０内に存続する（ｒｅｍａｉｎ）パス又は部分パスがあるか否かを判定しうる。さらに、判定モジュール２０６は、資源制約が存在するか否かを判定しうる。部分パスの集合１３０内に存続パス又は部分パスがないという判定又は資源制約があるという判定に応じて、シンボリック実行モジュール１５０はＦＵＡ１１８及びクラス１１６のシンボリック実行を停止しうる。部分パスの集合１３０内に存続パス又は部分パスがあるという判定又は資源制約がないという判定に応じて、判定モジュール２０６は、部分パスの集合１３０内の存続パス又は部分パスを示す及び／又は資源制約が存在しないことを示す信号を選択モジュール２０４に伝達しうる。それに応じて、選択モジュール２０４は、部分パスの集合１３０の他のパス又は部分パスを選択しうる。選択モジュール２０４は、パス又は部分パスを生成モジュール２０８に伝達しうる。追加的に又は代替的に、選択モジュール２０４は他の選択されたパスステートメントを選択しうる。上記動作（ｏｐｅｒａｔｉｏｎｓ）の一つ又は複数がここで説明されるように反復されうる。
【００４６】
生成モジュール２０８は、選択モジュール２０４からのパス又は部分パス及び／又は判定モジュール２０６からの選択されたパスステートメントを受信しうる。生成モジュール２０８は、パス、部分パス、選択されたパスステートメント、又はそれらのある組み合わせからＦＵＡパスを生成するように構成されうる。追加的に又は代替的に、生成モジュール２０８はＦＵＡ１１８からＦＵＡパスを生成しうる。生成モジュール２０８はＦＵＡパスをカバー率解析モジュール１５２のカバー率判定モジュール２１４に伝達する。
【００４７】
カバー率判定モジュール２１４は、ＦＵＡパスがＦＵＡ１１８に対する新しいカバー率を生成するか否かを判定するように構成されうる。いくつかの実施の形態では、カバー率判定モジュール２１４は、ＦＵＡパスがＦＵＡ１１８に対する新しいカバー率を生成するか否かをカバーされているＦＵＡコードフラグメントの集合１３４に少なくとも部分的に基づいて判定しうる。カバーされているＦＵＡコードフラグメントの集合１３４は、他のＦＵＡパスの解析において判定されていることがありうる一つ又は複数のカバーされているＦＵＡコードフラグメントを含みうる。カバー率判定モジュール２１４は、カバーされているＦＵＡコードフラグメトをＦＵＡパスに含まれたコードフラグメントと比較しうる。ＦＵＡパスのコードフラグメントの実行がカバーされているＦＵＡコードフラグメントの集合１３４内のＦＵＡコードフラグメントのカバー率につながる（ｌｅａｄ  ｔｏ）場合には、カバー率判定モジュール２１４は、ＦＵＡパスがＦＵＡ１１８に対する新しいカバー率を生成しないと判定しうる。
【００４８】
ＦＵＡパスがＦＵＡ１１８の新しいカバー率を生成しないことに応じて、カバー率判定モジュール２１４は、ＦＵＡパスが新しいカバー率を生成しないことを示す信号を更新モジュール２１２に伝達しうる。更新モジュール２１２は部分パスの集合１３０を更新しうる。例えば、更新モジュール２１２は、ＦＵＡパスを生成するために使用される選択されたパス又は選択されたパスステートメントが探索されることを示しうる。その後で、判定モジュール２０６は、部分パスの集合１３０内に存続するパス又は部分パスがあるか否か又は資源制約が存在するか否かを判定しうる。シンボリック実行モジュール１５０は、パス又は部分パスが部分パスの集合内に存続せずあるいは資源制約が存在する場合には、ＦＵＡ１１８及び／又はクラス１１６のシンボリック実行を停止しうる。選択モジュール２０４は、部分パスの集合１３０内に存続するパス又は部分パスがあること及び／又は資源制約が存在しないことを示す判定モジュール２０６から伝達される信号に応答して、部分パスの集合１３０内に存続する他のパス又は他の部分パスを選択しうる。選択モジュール２０４は、ここで説明されるように他のパスステートメントをさらに選択することができ、選択された存続パス及び／又は選択されたパスステートメントに対して一つ又は複数の動作が反復されうる。
【００４９】
ＦＵＡパスが新しいカバー率を生成することに応じて、カバー率判定ジュール２１４は、ステートメント選択モジュール２１６及び解析モジュール２３０に信号を伝達しうる。解析モジュール２３０は、ＦＵＡパスのシンボリック解析を行うように構成されうる。例えば、シンボリック解析は、ＦＵＡパスに沿った順方向到達可能性解析及びＦＵＡパスのマークステートメントを行いうる。解析モジュール２３０は次にシンボリック解析の結果をＦＵＡ解析レポート２３２に伝達しうる。
【００５０】
ステートメント選択モジュール２１６は、ＦＵＡパスから一つのＦＵＡパスステートメントを選択するように構成されうる。ステートメント選択モジュール２１６は、選択されたＦＵＡパスステートメントをカバー率判定モジュール２１４に伝達しうる。カバー率判定モジュール２１４は、ＦＵＡ１１８のカバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能か否かを判定しうる。カバー率判定モジュール２１４は、判定をカバーされているＦＵＡコードフラグメント１３４及び／又はＦＵＡ１１８に少なくとも部分的に基づきうる。
【００５１】
カバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能であることに応じて、カバー率判定モジュール２１４は、カバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能であることを示す信号を追加モジュール２１８に伝達しうる。追加モジュール２１８は選択されたＦＵＡパスステートメントをカバーされているステートメント１３２に追加するように構成されうる。
【００５２】
追加モジュール２１８が選択されたＦＵＡパスステートメントをカバーされているステートメントの集合１３２に追加した後で又はカバーされていないコードフラグメントが選択されたＦＵＡパスから到達可能であることに応じて、カバー率判定モジュール２１４は、ＦＵＡパスが一つ又は複数の追加ＦＵＡパスステートメントを含むか否かを判定しうる。一つ又は複数の追加ＦＵＡパスがＦＵＡに含まれているとの判定に応じて、ステートメント選択モジュール２１６は、追加ＦＵＡパスステートメントのそれぞれを順に選択でき、カバー率判定モジュール２１４は、カバーされていないコードフラグメントが選択されたＦＵＡパスステートメントから到達可能であるか否かを次に判定でき、追加モジュール２１８は、上記の条件に応じて、選択されたＦＵＡパスステートメントをカバーされているステートメントの集合１３２に追加できる。
【００５３】
カバー率判定モジュール２１４がＦＵＡステートメントには追加ＦＵＡパスステートメントは含まれていないと判定することに応じて、カバー率判定モジュール２１４は、ＦＵＡ１１８がカバーされているか否かを判定しうる。ＦＵＡ１１８が完全にカバーされていることに応じて、カバー率解析モジュール１５２はＦＵＡ１１８及び／又はクラス１１６のシンボリック実行を停止するように構成されうる。ＦＵＡ１１８が完全にカバーされていないことに応じて、カバー率判定モジュール２１４は、更新モジュール２１２に信号を伝達しうる。更新モジュール２１２は部分パスの集合１３０を更新しうる。判定モジュール２０６は、部分パスの集合１３０内に存続するパス又は部分パスがあるか否か又は資源制約が存在するか否かを判定しうる。シンボリック実行モジュール１５０はＦＵＡ１１８及び／又はクラス１１６のシンボリック実行を停止しうる。選択モジュール２０４は、部分パスの集合１３０内に存続する他のパス又は他の部分パスを選択しうる。選択モジュール２０４は他のパスステートメントをさらに選択でき、ここで説明されるように選択された存続パス及び／又は選択されたパスステートメントに対して一つ又は複数の動作が反復されうる。
【００５４】
図３Ａ及び３Ｂは、ここで説明される少なくとも一つの実施の形態に従って構成された、ソフトウェアプログラム解析の例示の方法３００のフローチャートである。方法３００は、いくつかの実施の形態では、図２を参照して説明されるコンピューティングデバイス２５０によってプログラム可能に行われうる。追加的に又は代替的に、方法３００は、図１の検証ツール１００のような検証ツールによって行われうる。検証ツール１００及び／又はコンピューティングデバイス２５０は、方法３００を行うため又は方法３００の性能を生じさせるためにプロセッサによって実行可能なプログラミングコード又は命令を格納された又はコード化された非一時的なコンピュータ読取可能媒体（例えば、図２のメモリ２２２）を含みうるかあるいはそれに通信可能に接続されうる。検証ツール１００及び／又はコンピューティングデバイス２５０は、方法３００の性能（ｐｅｒｆｏｒｍａｎｃｅ）を発揮させる又はコントロールするコンピュータ命令を実行するように構成されるプロセッサ（例えば、図２のプロセッサ２２４）を含みうる。個別のブロックとして示されているが、種々のブロックは、所望の実装に応じて、分割して追加のブロックとされ、組み合わせてより少ないブロックとされ、あるいは除去されうる。
【００５５】
図３Ａを参照すると、方法３００は、ソフトウェアプログラムの少なくとも一部分が受信されるブロック３０２において開始する。受信されたソフトウェアプログラムの一部分はＦＵＡを含みうる。例えば、図１を参照すると、ソフトウェアプログラム１０２の一部分は、ＦＵＡ１１８をさらに含みうるクラス１１６を含みうる。ソフトウェアプログラム１０２のその部分は検証ツール１００によって受信されうる。
【００５６】
ブロック３０４において、ＦＵＡパスが生成されうる。いくつかの実施の形態では、ＦＵＡパスは、受信されたソフトウェアプログラムの一部分の選択された部分パス及び／又は選択されたパスに少なくとも部分的に基づいて生成されうる。例えば図２を参照すると、生成モジュール２０８は、クラス１１６の部分パスの集合１３０から選択モジュール２０４によって選択された部分パス及び／又はパスからＦＵＡパスを生成しうる。
【００５７】
ブロック３０６では、ＦＵＡパスがＦＵＡに対する新しいカバー率を生成するか否かが判定されうる。いくつかの実施の形態では、判定はカバーされているＦＵＡコードフラグメントの集合に基づきうる。例えば、図２を参照すると、カバー率判定モジュール２１４は、ＦＵＡパスが新しいカバー率を生成するか否かをカバーされているＦＵＡコードフラグメントの集合１３４に基づいて判定しうる。ＦＵＡパスが新しいカバー率を生成するという判定（ブロック３０６における“Ｙｅｓ”）に応じて、方法はブロック３０８及び／又は３３４へと進行しうる。ＦＵＡパスが新しいカバー率を生成しないという判定（ブロック３０６において“Ｎｏ”）に応じて、方法３００はブロック３２０へと進行しうる。
【００５８】
ブロック３０８において、ＦＵＡパスステートメントがＦＵＡパスから選択されうる。例えば、図１を参照すると、ステートメント選択モジュール２１６は、ＦＵＡパスからＦＵＡパスステートメントを選択しうる。ブロック３３４において、ＦＵＡパスが解析されうる。例えば、図２を参照すると、解析モジュール２３０はＦＵＡパスを解析し、ＦＵＡ解析レポート２３２を生成しうる。
【００５９】
ブロック３１０において、ＦＵＡのカバーされていないフラグメントが選択されたＦＵＡパスステートメントから到達可能であるか否かが判定されうる。いくつかの実施の形態では、その判定はカバーされているＦＵＡコードフラグメントの集合１３４に基づきうる。例えば、図２を参照すると、カバー率判定モジュール２１４は、ＦＵＡのカバーされていないフラグメントが選択されたＦＵＡパスステートメントから到達可能であるか否かをカバーされているＦＵＡコードフラグメントの集合に基づいて判定しうる。ＦＵＡのカバーされていないフラグメントが選択されたＦＵＡパスステートメントから到達可能であるという判定（ブロック３１０において“Ｙｅｓ”）に応じて、方法３００はブロック３１２へと進行しうる。ＦＵＡのカバーされていないフラグメントが選択されたＦＵＡパスステートメントから到達可能でないという判定（ブロック３１０において“Ｎｏ”）に応じて、方法３００はブロック３１４へと進行しうる。
【００６０】
ブロック３１２において、選択されたＦＵＡパスステートメントがカバーされているステートメントの集合に追加されうる。例えば、図２を参照すると、追加モジュール２１８は、選択されたＦＵＡパスステートメントをカバーされているステートメントの集合１３２に追加しうる。
【００６１】
ブロック３１４において、ＦＵＡパスに含まれた他の（ｎｏ  ｍｏｒｅ）ＦＵＡパスステートメントがあるか否かが判定されうる。ＦＵＡパスに含まれた他のＦＵＡパスステートメントがあるという判定（ブロック３１４において“Ｙｅｓ”）に応じて、方法３００はブロック３０８、３１０、３１２、及び３１４のうちの一つ又は複数を通じて進行しうる。ＦＵＡパスに含まれた他のＦＵＡパスステートメントがないという判定（ブロック３１４において“Ｎｏ”）に応じて、方法３００はブロック３１６へと進行する。
【００６２】
ブロック３１６において、カバーされているＦＵＡフラグメントの集合が更新されうる。例えば、図２を参照すると、カバー率更新モジュール２２８はカバーされているＦＵＡコードフラグメントの集合１３４を更新しうる。
【００６３】
ブロック３１８において、ＦＵＡがカバーされているか否かが判定されうる。例えば、図２を参照すると、カバー率判定モジュール２１４は、ＦＵＡ１１８がカバーされているか否かを判定しうる。ＦＵＡがカバーされているという判定（ブロック３１８において“Ｙｅｓ”）に応じて、方法３００は図３Ｂのブロック３３２へと進行しうる。ブロック３３２において、方法３００は停止しうる。ＦＵＡがカバーされていないという判定（ブロック３１０において“Ｎｏ”）に応じて、方法３００は図３Ｂのブロック３２０へと進行しうる。
【００６４】
図３Ｂを参照すると、ブロック３２０において、部分パスの集合が更新されうる。例えば、図２を参照すると、更新モジュール２１２は部分パスの集合１３０を更新しうる。ブロック３２２において、資源制約が存在するか否か又は他の部分パスがないか否かが判定される。資源制約が存在する又は他の部分パスがないという判定（ブロック３２２において“Ｙｅｓ”）に応じて、方法３００はブロック３３２へと進行でき、そこで方法３００は停止しうる。資源制約がない又は他の部分パスがあるという判定（ブロック３２２において“Ｎｏ”）に応じて、方法３００はブロック３２４へと進行しうる。
【００６５】
ブロック３２４において、パスが部分パスの集合から選択されうる。いくつかの実施の形態では、部分パスが部分パスの集合から選択されうる。例えば、図２を参照すると、選択モジュール２０４は部分パスの集合１３０からパス又は部分パスを選択しうる。ブロック３２４に続いて、方法３００は次に、ブロック３０４、３０６、３０８、３１０、３１２、３１４、３１６、３１８、３２０、及び３３２のうちの一つ又は複数へと進行しうる。
【００６６】
追加的に又は代替的に、方法３００はブロック３２４に続いてブロック３２６へと進行しうる。ブロック３２６において、パスステートメントが選択されうる。例えば、図２を参照すると、選択モジュール２０４は、選択されたパス又は選択された部分パスからパスステートメントを選択しうる。
【００６７】
ブロック３２８において、選択されたパスステートメントがカバーされているか否かが判定されうる。いくつかの実施の形態では、その判定は、完全にカバーされているステートメントの集合に基づきうる。例えば、図２を参照すると、判定モジュール２０６は、選択されたパスステートメントがカバーされているか否かをカバーされているステートメントの集合１３２に少なくとも部分的に基づいて判定しうる。選択されたパスステートメントがカバーされているという判定（ブロック３２８において“Ｙｅｓ”）に応じて、方法３００はブロック３０４、３０６、３０８、３１０、３１２、３１４、３１６、３１８、３２０、３２２、及び３３２のうちの一つ又は複数へと進行しうる。選択されたパスステートメントがカバーされていないという判定（ブロック３２８において“Ｎｏ”）に応じて、方法３００はブロック３３０へと進行する。
【００６８】
ブロック３３０において、選択されたパスステートメントは実行されうる。例えば、図２を参照すると、選択されたパスステートメントは実行モジュール２１０によってシンボリックに実行されうる。ブロック３３０に続いて、方法３００は、ブロック３０４、３０６、３０８、３１０、３１２、３１４、３１６、３１８、３２０、３２２、３２８、及び３３２のうちの一つ又は複数へと進行しうる。
【００６９】
ここで開示されたこの及び他の手順および方法については、処理及び方法において行われる機能は異なる順序で実行されうることを当業者は認識するであろう。さらに、概説された工程及び動作は例として提示されているにすぎず、その工程及び動作のいくつかは任意であり、開示された実施の形態から逸脱することなしに、組み合わせてより少ない工程及び動作とされ、あるいは拡張されて追加の工程及び動作とされうる。
【００７０】
図４−７は、ここで説明されるいくつかの実施の形態による例示のソフトウェア解析を提示する。図４は、図１の検証ツール１００又は図２のコンピューティングデバイス２５０によって解析されうるクラス１１６の例を示す。クラス１１６は、ＦＵＡ１１８の例、環境セットアップ１２０の例、及び呼び出された関数１２２の例を含む。クラス１１６では、ＦＵＡ１１８、環境セットアップ１２０、及び呼び出された関数１２２は、Ｃ／Ｃ＋＋スタイルでの疑似コードで記述される。ここで開示された実施の形態は、Ｃ／Ｃ＋＋で記述されたプログラムの解析又は検証に限定されない。いくつかの実施の形態では、検証ツール１００及び／又は図２のコンピューティングデバイス２５０は、Ｃ、Ｃ＋＋、ＪａｖａＳｃｒｉｐｔ（登録商標）、Ｊａｖａ（登録商標）、Ｐｙｔｈｏｎ（登録商標）、ＰＨＰ、ＦＢＭＬ，ＡＳＰ．ＮＥＴ、Ｊ２ＥＥ、及び任意の他のプログラミング言語を含むがこれらに限定されないプログラミング言語で記述されたソフトウェアプログラムを解析するように構成されうる。
【００７１】
図５はシンボリックドライバー５００を示す。シンボリックドライバー５００は、図４のクラス１１６をシンボリックに実行するように構成されうる。具体的には、シンボリックドライバー５００は、環境セットアップ１２０を実行するコードフラグメント５０２及びＦＵＡ１１８を実行する他のコードフラグメント５０４を含みうる。ＦＵＡ１１８を実行することにより、呼び出された関数も実行されうる。いくつかの実施の形態では、シンボリックドライバー５００は、図２の実行モジュール２１０のような実行モジュールにおいて実装されうる。
【００７２】
図６は、図４のＦＵＡ１１８の制御フローグラフ６００を示す。制御フローグラフ６００は、基本ブロック６０２Ａ−６０２Ｄを含む。第１の基本ブロック６０２Ａは、ＦＵＡ１１８における“ｉｆ”ステートメントに対応する。第２の基本ブロック６０２Ｂは、ＦＵＡ１１８における“ｃｏｎｆｉｇＢａｎｄｗｉｄｔｈ（ｂ）”および“ｂａｎｄｗｉｄｔｈ＿＝ｂ”コードフラグメントに対応する。第３の基本ブロック６０２Ｃは、ＦＵＡ１１８の“ｒｅｔｕｒｎ”コードフラグメントに対応する。第４の基本ブロック６０２Ｄは、“ｅｌｓｅ  ｂａｎｄｗｉｄｔｈ＿＝０”コードフラグメントに対応する。基本ブロック６０２Ａ−６０２Ｄは、ＦＵＡ１１８が分岐カバー率に対する２つのパスを含むのみでありうることを示す。制御フローグラフ６００は、図７を参照して説明される解析の間のＦＵＡ１１８のカバー率をさらに示しうる。
【００７３】
図７は、クラス１１６のシンボリック実行ツリー（ｔｒｅｅ）７００を示す。ツリー７００は、ノード７０２Ａ−７０２Ｋ（一般には、一つのノード７０２又は複数のノード７０２）、パス７０４Ａ−７０４Ｋ（一般に、一つのパス７０４又は複数のパス７０４）、及び分岐（ｂｒａｎｃｈ）７０６Ａ−７０６Ｅ（一般に、一つの分岐７０６又は複数の分岐７０６）を含む。パス７０４は、ノード７０２のシーケンスを表す。例えば、第１のパス７０４Ａは、第１のノード７０２Ａ、第２のノード７０２Ｂ、第４のノード７０２Ｄ、及び第８のノード７０２Ｈのシーケンスを表す。同様に、第２のパス７０４Ｂは、第１のノード７０２Ａ、第１のノード７０２Ｂ、第４のノード７０２Ｄ、及び第９のノード７０２Ｉのシーケンスを表す。分岐７０６は、ノード７０２のシーケンスの間の判定ポイント（ｄｅｃｉｓｉｏｎ  ｐｏｉｎｔ）を表す。例えば、第１の分岐７０６Ａは、第１のノード７０２Ａから第２のノード７０２Ｂまでの又は第１のノード７０２Ａから第３のノード７０２Ｃまでのシーケンスの間の判定ポイントを表す。
【００７４】
ツリー７００において、第１の分岐７０６Ａ、第１のノード７０２Ａ、第２のノード７０２Ｂ、及び第３のノード７０２Ｃは、環境セットアップ１２０を表す。具体的には、第１のノード７０２Ａから第２のノード７０２Ｂまでの又は第１のノード７０２Ａから第３のノード７０２Ｃまでの第１の分岐７０６Ａは、第１の変数“ａ”の値に基づきうる。“ａ”が１０より大きい場合には、ツリー７００におけるシーケンスは第１のノード７０２Ａから第２のノード７０２Ｂまでであり、“ａ”が１０以下である場合には、ツリー７００におけるシーケンスは第１のノード７０２Ａから第３のノード７０２Ｃまでである。したがって、第１の分岐７０６Ａは環境セットアップ１２０を表す。
【００７５】
さらに、ツリー７００では、第２及び第３の分岐７０６Ｂ−７０６Ｃならびに第２、第３、第４、第５、第３、第６、第７のノード７０２Ｂ−７０２Ｇは、ＦＵＡ１１８を表す。具体的には、第２のノード７０２Ｂから第４のノード７０２Ｄまでの又は第２のノード７０２Ｂから第５のノード７０２Ｅまでの第２の分岐は第２の変数“ｂ”の値に基づきうる。さらに、ツリー７００では、第３のノード７０２Ｃから第６のノード７０２Ｆまでの又は第３のノード７０２Ｃから第７のノード７０２Ｇまでの第３の分岐７０６Ｃは第２の変数“ｂ”の値に基づきうる。具体的には、“ｂ”の値が０より大きい場合には、ツリー７００のシーケンスは、第２のノード７０２Ｅから第４のノード７０２Ｄまで又は第３のノード７０２Ｃから第６のノード７０２Ｆまででありうる。“ｂ”の値が０以下である場合には、ツリー７００のシーケンスは第２のノード７０２Ｂから第５のノード７０２Ｅまで又は第３のノード７０２Ｃから第７のノード７０２Ｇまででありうる。
【００７６】
同様に、第４及び第５の分岐７０６Ｄ及び７０６Ｅならびに第４、第８、第９、第１０、及び第１１のノード７０２Ｄ、７０２Ｈ、７０２Ｉ、７０２Ｆ、７０２Ｊ、及び７０２Ｋは呼び出された関数１２２を表す。具体的には、第４及び第５の分岐７０６Ｄ及び７０６Ｅは第３の変数“ｃ”の値に依存しうる。
【００７７】
ツリー７００を評価すると、ＦＵＡ１１８は２つのパス７０４の実行を通じてカバーされうる。具体的には、ツリー７００では、ＦＵＡ１１８は、第３のパス７０４Ｃと第２のパス７０４Ａ、第２のパス７０４Ｂ、第４のパス７０４Ｄ、又は第５のパス７０４Ｆのうちの一つを実行することによってカバーされうる。あるいは、ＦＵＡ１１８は、第６のパス７０４Ｆと第１のパス７０４Ａ、第２のパス７０４Ｂ、第４のパス７０４Ｄ、又は第５のパス７０４Ｅのうちの一つを実行することによってカバーされうる。
【００７８】
図３Ａ、３Ｂ、６、及び７を組み合わせて参照して、ツリー７００及び制御フローグラフ６００に基づくＦＵＡ１１８例示解析が説明される。ＦＵＡ１１８のシンボリック実行は第１のノード７０２Ａ（ブロック３２４）を選択することによって開始しうる。第１のノード７０２Ａはカバーされることができない（ブロック３２８において“Ｎｏ”）。したがって、第１のノード７０２Ａは実行されうる（ブロック３３０）。さらに、第１のノード７０２ＡはＦＵＡパスを生成するために使用されうる（ブロック３０４）。
【００７９】
第１のノード７０２Ａに基づいたＦＵＡパスは、第３の基本ブロック６０２Ｃを含みうる。第１のノード７０２Ａは、ＦＵＡ１１８の新しいカバー率を、具体的には第３の基本ブロック６０２Ｃのカバー率を生成する（ブロック３０６において”Ｙｅｓ”）。さらに、第１のノード７０２Ａが解析されうる（ブロック３３４）。ＦＵＡパスは、単一のステートメント“ｒｅｔｕｒｎ”を、例えば、選択される第３の基本ブロック６０２Ｃを含みうる（ブロック３０８）。ＦＵＡ１１８のカバーされていないフラグメントは第３の基本ブロック６０２Ｃから到達可能ではありえず（ブロック３１０において“Ｎｏ”）、他のＦＵＡパスステートメントはありえない（ブロック３１４において“Ｎｏ”）。したがって、カバーされているＦＵＡフラグメントの集合は第３の基本ブロック６０２Ｃを含むように更新されうる（ブロック３１６）。第３の基本ブロック６０２Ｃだけがカバーされ、したがってＦＵＡはカバーされない（ブロック３１８において“Ｎｏ”）。部分パスの集合は、第１のノード７０２Ａが実行されたことを示すために更新されうる（ブロック３２０）。存続部分パスが有り（ブロック３２２において“Ｎｏ”）、したがって第２のノード７０２Ｂ及び／又は第３のノード７０２Ｃが選択されうる（ブロック３２４）。
【００８０】
第２のノード７０２Ｂはカバーされえない（ブロック３２８において“Ｎｏ”）。第２のノード７０２Ｂはしたがって実行されうる（ブロック３３０）。さらに、第２のノード７０２ＢはＦＵＡパスを生成するために使用されうる（ブロック３０４）。第２のノード７０２Ｂを使用して生成されたＦＵＡパスは、第１のノード７０２ＡによってカバーされたＦＵＡパスと同様の第３の基本ブロック６０２Ｃを含みうる。したがって、第２のノード７０２Ｂによって生成されたＦＵＡパスは、既にカバーされている第３の基本ブロック６０２Ｃをカバーする。ＦＵＡパスはＦＵＡ１１８に対する新しいカバー率を生成しない（ブロック３０６において“Ｎｏ”）。部分パスの集合は、第２のノード７０２Ｂが探索されたことを示すために更新されうる（ブロック３２０）。第３のノード７０２Ｃ、第４のノード７０２Ｄ、及び第６のノード７０２Ｆの解析は第２のノード７０２Ｂの解析と同様である。
【００８１】
第８のノード７０２Ｈが次に選択されうる（ブロック３２４）。第８のノード７０２Ｈが実行されることができ（ブロック３３０）、第８のノード７０２Ｈを使用してＦＵＡパスが生成されうる（ブロック３０２）。第８のノード７０２Ｈを使用して生成されたＦＵＡパスは、第１の基本ブロック６０２Ａ、第２の基本ブロック６０２Ｂ、及び第３の基本ブロック６０２Ｃを含みうる。したがって、第８のノード７０２Ｈを使用して生成されたＦＵＡパスはＦＵＡ１１、例えば、第２の基本ブロック６０２Ｂに対する新しいカバー率を生成し、第１の基本ブロック６０２Ａの部分カバー率が新しいカバー率でありうる（ブロック３０６において“Ｙｅｓ”）。第３の基本ブロック６０２Ｃが選択されうる（ブロック３０８）。第３の基本ブロック６０２Ｃは、ＦＵＡパスの終端でありうる。したがって、ＦＵＡ１１８のカバーされていないフラグメントは、第３の基本ブロック６０２Ｃから到達可能ではない（ブロック３１０において“Ｎｏ”）。
【００８２】
第２の基本ブロック６０２Ｂが次に選択されうる（ブロック３１４及び３０８）。第３の基本ブロック６０２Ｃは既にカバーされているから、ＦＵＡ１１８のカバーされていないフラグメントは第２の基本ブロック６０２Ｂから到達可能でない（ブロック３１０において“Ｎｏ”）。第１の基本ブロック６０２Ａが次に選択されうる（ブロック３１４及び３０８）。ここでも、第２の基本ブロック６０２Ｂはカバーされているが、第４の基本ブロック６０４Ｄはカバーされていない。したがって、ＦＵＡ１１８のカバーされていないフラグメントは第１の基本ブロック６０２Ａから到達可能である（ブロック３１０において“Ｙｅｓ”）。第１の基本ブロック６０２Ａは次に、カバーされているステートメントの集合に追加されうる（ブロック３１２）。
【００８３】
カバーされているＦＵＡフラグメントの集合は更新されうる（ブロック３１６）。第４の基本ブロック６０２Ｄはカバーされておらず、第１の基本ブロック６０２Ａは部分的にカバーされているにすぎないから、ＦＵＡはカバーされていない（ブロック３１８において“Ｎｏ”）。部分パスの集合は更新されうる（ブロック３２０）。さらに、資源制約は存在せず、存続部分パスがあり（ブロック３２２において“Ｎｏ”）、したがって第９のノード７０２Ｉが選択されうる（ブロック３２４）。
【００８４】
第９のノード７０２Ｉはカバーされえない（ブロック３２８において“Ｎｏ”）。したがって、第９のノード７０２Ｉは実行されうる（ブロック３３０）。さらに、第９のノード７０２ＩはＦＵＡパスを生成するために使用されうる（ブロック３０４）。第９のノード７０２Ｉを使用して生成されたＦＵＡパスは、第８のノード７０２Ｈを使用して生成されたＦＵＡパスと同様に、第１の基本ブロック６０２Ａ、第２の基本ブロック６０２Ｂ、及び第３の基本ブロック６０２Ｃを含みうる。したがって、第９のノード７０２Ｉによって生成されたＦＵＡパス、既にカバーされている基本ブロック６０２をカバーする。ＦＵＡパスはＦＵＡ１１８に対する新しいカバー率を生成しない（ブロック３０６において“Ｎｏ”）。
【００８５】
部分パスの集合は更新されうる（ブロック３２０）。さらに、資源制約は存在せず、存続部分パスは存在せず（ブロック３２２において“Ｎｏ”）、したがって第５のノード７０２Ｅが選択されうる（ブロック３２４）。
【００８６】
第５のノード７０２Ｅが次に選択されうる（ブロック３２４）。第５のノード７０２Ｅが実行され（ブロック３３０）、第５のノード７０２Ｅを使用してＦＵＡパスが生成されうる。第５のノード７０２Ｅを使用して生成されたＦＵＡパスは、第１の基本ブロック６０２Ａ、第４の基本ブロック６０２Ｄ、及び第３の基本ブロック６０２Ｃを含みうる。したがって、第５のノード７０２Ｅを使用して生成されたＦＵＡパスは、ＦＵＡ１１８に対する新しいカバー率（ブロック３１０において“Ｙｅｓ”）、例えば第４の基本ブロック６０２Ｄを生成し、第１の基本ブロック６０２Ａの部分カバー率が新しいカバー率でありうる。第３の基本ブロック６０２Ｃが選択されうる（ブロック３０８）。第３の基本ブロック６０２ＣはＦＵＡパスの終端（ｅｎｄ  ｏｆ  ｔｈｅ  ＦＵＡ  ｐａｔｈ）でありうる。したがって、ＦＵＡ１１８のカバーされていないフラグメントは第３の基本ブロック６０２Ｃから到達可能ではない（ブロック３１０において“Ｎｏ”）。
【００８７】
第４の基本ブロック６０２Ｄが次に選択されうる（ブロック３１４及び３０８）。第３の基本ブロック６０２Ｃが既にカバーされているので、ＦＵＡ１１８のカバーされていないフラグメントは第４の基本ブロック６０２Ｄから到達可能ではない（ブロック３１０において“Ｎｏ”）。第１の基本ブロック６０２Ａが次に選択されうる（ブロック３１４及び３０８）。ここでも、第４の基本ブロック６０２Ｄはカバーされており、第２の基本ブロック６０２Ｂは既にカバーされている可能性がある。したがって、ＦＵＡ１１８のカバーされていないフラグメントは第１の基本ブロック６０２Ａから到達可能ではない。
【００８８】
カバーされているＦＵＡフラグメントの集合が更新されうる（ブロック３１６）。基本ブロック６０２がカバーされているので、ＦＵＡはカバーされる（ブロック３１８において“Ｙｅｓ”）。シンボリック実行は停止されうる（ブロック３３２）。したがって、ＦＵＡ１１８はカバーされ、ツリー７００において、第１、第２、第３、第４、第５、第８、及び第９のノード７０２Ａ、７０２Ｂ、７０２Ｃ、７０２Ｄ、７０２Ｅ、７０２Ｈ、及び７０２Ｉの含まれたシンボリック実行を解析される。
【００８９】
ここで説明された実施の形態は、下記でさらに詳細に説明されるように、種々のコンピュータハードウェア又はソフトウェアを含む専用又は汎用コンピュータの使用を含みうる。
【００９０】
ここで説明される実施の形態は、コンピュータ実行可能命令又はデータ構造を搬送するための又はその命令又はデータ構造を記録されたコンピュータ読取り可能媒体を使用して実装されうる。そのようなコンピュータ読取り可能媒体は、汎用又は専用コンピュータによってアクセスされうる任意の利用可能な媒体でありうる。例示としてであって限定としてではなく、このようなコンピュータ読取り可能媒体は、ＲＡＭ、ＲＯＭ、ＥＥＰＲＯＭ、ＣＤ−ＲＯＭ又は他の光ディスク記憶装置、磁気ディスク記憶装置または他の磁気記憶デバイスを含む非一時的なコンピュータ読取り可能記憶媒体、又はコンピュータ実行可能な命令又はデータ構造の形態をなす所望のプログラムコードを搬送し又は記憶するために使用されうるそして汎用又は専用コンピュータによってアクセスされうる任意の他の非一時的な記憶媒体を含みうる。上記のものの組み合わせもコンピュータ読取り可能媒体の範囲内に含まれうる。
【００９１】
コンピュータ実行可能命令は、例えば、汎用コンピュータ、専用コンピュータ、又は専用処理装置にある機能又は機能のグループを実行させる命令及びデータを含む。主題は構造的特徴及び／又は方法論的行為に特定の言語で説明されたが、添付請求項に定義された主題は上記の特定の特徴又は行為に必ずしも限定されないことが理解されるべきである。むしろ、上記の特定の特徴及び行為は、請求項を実施する例示の形式として開示されている。
【００９２】
ここで使用されるように、「モジュール」又は「コンポーネント」という用語は、コンピューティングシステム上で実行するソフトウェアオブジェクト又はルーチンを意味しうる。ここで説明された種々のコンポーネント、モジュール、エンジン、及びサービスは、コンピューティングシステム上で実行するオブジェクト又はプロセスとして（例えば、別々のスレッドとして）実装されうる。ここで説明されたシステム及び方法は、ソフトウェアで実装されることが好ましいが、ハードウェアでの実装またはソフトウェアとハードウェアの組み合わせも可能であり意図されている。この説明では、「コンピューティングエンティティ」（ｃｏｍｐｕｔｉｎｇ  ｅｎｔｉｔｙ）は、ここにおいて先に定義された任意のコンピューティングシステム又はコンピューティングシステム上で動作する任意のモジュール又はモジュレートの組み合わせでありうる。
【００９３】
ここにおいて記載されたすべての実施例及び条件付き言語は、本発明及び技術を進展させることに対して本発明者によって貢献される概念を読者が理解するのを容易にするための教育上の目的を意図されており、このような具体的に記載された実施例及び条件に限定されないとして解釈されるべきである。本発明の実施の形態が詳細に説明されたが、それらに対しては本発明の精神及び範囲から逸脱することなしに種々の変化、置換、及び変更がなされうることが理解されるべきである。
【符号の説明】
【００９４】
１０２    ソフトウェアプログラム
１０８    ソルバーモジュール
１１２    値テストエンジン
１１６    クラス
１１８    解析中の関数
１２０    環境セットアップ
１２２    呼び出された関数
１３０    部分パスの集合
１３２    カバーされているステートメントの集合
１３４    カバーされているＦＵＡコードフラグメントの集合
１５０    シンボリック実行モジュー
１５２    カバー率解析モジュール
２０４    選択モジュール
２０６    判定モジュール
２０８    生成モジュール
２１０    実行モジュール
２１２    更新モジュール
２１４    カバー率判定モジュール
２１８    追加モジュール
２２４    プロセッサ
２２６    通信ユニット
２２８    カバー率更新モジュール
２３４    通信モジュール
【図１】
2015219907.tif 000003
【図２】
2015219907.tif 000004
【図３Ａ】
2015219907.tif 000005
【図３Ｂ】
2015219907.tif 000006
【図４】
2015219907.tif 000007
【図５】
2015219907.tif 000008
【図６】
2015219907.tif 000009
【図７】
2015219907.tif 000010