(57)【特許請求の範囲】
【請求項１】
イベント駆動型ソフトウェアアプリケーションの複数のイベントの実行順序を制約するシーケンス実行制約を決定し、
前記複数のイベントの１つ又は２つ以上の可能なイベントシーケンスにおける前記複数のイベントの位置を制約するシーケンス位置制約を決定し、
前記複数のイベントのそれぞれのイベント入力とイベント出力との間の関係をそれぞれが示すイベント関係制約を決定し、
前記シーケンス実行制約、前記シーケンス位置制約及び前記イベント関係制約を含み、前記１つ又は２つ以上の可能なイベントシーケンスを列挙する制約セットを形成し、
前記１つ又は２つ以上のイベントシーケンスの制御フロー情報を前記制約セットにエンコードする、
ことを含む方法。
【請求項２】
前記複数のイベントのそれぞれのイベントのそれぞれのイベント入力のそれぞれが前記複数のイベントの他のイベントのイベント入力に対応し且つ前記複数のイベントのそれぞれのイベントのそれぞれのイベント出力のそれぞれが前記複数のイベントの他のイベントのイベント出力に対応するように、前記複数のイベントのイベント入力及びイベント出力を割り当てる、ことを更に含む、請求項１に記載の方法。
【請求項３】
前記イベント入力及び前記イベント出力を割り当てることは、
前記複数のイベントのそれぞれのために、前記複数のイベントの１つ又は２つ以上に関連するイベント入力に対応するシンボリック入力変数を導入し、
前記複数のイベントのそれぞれのために、前記複数のイベントの１つ又は２つ以上に関連するイベント出力に対応するシンボリック出力変数を導入する請求項２に記載の方法。
【請求項４】
前記シーケンス実行制約の決定は、順次実行される複数のイベントのペアに対する可能な複数の配列に基づくものであり、前記複数の可能な配列の１つの配列におけるペアの第１イベントの第１イベント出力が、前記１つの配列の前記ペアの第２イベントの第２イベント入力として使用される、請求項１に記載の方法。
【請求項５】
前記イベント関係制約の決定は、前記複数のイベントにおけるイベントの数の１つ又は２つ以上と、前記イベント駆動型ソフトウェアアプリケーションの制御フローに対して一回実行される前記複数のイベントのただ１つのイベントとに基づく、請求項１に記載の方法。
【請求項６】
前記複数のイベントのそれぞれのために、前記複数のイベントの実行順序における対応するイベントの位置に関連するシンボリック順序変数を導入し、
前記シーケンス実行制約及び前記シーケンス位置制約に基づいて前記シンボリック順序変数を制約する、
ことを更に含む、請求項１に記載の方法。
【請求項７】
前記複数のイベントを取得するために、一群のイベントから余分なイベントを取り除くことを更に含む、請求項１に記載の方法。
【請求項８】
前記制約セットの前記１つ又は２つ以上の可能なイベントを探索するために、制約の解を適用することを更に含む、請求項１に記載の方法。
【請求項９】
新しいイベントに基づいて、前記シーケンス実行制約、前記シーケンス位置制約及び前記イベント関係制約の１つ又は２つ以上を更新し、
前記シーケンス実行制約、前記シーケンス位置制約及び前記イベント関係制約の前記１つ又は２つ以上の更新に基づいて前記制約セットを修正する、
ことを更に含む、請求項１に記載の方法。
【請求項１０】
前記制約セットに基づいて、前記イベント駆動型ソフトウェアアプリケーションのデバッグ、検査及びテスト生成動作を実行することを更に含む、請求項１に記載の方法。
【請求項１１】
イベント駆動型ソフトウェアアプリケーションの複数のイベントの実行順序を制約するシーケンス実行制約を決定し、
前記複数のイベントの１つ又は２つ以上の可能なイベントシーケンスにおける前記複数のイベントの位置を制約するシーケンス位置制約を決定し、
前記複数のイベントのそれぞれのイベント入力とイベント出力との間の関係をそれぞれが示すイベント関係制約を決定し、
前記シーケンス実行制約、前記シーケンス位置制約及び前記イベント関係制約を含み、前記１つ又は２つ以上の可能なイベントシーケンスを列挙する制約セットを形成し、
前記１つ又は２つ以上のイベントシーケンスの制御フロー情報を前記制約セットにエンコードする、
動作をコンピュータに実行させるプログラム。
【請求項１２】
前記動作は、前記複数のイベントのそれぞれのイベントのそれぞれのイベント入力が前記複数のイベントの他のイベントのイベント入力に対応し且つ前記複数のイベントのそれぞれのイベントのそれぞれのイベント出力が前記複数のイベントの他のイベントのイベント出力に対応するように、前記複数のイベントのイベント入力及びイベント出力を割り当てる、ことを更に含む、請求項１１に記載のプログラム。
【請求項１３】
前記イベント入力及び前記イベント出力を割り当てることは、
前記複数のイベントのそれぞれのために、前記複数のイベントの１つ又は２つ以上に関連するイベント入力に対応するシンボリック入力変数を導入し、
前記複数のイベントのそれぞれのために、前記複数のイベントの１つ又は２つ以上に関連するイベント出力に対応するシンボリック出力変数を導入する請求項１２に記載のプログラム。
【請求項１４】
前記シーケンス実行制約の決定は、順次実行される複数のイベントのペアに対する可能な複数の配列に基づくものであり、前記複数の可能な配列の１つの配列におけるペアの第１イベントの第１イベント出力が、前記１つの配列の前記ペアの第２イベントの第２イベント入力として使用される、請求項１１に記載のプログラム。
【請求項１５】
前記イベント関係制約の決定は、前記複数のイベントにおけるイベントの数の１つ又は２つ以上と、前記イベント駆動型ソフトウェアアプリケーションの制御フローに対して一回実行される前記複数のイベントのただ１つのイベントとに基づく、請求項１１に記載のプログラム。
【請求項１６】
前記動作は、
前記複数のイベントのそれぞれのために、前記複数のイベントの実行順序における対応するイベントの位置に関連するシンボリック順序変数を導入し、
前記シーケンス実行制約及び前記シーケンス位置制約に基づいて前記シンボリック順序変数を制約する、
ことを更に含む、請求項１１に記載のプログラム。
【請求項１７】
前記動作は、前記複数のイベントを取得するために、一群のイベントから余分なイベントを取り除くことを更に含む、請求項１１に記載のプログラム。
【請求項１８】
前記動作は、前記制約セットの前記１つ又は２つ以上の可能なイベントを探索するために、制約の解を適用することを更に含む、請求項１１に記載のプログラム。
【請求項１９】
前記動作は、
新しいイベントに基づいて、前記シーケンス実行制約、前記シーケンス位置制約及び前記イベント関係制約の１つ又は２つ以上を更新し、
前記シーケンス実行制約、前記シーケンス位置制約及び前記イベント関係制約の前記１つ又は２つ以上の更新に基づいて前記制約セットを修正する、
ことを更に含む、請求項１１に記載のプログラム。
【請求項２０】
前記動作は、前記制約セットに基づいて、前記イベント駆動型ソフトウェアアプリケーションのデバッグ、検査及びテスト生成動作を実行することを更に含む、請求項１１に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本明細書に記載の実施形態は、イベント駆動型ソフトウェアのテストに関する。
【背景技術】
【０００２】
認証又は検証ソフトウェアのようなテストソフトウェアは、インフォメーションテクノロジ（information technology、ＩＴ）組織に普及したものである。例えば、ソフトウェアが１つ又は２つ以上のクライアントコンピュータシステムで実行されるデスクトップアプリケーションであるか、又は１つ又は２つのサーバコンピュータシステムで実行されるウェブアプリケーションであるかにかかわらず、ソフトウェアの品質を検証することは多くの場合で重要である。ソフトウェアのいくつかの形式のエラーは、ユーザを苛立たせ、不便を感じさせるだけであるが、他の形式のエラーは、データの損失及び金銭上の損失のような他の問題を引き起こす可能性がある。
【０００３】
ユビキタス化されているソフトウェアの１つは、グラフィカルユーザインタフェース（graphical user interface、ＧＵＩ）ベースのアプリケーション及びウェブベースのアプリケーションのようなイベント駆動型ソフトウェアである。イベント駆動型ソフトウェアでは、ソフトウェアのフローは、ユーザアクション（マウスクリック、キータッチ）、センサ出力又は他のブログラム／スレッドからのメッセージのようなイベントによって決定されてもよい。イベント駆動型ソフトウェアは、テストの間に探索されてもよい多くの数の異なるイベント、及び対応するイベントシーケンスを有してもよい。多くの数のイベント及びイベントシーケンスは、イベントシーケンス爆発を起こす可能性がある。イベントシーケンス爆発は、イベント駆動型ソフトウェアが時間を浪費し及び／又は資源を消費するおそれがある。いくつかの例では、イベントシーケンス爆発から要求される処理量は、テストの実行を難しくする。
【発明の概要】
【発明が解決しようとする課題】
【０００４】
本明細書の主題は、多くの課題を解決する実施形態、又は上述の課題のような環境においてのみ作動する実施形態に限定されるものではない。むしろ、この背景技術は、本明細書で説明される実施形態が実施できる技術領域の一例を説明するためにのみ提供されるものである。
【課題を解決するための手段】
【０００５】
実施形態の一態様に従うと、方法は、イベント駆動型ソフトウェアアプリケーションの複数のイベントの実行順序を制約するシーケンス実行制約を決定することを含んでもよい。また、方法は、複数のイベントの１つ又は２つ以上の可能なイベントシーケンスにおける複数のイベントの位置を制約するシーケンス位置制約を決定することを含んでもよい。さらに、方法は、複数のイベントのそれぞれのイベント入力とイベント出力との間の関係をそれぞれが示すイベント関係制約を決定することを含んでもよい。また、方法は、１つ又は２つ以上の可能なイベントシーケンスを列挙する制約セットであって、シーケンス実行制約、シーケンス位置制約及びイベント関係制約を含む制約セットを形成することを含んでもよい。加えて、方法は、１つ又は２つ以上のイベントシーケンスの制御フロー情報を制約セットにエンコードすることを含んでもよい。
【０００６】
実施形態の目的及び利点は、少なくとも特許請求の範囲で具体的に挙げられた構成要素、特徴及び組み合わせによって理解及び達成されることになるであろう。
【０００７】
上述の全般的な説明及び以下の詳細な説明は、典型的且つ説明的なものであり、特許請求の範囲に記載される発明を限定するものではないことが理解されるであろう。
【図面の簡単な説明】
【０００８】
【図１Ａ】ソフトウェアをテストするように構成されたシステムの一例を示す図である。
【図１Ｂ】ソフトウェアをテストするように構成されたテストモジュールを含んでもよい電子デバイスの一例を示す図である。
【図２】イベント駆動型ソフトウェアアプリケーションのテストに対して使用されてもよいフローの一例を示す図である。
【図３】制約セットを逐次更新する一例の方法３００のフローチャートである。
【発明を実施するための形態】
【０００９】
例示的な実施形態は、添付図面を使用して更に具体的且つ詳細に記載且つ説明されることになる。
【００１０】
本明細書に記載されるいくつかの実施形態は、電子デバイスのためのグラフィカルユーザインタフェース（ＧＵＩ）ベースのアプリケーション及びウェブベースのアプリケーションのようなイベント駆動型ソフトウェアアプリケーションをテストする方法及びそのシステムに関する。イベント駆動型ソフトウェアアプリケーションのフローは、ユーザアクション（マウスクリック、キータッチ）、センサ出力又は他のブログラム／スレッドからのメッセージのような種々の「イベント（event）」によって決定されてもよい。イベント駆動型ソフトウェアアプリケーションは、テストの間に探索されてもよい多くの数の異なるイベント、及び対応するイベントシーケンスを有してもよい。多くの数のイベント及びイベントシーケンスは、イベント駆動型ソフトウェアアプリケーションを分析するときに、イベントシーケンス爆発を起こす可能性がある。
【００１１】
以下に詳細に説明されるように、探索されてもよいイベントシーケンスの数を低減するために、イベント駆動型ソフトウェアアプリケーションのイベント及びイベントシーケンスに関連する種々の形式の制約を決定して制約セットを形成してもよい。制約セットは、種々の制約によって制約される可能なイベント駆動型ソフトウェアアプリケーションのイベントシーケンスを列挙してもよい。次いで、イベントセットは、制約ソルバを使用して解かれてもよい。さらに、イベント駆動型ソフトウェアアプリケーションの一連のイベントシーケンス（以下、「イベントスペース（event space）」とも称する）は、制約の解に基づいて探索されてもよい。このような処理によって、探索されてもよいイベントシーケンスの数を低減して、イベントシーケンス爆発に関連する問題を少なくとも部分的に避けることができる。
【００１２】
本発明の実施形態は、添付図面を参照して説明されることになる。
【００１３】
図１Ａは、本明細書に記載される少なくとも１つの実施形態に従って配置され、イベント駆動型ソフトウェアをテストするように構成された一例のシステム１００を示す図である。システム１００は、ソフトウェアプログラムのコードアンダーテスト（code under test）１０４に対するテストを実行して、ソフトウェアプログラムのテスト結果１０８を生成するように構成されるテストモジュール１０６を含んでもよい。コードアンダーテスト１０４は、例えば、イベント駆動型ソフトウェアアプリケーション、ソフトウェアアプリケーションのコード、ライブラリ、アプリケーション、スクリプト、又は処理デバイスが実行するための他の論理又は命令などの電子データを含んでもよい。いくつかの実施形態では、コードアンダーテスト１０４は、イベント駆動型ソフトウェアアプリケーションのコンプリート・インスタンス（complete instance）を含んでもよい。これらの実施形態又は他の実施形態では、コードアンダーテスト１０４は、ソフトウェアプログラムの一部を含んでもよい。コードアンダーテスト１０４は、イベント駆動型ソフトウェアアプリケーションで使用されてもよい適当な形式のコンピュータ言語で書き込まれてもよい。
【００１４】
コードアンダーテスト１０４は、いくつかのソフトウェアモジュールで構造化されたソフトウェアプログラムの一部を含んでもよい。ソフトウェアモジュールは、ソフトウェアモジュールの特定の機能を実行するコードを含んでもよい。特定の機能を実行するコードは、ソフトウェア関数と称されてもよい。いくつかの実施形態において、コードアンダーテスト１０４は、イベント駆動型アプリケーションに関連するイベントの発生に対して１つ又は２つ以上のソフトウェア関数を実行してもよい。例えば、コードアンダーテスト１０４は、イベント「ｅ１」に対して変数「ａ」に対する動作を実行してもよいソフトウェア関数「ｆ１（ａ）」を含んでもよい。
【００１５】
以下に詳細に説明されるように、テストモジュール１０６は、コードアンダーテスト１０４に対して、コードアンダーテスト１０４のテストを支援してもよい一連の動作を実行するように構成されてもよい。例えば、テストモジュール１０６は、コードアンダーテスト１０４のイベントシーケンスに関連してもよい種々の形式の制約を決定するように構成されてもよい。また、テストモジュール１０６は、種々の制約に基づくコードアンダーテスト１０４の可能なイベントシーケンスを列挙してもよい制約セットを決定し且つ生成してもよい。これらの実施形態のいくつかでは、テストモジュール１０６は、制約ソルバを使用して制約セットを解くように構成されてもよい。加えて、いくつかの実施形態では、テストモジュール１０６は、制約の解に基づいてコードアンダーテスト１０４のイベントスペースを探索するように構成されてもよい。これらの実施形態又は他の実施形態では、テストモジュール１０６は、コードアンダーテスト１０４に関連する１つ又は２つ以上のクエリが制約の解に基づくイベントスペースの探索によって充足可能であるか否かを決定するように構成されてもよい。以下に詳細に説明されるように、図２及び３は、制約セットを生成し且つイベントスペース探索を実行するために実行されてもよい動作の例を説明する。
【００１６】
いくつかの実施形態において、テストモジュール１０６は、コードアンダーテスト１０４のテストからテスト結果１０８を生成してもよい。テスト結果１０８は、イベントシーケンスの探索に基づいてコードアンダーテスト１０４の特定のクエリが充足可能であるか又は充足可能ではないかを決定したことを示してもよい。これらの実施形態又は他の実施形態では、テストモジュール１０６は、制約が充足可能であるときに、１つ又は２つ以上の制約セットに対して１つ又は２つ以上の解を生成してもよい。いくつかの実施形態において、一組の制約を解くことは、制約セットに含まれる全ての制約を充足する１つ又は２つ以上の解を探し出す試みを実行することを含んでもよい。これらの実施形態のいくつかでは、テストモジュール１０６は、テスト結果１０８を有する解を含んでもよい。いくつかの実施形態では、解を使用して、コードアンダーテスト１０４をテスト又はデバックしてもよい。
【００１７】
図１Ｂは、本明細書に記載される少なくとも１つの実施形態に従って、テストモジュール１０６を含んでもよい一例の電子デバイス１０２を示す図である。電子デバイス１０２は、テストモジュール１０６を使用してコードアンダーテスト１０４をテストするように構成された適当な装置、機器又はデバイスを含んでもよい。電子デバイス１０２は、メモリ１１２に通信可能に結合されたプロセッサ１１０を含んでもよい。いくつかの実施形態において、テストモジュール１０６は、プロセッサ１１０が実行するためにメモリ１１２に常駐する論理又は命令に統合されてもよい。
【００１８】
プロセッサ１１０は、適切な特定用途のコンピュータ及び汎用のコンピュータ、若しくは種々のコンピュータハードウェア又はソフトウェアを含むコンピュータエンティティ又は処理装置を含んでもよく、コンピュータが読み取り可能な適切な媒体に格納された命令を実行するように構成されてもよい。例えば、プロセッサ１１０は、マイクロプロセッサ、マイクロコントローラ、デジタル信号処理（ＤＳＰ）、特定用途向け集積回路（ＡＳＩＣ）、フィールドプログラマブルゲートアレイ（ＦＰＧＡ）又はプログラムの命令を解釈及び／又は実行する及び／又はデータを処理するように構成された他のデジタル回路又はアナログ回路を含んでもよい。図１Ｂには単一のプロセッサとして記載されているものの、プロセッサ１１０はいくつもの操作を実行するように構成されたいくつものプロセッサを含んでもよい。いくつかの実施形態では、プロセッサ１１０は、プログラム命令を解釈及び／又は実行し及び／又はメモリ１１２に記憶されたデータを処理してもよい。
【００１９】
メモリ１１２は、コンピュータ実行可能な命令又はデータ構造を格納して運搬又は所有するコンピュータ読み取り可能な媒体を含んでもよい。コンピュータ読み取り可能な媒体は、汎用コンピュータ又は特定用途コンピュータによりアクセスできる入手可能な媒体であってもよい。限定されない例示では、コンピュータが読み取り可能な媒体は、ランダムアクセスメモリ（ＲＡＭ）、リードオンリメモリ（ＲＯＭ）、電気的に消去可能なプログラマブルリードオンリメモリ（ＥＥＰＲＯＭ）、コンパクトディスクリードオンリメモリ（ＣＤ−ＲＯＭ）又は他の光学ディスク記憶装置、磁気ディスク記憶装置又は他の磁気記憶デバイス、フラッシュメモリデバイス（固体メモリデバイス等）又は所望のプログラムコードをコンピュータが実行可能な命令又はデータ構造で運搬又は格納するために使用され、汎用コンピュータ又は特定用途コンピュータによりアクセス可能な他の記憶媒体又は一時的でないコンピュータ読み取り可能な記憶媒体であってもよい。また、上述の機器を組み合わせたものは、コンピュータ読み取り可能な媒体に含まれてもよい。例えば、コンピュータ読み取り可能な命令は、プロセッサ１１０が特定の関数又は一群の関数を実行する命令及びデータを含んでもよい。
【００２０】
テストモジュール１０６は、プロセッサ１１０がコードアンダーテスト１０４のテストを実行するように構成された命令及びデータを含んでもよい。これにより、いくつかの実施形態では、電子デバイス１０２は、図１Ｂに示すメモリ１１２のテストモジュール１０６と協働してもよい。
【００２１】
図２は、本明細書に記載される少なくとも１つの実施形態に従うイベント駆動型ソフトウェアアプリケーションのテストに対して使用されてもよい一例のフロー２００のフローを示す図である。フロー２００は、適当なシステム、機器又はデバイスで実行されてもよい。例えば、図１Ｂの電子デバイス１０２のテストモジュール１０６は、フロー２００に関連する動作の１つ又は２つ以上を実行してもよい。個別のブロックとして説明されるものの、種々のブロックは、所望の実装に依存して、付加的なブロックに分割されてもよく、より少ないブロックに組み合わされてもよく、削除されてもよい。
【００２２】
フロー２００は、図１Ａのコードアンダーテスト１０４のようなコードアンダーテストとして動作してもよいイベント駆動型ソフトウェアアプリケーションの１つ又は２つ以上の部分に対して実行されてもよい。いくつかの実施形態では、フロー２００は、コードアンダーテストに関連してもよい１つ又は２つ以上の初期イベント２０２を受信することによって開始してもよい。初期イベントは、ソースアプリケーション（source application）の構文解析ツール（parser）又はインタープリタ（interpreter）から取得されてもよいイベントであってもよい。コードアンダーテストの実行の間に動的に見出されるイベントは、いくつかの例において初期イベントとして見なされてもよい。例えば、ウェブアプリケーションの初期イベントは、関連するソースコードと共にウェブブラウザから読み出されてもよい。
【００２３】
説明される実施形態では、フロー２００は、プリプロセスフェーズ２０４、制約セット決定フェーズ２０６及びテスト結果生成フェーズ２１０を含んでもよい。プリプロセスフェーズ２０４、制約セット決定フェーズ２０６及びテスト結果生成フェーズ２１０は、初期イベント２０２及び関連するコードアンダーテストを使用して、図１Ａを参照して説明されたテスト結果１０８に類似してもよいテスト結果２０８を出力してもよい。
【００２４】
プリプロセスフェーズ２０４は、初期イベント２０２のイベントプロパティ（event property）を決定し且つ割り当てることに関連する動作に対応するブロック２１２を含んでもよい。ブロック２１２において、初期イベント２０２のそれぞれの入力及び出力（以下「イベント入力」及び「イベント出力」とも称する）は決定されてもよい。また、イベント入力と関連するイベント出力との間の関係は決定されてもよい。加えて、いくつかの実施形態では、イベント入力及びイベント出力は、割り当てられてもよい。ここで、種々の初期イベント２０２のイベント入力及びイベント出力との間の関連性は、確立されてもよい。いくつかの実施形態において、シンボリック入力変数はイベント入力のそれぞれのために導入されてもよく、シンボリック出力変数はイベント出力のそれぞれのために導入されてもよい。また、式は、シンボリック変数及び決定された関係を使用して、初期イベント２０２、及び関連する関数のために生成されてもよい。
【００２５】
例えば、初期イベント２０２は、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」を含んでもよい。イベント「ｅ１」は、「ｆ１（ａ）＝｛ａ＝ａ＋３｝」で示される式によって表されてもよい関数「ｆ１（ａ）」に関連してもよい。イベント「ｅ２」は、「ｆ２（ａ）＝｛ａ＝２ａ｝」で示される式によって表されてもよい関数「ｆ２（ａ）」に関連してもよい。イベント「ｅ３」は、「ｆ３（ａ）＝｛ａ＝１｝」で示される式によって表されてもよい関数「ｆ３（ａ）」に関連してもよい。イベント「ｅ４」は、「ｆ４（ａ）＝｛ａ＝３ａ−１｝」で示される式によって表されてもよい関数「ｆ４（ａ）」に関連してもよい。イベント「ｅ５」は、「ｆ５（ａ）＝｛ａ＝２ａ＋６｝」で示される式によって表されてもよい関数「ｆ５（ａ）」に関連してもよい。
【００２６】
上述のように、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」のイベント出力及びイベント入力のそれぞれは、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」の１つ又は２つ以上のシーケンスが実行されるときに、１つのイベントの出力が他のイベントの入力として使用されるように変数「ａ」に対応してもよい。このように、インベント入力とイベント出力との間の関連性及び関係は決定されてもよい。
【００２７】
いくつかの実施形態では、シンボリック入力変数及びシンボリック出力変数は、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」のイベント入力とイベント出力との間の関係に基づいてイベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」のために生成されてもよい。一例では、シンボリック入力変数「ａ１」及びシンボリック出力変数「ａ１」はイベント「ｅ１」のために導入されてもよく、シンボリック入力変数「ａ２」及びシンボリック出力変数「ａ２」はイベント「ｅ２」のために導入されてもよく、シンボリック入力変数「ａ３」及びシンボリック出力変数「ａ３」はイベント「ｅ３」のために導入されてもよく、シンボリック入力変数「ａ４」及びシンボリック出力変数「ａ４」はイベント「ｅ４」のために導入されてもよく、シンボリック入力変数「ａ５」及びシンボリック出力変数「ａ５」はイベント「ｅ５」のために導入されてもよい。
【００２８】
加えて、シンボリック入力変数と対応するシンボリック出力変数との間の関係を示すシンボリック式は、生成されてもよい。例えば、シンボリック出力変数「ａ１」の値がシンボリック入力変数「ａ１」の値に対して式「ｆ１」を実行することによって生成されてもよい式「ａ１→ｆ１→ａ１」は、生成されてもよい。同様に式「ａ２→ｆ２→ａ２」、「ａ３→ｆ３→ａ３」、「ａ４→ｆ４→ａ４」及び「ａ５→ｆ５→ａ５」は、イベント「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」に対してそれぞれ生成されてもよい。
【００２９】
上述の例では、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」のイベント入力及びイベント出力の全ては、変数「ａ」に関連してもよい。しかしながら、いくつかの例では、イベント２０２は、異なるイベント入力及びイベント出力を有してもよい。このように、いくつかの実施形態では、イベント入力及びイベント出力の割り当ては、イベント２０２のイベントのそれぞれのイベント入力のそれぞれが初期イベント２０２の他のイベントのイベント入力に対応してもよいように、イベント２０２のイベント入力及びイベント出力に対して共同体動作（union operation）を実行することを含んでもよい。共同体動作は、イベント２０２のそれぞれのイベントのイベント出力のそれぞれが初期イベント２０２の他のイベントのイベント出力に対応してもよいように、実行されてもよい。
【００３０】
例えば、イベント「ｅ１．１」は、イベント「ｅ１．１」のイベント入力及びイベント出力としてもよい入力変数及び出力変数として変数「ａ」及び「ｂ」を有してもよい関数「ｆ１．１（ａ，ｂ）」に関連してもよい。加えて、イベント「ｅ２．１」は、イベント「ｅ２．１」のイベント入力及びイベント出力としてもよい入力変数及び出力変数として変数「ｂ」及び「ｃ」を有してもよい関数「ｆ２．１（ｂ，ｃ）」に関連してもよい。このように、共同体動作は、イベント「ｅ１．１」及び「ｅ２．１」のそれぞれが関数「ｆ１．１（ａ，ｂ）」及び「ｆ２．１（ａ，ｂ）」の変数「ａ」、「ｂ」及び「ｃ」に関連する、対応するイベント入力及びイベント出力を有してもよいように、イベント「ｅ１．１」及び「ｅ２．１」のイベント入力及びイベント出力に対して実行されてもよい。
【００３１】
具体的には、いくつかの実施形態では、シンボリック入力変数「ａ１．１」、「ｂ１．１」及び「ｃ１．１」並びにシンボリック出力変数「ａ１．１」、「ｂ１．１」及び「ｃ１．１」は、イベント「ｅ１．１」のために生成されてもよい。同様に、シンボリック入力変数「ａ２．１」、「ｂ２．１」及び「ｃ２．１」並びにシンボリック出力変数「ａ２．１」、「ｂ２．１」及び「ｃ２．１」は、イベント「ｅ２．１」のために生成されてもよい。これらの実施形態及び他の実施形態において、式「（ａ１．１，ｂ１．１，ｃ１．１）→ｆ１．１→（ａ１．１´，ｂ１．１´，ｃ１．１´）」及び式「（ａ２．１，ｂ２．１，ｃ２．１）→ｆ２．１→（ａ２．１´，ｂ２．１´，ｃ２．１´）」は、イベント「ｅ１．１」及び「ｅ２．１」に対してそれぞれ生成されてもよい。このように、イベント「ｅ１．１」及び「ｅ２．１」は、互いに対応するイベント入力及びイベント出力を有してもよい。
【００３２】
また、プリプロセスフェーズ２０４は、等価イベント検出（equivalent event detection）に関連する動作に対応してもよいブロック２１４を含んでもよい。等価イベント検出の間、初期イベント２０２の２つ又は３つ以上のイベントが等価であるか否かが決定されてもよい。加えて、初期イベント２０２のイベントは、初期イベント２０２のイベントシーケンスと等価であるか否かが決定されてもよい。イベントは、入力、出力及び関連する動作が実質的に同一の結果を生成するとき、互いに等価である又はイベントシーケンスと等価であると見なされてもよい。例えば、上述のイベント「ｅ５」は、説明された例において「ｆ５（ａ）＝（ｆ２（ｆ１（ａ）））」であるので、イベント「ｅ１」の発生に次いでイベント「ｅ２」が発生するイベントシーケンスと等価であってもよい。
【００３３】
さらに、プリプロセスフェーズ２０４は、余分なイベントの除去に関連する動作に対応してもよいブロック２１６を含んでもよい。名前が示すように、余分なイベントの除去の間、余分なイベントは除去されてもよい。余分なイベントは、他のイベント又は他のイベントシーケンスと等価であってもよいイベントであってもよい。例えば、イベント「ｅ５」は、イベントシーケンス「ｅ１→ｅ２」と等価であってもよいので、余分なイベントであってもよい。余分なイベントの他の例は、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」の何れか１つに等価であるイベントであってもよい。
【００３４】
プリプロセスフェーズ２０４に続いて、動作は、制約セット決定フェーズ２０６の処理イベント２１８において処理イベント２１８に実行される。処理イベント２１８は、いくつかの例では、初期イベントの２０２の全てを含んでもよく、他の例では、１つ又は２つ以上の余分なイベントの除去により初期イベントの全てよりも少ないイベントを含んでもよい。制約セット決定フェーズ２０６の間、制約セットは、処理イベント２１８に基づいて決定されてもよい。制約セットは、処理イベント２１８に関連する可能なシーケンスを列挙してもよい。いくつかの例では、制約セットは、処理イベントに関連してもよい可能なイベントシーケンスの全てを列挙してもよい。
【００３５】
制約セット決定フェーズ２０６は、シーケンス実行制約（sequence-execution constraints）の決定に関連する動作に対応するブロック２２０を含んでもよい。シーケンス実行制約は、処理イベント２１８の実行順序を制約してもよい。例えば、いくつかの実施形態では、１つのイベントは、他のイベントの直前に発生してもよい。このように、シーケンス実行制約は、ペアのイベントの第１のイベントの第１イベント出力がペアのイベントの第２のイベントの第２イベント入力として使用されてもよいペアの処理イベント２１８に対して種々の可能な配列のそれぞれを決定することによって決定されてもよい。それに応じて、配列の数は、イベントシーケンスを制約してもよい。
【００３６】
加えて、いくつかの実施形態では、シンボリック順序変数は、処理イベントのそれぞれに割り当てられてもよい。これらの実施形態のいくつかでは、シンボリック順序変数は、関連するイベントのシーケンス順序位置を示す整数が割り当てられてもよい。例えば、イベントシーケンスの第１のイベントのシンボリック順序変数は「１」が割り当てられてもよく、イベントシーケンスの第２のイベントのシンボリック順序変数は「２」が割り当てられる等してもよい。
【００３７】
例えば、可能なイベント２１８は、上述のイベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」を含んでもよく、イベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」のシーケンス実行制約は、以下のように決定され且つ示されてもよい。イベント「ｅ１」はシンボリック順序変数「ｔ１」が割り当てられてもよく、イベント「ｅ２」はシンボリック順序変数「ｔ２」が割り当てられてもよく、イベント「ｅ３」はシンボリック順序変数「ｔ３」が割り当てられてもよく、イベント「ｅ４」はシンボリック順序変数「ｔ４」が割り当てられてもよい。イベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」の異なるペアのシーケンス順序の可能な配列は、適用可能なシンボリック順序変数と適用可能なシンボリック入力及び出力変数との間の対応関係と共に決定されてもよい。イベントの異なるペアのシーケンス順序の可能な配列は、以下の表１の第１カラムに示される。ここで、矢印「→」を使用して、矢印の左側のイベントは、矢印の右側のイベントの直前に発生することを示す。加えて、表１の第２カラムは、第１カラムで示されるイベント関係に関連するシンボリック順序変数の間の関係を示す対応式を示す。また、表１の第３カラムは、第１カラムに示されるイベント関係に関連するシンボリック入力変数とシンボリック出力変数との間の関係を示す対応式を示す。
【００３８】
【表１】
0006477269.tif 000002
【００３９】
また、制約セット決定フェーズ２０６は、シーケンス位置制約（sequence-position constraints）の決定に関連する動作に対応するブロック２２４を含んでもよい。シーケンス位置制約は、イベントの可能なシーケンスのイベントの位置を制約してもよい。いくつかの実施形態では、シーケンス位置制約は、処理イベント２１８の数及び／又は一度に実行可能な１つのイベントのみに基づくものであってもよい。例えば、いくつかの実施形態では、イベントは、イベントのシーケンスの可能なイベントの数よりも大きいイベントのシーケンスの位置を有さなくてもよい。加えて、これらの実施形態又は他の実施形態では、イベントは、２つ以上のイベントが同時に実行できないように、イベントのシーケンスの他のイベントと位置を共有できなくてもよい。いくつかの実施形態では、シーケンス位置制約は、処理イベント２１８に割り当ててもよいシンボリック順序変数に適用されてもよい。
【００４０】
例えば、処理イベント２１８がイベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」を含む例では、イベントの合計数は４であってもよい。このため、イベントシーケンスの第１位置のイベントのシンボリック順序変数が０であると仮定すると、シンボリック順序変数「ｔ１」、「ｔ２」、「ｔ３」及び「ｔ４」のそれぞれは、４つのイベントであるので、「５」よりも小さい整数が割り当てられるように制約されてもよい。加えて、シンボリック順序変数「ｔ１」、「ｔ２」、「ｔ３」及び「ｔ４」の何れも同一の整数が割り当てられなくてもよい。いくつかの例では、イベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」に関連するシーケンス位置制約は、以下の式「ｔ１≦３∧ｔ２≦３∧ｔ３≦３∧ｔ４≦３∧ｔ１≠ｔ２∧ｔ１≠ｔ３∧ｔ１≠ｔ４∧ｔ２≠ｔ３∧ｔ２≠ｔ４∧ｔ３≠ｔ４」によって示されてもよい。
【００４１】
いくつかの実施形態において、シーケンス位置制約及び／又はシーケンス実行制約は、コードアンダーテストの制御フローに基づいてもよい。例えば、いくつかの例では、コードアンダーテストの制御フローは、イベント「ｅ１．２」の対応するシンボリック順序変数「ｔ１．２」がイベント「ｅ２．２」の対応するシンボリック順序変数「ｔ２．２」よりも少ない整数を有するように制約されてもよいように、イベント「ｅ１．２」は、イベント「ｅ２．２」の前に常に発生すること指示してもよい。加えて、イベント「ｅ１．２」の直前にイベント「ｅ２．２」が発生する配列は、制御フローに基づいて可能ではなくてもよく、他のイベントの直前に起こる１つのイベントの可能な配列のリストから除去されてもよい。このように、シーケンス実行制約は、制御フロー情報がシーケンス位置情報及びシーケンス実行情報にエンコードされてもよいように、制御フローに基づいてさらにもっと限定されてもよい。
【００４２】
他の例のように、コードアンダーテストは、第１条件ｐ１が存在する場合にコードアンダーテストは、イベント「ｅ１．３」からイベント「ｅ２．３」に進んでもよく、第２条件ｐ２が存在する場合にコードアンダーテストは、イベント「ｅ１．３」からイベント「ｅ３．３」に進んでもよい分岐を有してもよい。このように、イベント「ｅ２．３」の直前に起こるイベント「ｅ１．３」に関連する配列は、第１条件ｐ１が存在する規定を含んでもよく、イベント「ｅ３．３」の直前に起こるイベント「ｅ１．３」に関連する配列は、第２条件ｐ２が存在する規定を含んでもよい。このように、シーケンス実行制約は、制御フローに基づいてさらにもっと限定されてもよい。また、イベント「ｅ１．３」のシンボリック順序変数「ｔ１．３」は、シーケンス位置制約が制御フローによってより制限されるように、イベント「ｅ３．３」及びイベント「ｅ３．３」のシンボリック順序変数「ｔ２．３」及び「ｔ３．３」のそれぞれよりも少なくなるように制約されてもよく、すなわちｐ１⇒ｔ１．３＜ｔ２．３及びｐ２⇒ｔ１．３＜ｔ３．３としてもよい。
【００４３】
また、制約セット決定フェーズ２０６は、イベント関係制約（event-relation constraints）の決定に関連する動作に対応するブロック２２６を含んでもよい。イベント関係制約は、処理イベント２１８のそれぞれのイベント出力に対する処理イベント２１８のイベントのそれぞれのイベント入力の間の関係を示し且つ規定してもよい。いくつかの実施形態では、イベント関係制約は、処理イベント２１８のシンボリック入力変数、シンボリック出力変数及びそれぞれの関数に対して規定されてもよい。
【００４４】
例えば、上述のように、シンボリック入力変数「ａ１」及びシンボリック出力変数「ａ１」は、イベント「ｅ１」に割り当てられてもよい。加えて、イベント「ｅ１」は、式「ａ＝ａ＋３」を含んでもよい関数「ｆ１（ａ）」に関連してもよい。このように、関数「ｆ１（ａ）」に対してシンボリック入力変数「ａ１」とシンボリック出力変数「ａ１」との間の関係を規定してもよいイベント関係制約は、生成されてもよい。具体的には、いくつかの実施形態では、イベント「ｅ１」のイベント関係制約は、「ｅ１：ａ１´＝ａ１＋３」で表されてもよい。同一の概念は、いくつかの実施形態では、イベント「ｅ２」、「ｅ３」及び「ｅ４」のイベント関係制約を「ｅ２：ａ２´＝２＊ａ２」、「ｅ３：ａ３´＝１」及び「ｅ４：ａ４´＝３＊ａ４−１」としてもよいように、イベント「ｅ２」、「ｅ３」及び「ｅ４」に適用されてもよい。
【００４５】
加えて、制約セット決定フェーズ２０６は、制約セットの形成に関連する動作に対応するブロック２２８を含んでもよい。いくつかの実施形態では、制約セットは、ブロック２２で決定されるシーケンス実行制約と、ブロック２２４で決定されるシーケンス位置制約と、ブロック２２６で決定されるシーケンス関係制約とを含んでもよい。
【００４６】
例えば、イベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」の制約セットは、表１のシーケンス実行制約「(ｔ２＝ｔ１＋１⇒ａ２＝ａ１’）∧（ｔ１ ＝ｔ２＋１⇒ａ１＝ａ２’）∧（ｔ３＝ｔ１＋１⇒ａ３＝ａ１’）∧（ｔ１＝ｔ３＋１⇒ａ１＝ａ３’）∧（ｔ４＝ｔ１＋１⇒ａ４＝ａ１’）∧（ｔ１＝ｔ４＋１⇒ａ１＝ａ４’）∧（ｔ３＝ｔ２＋１⇒ａ３＝ａ２’）∧（ｔ２＝ｔ３＋１⇒ａ２＝ａ３’）∧（ｔ４＝ｔ２＋１⇒ａ４＝ａ２’）∧（ｔ２＝ｔ４＋１⇒ａ２＝ａ４’）∧（ｔ４＝ｔ３＋１⇒ａ４＝ａ３’）∧（ｔ３＝ｔ４＋１⇒ａ３＝ａ４’）」を含んでもよい。また、制約セットは、シーケンス位置制約「ｔ１≦３∧t2≦３∧ｔ３≦３∧ｔ４≦３∧ｔ１≠ｔ２∧ｔ１≠ｔ３∧ｔ１≠ｔ４∧ｔ２≠ｔ３∧ｔ２≠ｔ４∧ｔ３≠ｔ４」及びシーケンス関係制約「“ｅ１：ａ１’＝ａ１＋３”、“ｅ２： ａ２’＝２＊ａ２”、“ｅ３：ａ３’＝１”及び“ｅ４：ａ４’＝３＊ａ４−１”」を含んでもよい。これらの制約は、初期イベント２０２及び処理イベント２１８の可能なイベントシーケンスをエンコードし且つ規定してもよい。
【００４７】
上述のように、処理イベント２１８は、ブロック２２８で形成される制約セットがコードアンダーテストの初期イベントに基づいてもよいように、初期イベント２０２に基づいてもよい。しかしながら、コードアンダーテストは、初期イベント２０２の初期見出しの後に見出されてもよい他のイベントを含んでもよい。そして、いくつかの実施形態では、制約セット決定フェーズ２０６は、見出されてもよい新たなイベントに基づいてブロック２２８で形成されてもよい制約セットの更新に関連する動作に対応するブロック２３０を含んでもよい。いくつかの実施形態では、制約セットは、図３を参照して説明される方法３００に従って更新されてもよい。
【００４８】
制約セット決定フェーズ２０６に続いて、動作は、テスト結果生成フェーズ２１０において最終制約セット（finalized constraint set）２２２に実行される。いくつかの例では、最終制約セット２２２は、ブロック２２８で形成された初期制約セットを含んでもよく、他の例では、最終制約セット２２２は、ブロック２３０で更新されてもよい更新制約セット（updated constraint set）を含んでもよい。加えて、最終制約セット２２２は、コードアンダーテストのイベントスペースを実際に発生してもよいこれらのイベントシーケンスに限定されてもよいように、コードアンダーテストの可能なイベントシーケンスを含んでもよい。一方、最終制約セット２２２を除き、イベントスペースは、除去されてもよく及び／又は達成可能でなくてもよいいくつかのイベントシーケンスを含んでもよい。
【００４９】
テスト結果生成フェーズ２１０は、最終制約セット２２２の解に関連する動作に対応するブロック２３２を含んでもよい。制約セットの解は、適当な制約ソルバ（constraint solver）を使用して実行してもよい。例えば、いくつかの実施形態では、制約ソルバは、シンボリック順序変数の全ての可能な値を列挙してもよく、制約においてエンコードされた全ての可能なイベントシーケンスを列挙してもよい。例えば、制約ソルバは、ソルバによって見出された有効なイベントシーケンスを示してもよいシンボリック順序変数への有効値割り当てを探し出してもよい。
【００５０】
また、テスト結果生成フェーズ２１０は、解制約セット（solved constraint set）に基づくコードアンダーテストのイベントスペースの探索に関連する動作に対応するブロック２３４を含んでもよい。いくつかの実施形態では、イベントスペースの探索は、クエリの回答、でバグ動作の実行、テスト生成動作の実行及び／又はイベントスペースのチェックを含んでもよい。テスト結果生成フェーズ２１０に関連する動作に含まれる処理量は、探索されてもよいイベントスペースが最終制約セット２２２に基づいて低減されてもよいので、従来のように実行したときと比較して低減することができる。
【００５１】
図３は、本明細書に記載される少なくとも１つの実施形態に従って、制約セットを更新する一例の方法３００のフローチャートである。方法３００は、適当な装置、機器又はデバイスで実行されてもよい。例えば、方法３００は、図１Ｂの電子デバイス１０２のテストモジュール１０６は、方法３００に関連する動作の１つ又は２つ以上を実行してもよい。個別のブロックとして説明されるものの、方法３００の種々のブロックは、所望の実装に依存して、付加的なブロックに分割されてもよく、より少ないブロックに組み合わされてもよく、削除されてもよい。加えて、上述のように、いくつかの実施形態では、方法３００は、図２のブロック２３０で実行されてもよい。
【００５２】
方法３００は、コードアンダーテストが受信されてもよいブロック３０２において開始されてもよい。例えば、フロー２００において初期イベント２０２が抽出されたコードアンダーテストは、ブロック３０２において受信されてもよい。ブロック３０４において、新しいイベント「ｅ」は見出されてもよい。例えば、コードアンダーテストがウェブベースのアプリケーション（Web-based application）に関連するとき、新たなイベント「ｅ」は、新しいウェブページがひらくときにウェブブラウザにより見出されてもよい。他の例では、コードアンダーテストがアンドロイド（Android、登録商標）に関連するとき、関連するアンドロイド（登録商標）のランタイム（runtime）は、新たなスクリーンが表れるときに新たなイベントを見出してもよい。新たなイベント「ｅ」は、先に見出されていないイベントであってもよい。例えば、初期イベント２０２がイベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ５」を含む例では、新たなイベント「ｅ」は、初期に見出されていなかった新たなイベント「ｅ６」にしてもよい。
【００５３】
ブロック３０６において、新しいイベント「ｅ」は、更新されてもよい制約セットにたいして余分であるか否かが決定されてもよい。例えば、新しいイベント「ｅ」は、制約セットを形成するために使用されるイベントに対して余分であるか否かが決定されてもよい。いくつかの実施形態では、あらたなイベントは、新たなイベント「ｅ」の機能が制約セットでエンコードされたイベントシーケンスによって取得されてもよいか否かを決定することのよって、余分であるか否かが決定されてもよい。新たなイベント「ｅ」の機能が取得されてもよい場合、新たなイベント「ｅ」は余分であると決定されてもよく、新たなイベント「ｅ」の機能が取得されない場合、制約セットは、新たなイベント「ｅ」に関連する制約によって更新されてもよいことが決定されてもよい。
【００５４】
例えば、イベント「ｅ６」は、動作「ａ＝３ａ＋８」を含んでもよい関数「ｆ６（ａ）」に関連してもよい。「ｅ６」が制約セット（以下の式で「Ｔ」で示される）でエンコードされるいくつかのイベントシーケンスと等価であるか否かを検査するために、制約セットは、以下の式「Ｔ∧（ａ’１＝３ａ０＋８∨ａ’２＝３ａ０＋８∨ａ’３＝３ａ０＋８∨ａ’４＝３ａ０＋８)” ここで“ａ０＝（ｔ１＝０？ａ１:（ｔ２＝０？ａ２ :（ｔ３＝０？ａ３:ａ４）））」で示されるように増やされてもよい。上述の式は以下の式「ｔ１＝０,ｔ２＝２,ｔ３＝３,ｔ４＝１；（ｅ１→ｅ４→ｅ２→ｅ３）」をもたらしてもよい。ここで、「ｅ１→ｅ４」は、イベント「ｅ６」と等価であってもよい。このため、イベント「ｅ６」は、制約セット「Ｔ」に対して余分であると見なされてもよい。
【００５５】
他の例では、新たなイベント「ｅ７」は、ブロック３０７で見出されてもよく、新たなイベント「ｅ７」は動作「ａ＝４ａ−２」を含んでもよい関数「ｆ７（ａ）」に関連してもよい。この例において、制約セット（以下の式で「Ｔ」で示される）は、以下の式「Ｔ∧（ａ’１＝４ａ０−２∨ａ’２＝４ａ０−２∨ａ’３＝４ａ０−２∨ａ’４＝４ａ０−２）」に示すように増やされてもよい。ここで、上述の「ａ０」は充足されなくてもよい。このため、イベント「ｅ７」は、制約セット「Ｔ」に対して余分ではないと見なされてもよい。
【００５６】
新たなイベント「ｅ」が余分であると見なされたとき、方法３００は、新たなイベント「ｅ」が破棄され又は無視されてもよいブロック３０８に進んでもよい。ブロック３０８に続いて、方法３００はブロック３０４に戻ってもよい。
【００５７】
新たなイベント「ｅ」が余分ではないと見なされたとき、方法３００はブロック３１０に進んでもよい。ブロック３１０において、制約セットは、新たなイベント「ｅ」のために逐次更新されてもよい。逐次の更新において、制約セットの古い制約の１つ又は２つ以上は維持され、新たなイベント「ｅ」に関連する新たな制約は決定され且つ制約セットに付加されてもよい。例えば、新たなシーケンス実行制約は、決定され、次いで、新たなイベント「ｅ」を含むペアに対する配列として付加されてもよい。また、シーケンス位置制約は、イベントシーケンスの他の可能なイベントとして新たなイベント「ｅ」の付加を反映するように更新されてもよい。また、新たなイベント「ｅ」に関連するイベント関係制約は、決定され且つ制約セットに付加されてもよい。
【００５８】
例えば、イベント「ｅ１」、「ｅ２」、「ｅ３」及び「ｅ４」に関連する制約セットに対して、上述の表１に示されるシーケンス実行制約は、以下の表２に示すようにイベント「ｅ７」に関連するシーケンス実行制約を含むように増やされてもよい。また、以下に説明するように、「ｅ７」に関連しない制約は、完全のまま維持されてもよい。
【００５９】
【表２】
0006477269.tif 000003
【００６０】
さらに、シーケンス位置制約は、イベントシーケンスの可能なイベントの数が４から５に増えてもよいので、更新されてもよい。例えば、イベント「ｅ１」、「ｅ２」、「ｅ３」、「ｅ４」及び「ｅ７」に関連するシンボリック位置変数に配置されたシーケンス位置制約は、これらのイベントが「ｔ１≦４∧ｔ２≦４∧ｔ３≦4∧ｔ４≦４∧ｔ１≠ｔ２∧ｔ１≠ｔ３∧ｔ１≠ｔ４∧ｔ２≠ｔ３∧ｔ２≠ｔ４∧ｔ３≠ｔ４∧ｔ７≦４∧ｔ７≠ｔ１∧ｔ７≠ｔ２∧ｔ７≠ｔ３∧ｔ７≠ｔ４」のように表らされてもよいように修正されてもよい。
【００６１】
加えて、イベント「ｅ７」のイベント関係制約は、決定され、「ｅ７：ａ７´＝４＊ａ７−２」として生成されてもよい。次いで、イベント関係制約「ｅ７：ａ７´＝４＊ａ７−２」は、制約セットのイベント関係制約「ｅ１：ａ１´＝ａ１＋３」、ｅ２：ａ２´＝２＊ａ２」、「ｅ３：ａ３´＝１」及び「ｅ４：ａ４´＝３＊ａ４−１」に付加されてもよい。
【００６２】
また、いくつかの実施形態では、新たなイベント「ｅ」は、関連するコードアンダーテストの制御フローに基づいて他のイベントが実行された後のみに実行されてもよい。これにより、いくつかの実施形態では、ブロック３１０は、上述のように、シーケンス実行制約及び／又はシーケンス位置制約を制御フローに基づいて更新し又は修正することを含んでもよい。
【００６３】
ブロック３１０に続いて、方法３００は、他の新たなイベント「ｅ」が見出されてもよいブロック３０４に戻ってもよい。これにより、方法３００を使用して、初期イベントが見出された後に見出されてもよい他のイベントに基づいて制約セットを更新してもよい。
【００６４】
いくつかの実施形態では、イベントシーケンスのエンコードは、プロパティの検査のためにクエリされてもよい。プロパティと制約セット「Ｔ」との結合は、プロパティの検査の間に制約ソルバによって解かれてもよい。制約ソルバが解を探し出した場合、プロパティは有効であると見なされてもよい。例えば、プロパティ「ａの値が最後に１０であるような、４イベントシーケンスはあるか？（Is there a 4-event sequence such a's value is 10 in the end?）」は、制約「Ｔ∧（（ｔ１＝３∧ａ’１＝１０）∨（ｔ２＝３∧ａ’２＝１０）∨（ｔ３＝３∧ａ’３＝１０）∨（ｔ４＝３∧ａ’４＝１０）」を解く試みによって検査されてもよい。この具体的な例では、制約ソルバは、イベントシーケンス「ｅ３→ｅ４→ｅ１→ｅ２」がこのプロパティを充足し且つプロパティが有効であることを示す解「ｔ１＝２，Ｔ２＝３，Ｔ３＝０，Ｔ４＝１」を戻してもよい。他の例では、プロパティ「ａの値が実行の後に０ｄきるようなシーケンスはあるか（初期的にａ＝１）？（Is there a sequence such that a's value can ever be 0 after the execution (initially a=1)?）」は、制約「Ｔ∧（ａ’１＝０∨ａ’２＝０∨ａ’３＝０∨ａ’４＝０）」を解く試みによって検査されてもよい。この具体的な例では、制約ソルバは、解を探し出さなくてもよい。このように、このプロパティは、（制約によって規定される全ての可能なイベントシーケンスのために）保持されてもよく、無効であるとみなされてもよい。
【００６５】
当業者は、本明細書に開示されたこれらの処理及び方法又は他の処理及び方法において、関数は異なる順序で実装されてもよいことを理解するであろう。また、概略的なステップ及び動作のみが一例として提供され、開示される実施形態の本質を損なうことなく、ステップ及び動作のいくつかは、付加的であり、組み合わせてより少ないステップ及び動作にしてもよく、付加的なステップ及び動作に拡張されてもよい。
【００６６】
上述のように、本明細書で説明される実施形態は、以下により詳細に説明されるように、様々なコンピュータハードウェア又はソフトウェアモジュールを含む特定用途のコンピュータ及び汎用のコンピュータ（図１Ｂのプロセッサ１１０等）を含んでもよい。また、上述のように、本明細書で説明される実施形態は、コンピュータが実行可能な命令又はデータ構造を格納して運搬又は所有するコンピュータ読み取り可能な媒体を使用して実装されてもよい。
【００６７】
本明細書で使用されるとき、用語「モジュール（module）」又は「コンポーネント（component）」は、コンピューティングシステムの汎用ハードウェア（例えば、コンピュータが読み取り可能な媒体、処理デバイス等）により格納及び／又は実行してもよいモジュール又はコンポーネント及び／又はソフトウェアオブジェクト又はソフトウェアルーティーンの動作を実行するように構成される特定のハードウェア実装を称してもよい。いくつかの実施形態において、本明細書に記載される異なるコンポーネント、モジュール、エンジン及びサービスは、コンピューティングシステムで（異なるスレッドとして）実行されるオブジェクト又は処理として実装されてもよい。本明細書に記載されるシステム及び方法のいくつかは、全般的に、（汎用ハードウェアに格納及び／又は実行される）ソフトウェア実装され、特定のハードウェア実装又ソフトウェア実装及びハードウェア実装の組み合わせが可能であり、予想される。本明細書において、「コンピューティングエンティティ（computing entity」は、本明細書で先に規定したコンピューティングシステム、若しくはいずれかのモジュール又はコンピューティングシステムで走るモジュールの組み合わせのようなコンピューティングシステムとしてもよい。
【００６８】
明細書で引用される全ての例及び条件的な言語は、教育的な目的を意図したものであり、技術を進歩させるため発明者が貢献した発明及び概念を読み手が理解することを支援するためのものであり、具体的に引用された例及び条件に限定されることなく解釈されるものである。本開示の実施形態を詳細に説明してきたが、本開示の精神及び範囲を逸脱することなく、種々の変化、置換、変更が可能であることを理解すべきである。
【図１Ａ】
0006477269.tif 000004
【図１Ｂ】
0006477269.tif 000005
【図２】
0006477269.tif 000006
【図３】
0006477269.tif 000007