(57)【要約】      （修正有）【課題】イベント駆動型アプリケーションを解析するデバイスを提供する。【解決手段】デバイスは、１つ以上のプロセッサを含み、記号環境において、有効にされているイベント集合を見出し５０４、イベントをランダムに選択して実行する５０６。記号動的半順序簡約を用いて、有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新し、読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄する５１０。【選択図】図５Ａ
2018026116.tif 000002
【特許請求の範囲】
【請求項１】
１つ以上のプロセッサを有するデバイスであって、前記１つ以上のプロセッサは、
記号環境において、有効にされているイベント集合のうちのイベントを実行し、
記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新し、
読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄する
よう構成されている、デバイス。
【請求項２】
前記１つ以上のプロセッサは、記号実行のために前記イベントをランダムに選択するようさらに構成されている、請求項１に記載のデバイス。
【請求項３】
前記１つ以上のプロセッサは、前記有効にされているイベント集合のイベント系列の境界に到達したかどうかを判定するようさらに構成されている、請求項１に記載のデバイス。
【請求項４】
前記１つ以上のプロセッサは、前記有効にされているイベント集合の前記境界に到達した場合、初期イベント系列を生成するようさらに構成されている、請求項３に記載のデバイス。
【請求項５】
前記１つ以上のプロセッサは、前記イベント系列における未探索のイベントを識別するようさらに構成されている、請求項４に記載のデバイス。
【請求項６】
前記１つ以上のプロセッサは、記号実行によって前記未探索のイベントを実行するようさらに構成されている、請求項５に記載のデバイス。
【請求項７】
前記１つ以上のプロセッサは、前記有効にされているイベント集合における各状態を反復処理して、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの前記永続集合及び前記訪問済みイベントを更新するようさらに構成されている、請求項１に記載のデバイス。
【請求項８】
複数の動作を実行するための又は前記複数の動作の実行を制御するための、処理デバイスにより実行可能なコンピュータ命令を記憶している非一時的なコンピュータ読み取り可能な媒体であって、前記複数の動作は、
記号環境において、有効にされているイベント集合のうちのイベントを実行する動作と、
記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新する動作と、
読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄する動作と、
を含む、コンピュータ読み取り可能な媒体。
【請求項９】
前記複数の動作は、記号実行のために前記イベントをランダムに選択する動作をさらに含む、請求項８に記載のコンピュータ読み取り可能な媒体。
【請求項１０】
前記複数の動作は、前記有効にされているイベント集合の境界に到達したかどうかを判定する動作をさらに含む、請求項８に記載のコンピュータ読み取り可能な媒体。
【請求項１１】
前記複数の動作は、前記有効にされているイベント集合の前記境界に到達した場合、イベント系列を生成する動作をさらに含む、請求項１０に記載のコンピュータ読み取り可能な媒体。
【請求項１２】
前記複数の動作は、前記イベント系列における未探索のイベントを識別する動作をさらに含む、請求項１１に記載のコンピュータ読み取り可能な媒体。
【請求項１３】
前記複数の動作は、記号実行によって前記未探索のイベントを実行する動作をさらに含む、請求項１２に記載のコンピュータ読み取り可能な媒体。
【請求項１４】
前記複数の動作は、前記有効にされているイベント集合における各状態を反復処理して、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの前記永続集合及び前記訪問済みイベントを更新する動作をさらに含む、請求項８に記載のコンピュータ読み取り可能な媒体。
【請求項１５】
イベント駆動型アプリケーションを解析する方法であって、
記号環境において、有効にされているイベント集合のうちのイベントを実行するステップと、
記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新するステップと、
読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄するステップと、
を含む、方法。
【請求項１６】
前記有効にされているイベント集合における各状態を反復処理して、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの前記永続集合及び前記訪問済みイベントを更新するステップをさらに含む、請求項１５に記載の方法。
【請求項１７】
前記有効にされているイベント集合のイベント系列の境界に到達したかどうかを判定するステップをさらに含む、請求項１５に記載の方法。
【請求項１８】
前記有効にされているイベント集合の前記境界に到達した場合、初期イベント系列を生成するステップをさらに含む、請求項１７に記載の方法。
【請求項１９】
前記イベント系列における未探索のイベントを識別するステップをさらに含む、請求項１８に記載の方法。
【請求項２０】
記号実行によって前記未探索のイベントを実行するステップをさらに含む、請求項１９に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本明細書に記載の実施形態は、イベント駆動型アプリケーションの解析のための記号（シンボリック）動的半順序簡約（symbolic  dynamic  partial  order  reduction）に関する。
【背景技術】
【０００２】
ウェブアプリケーション及びモバイルアプリケーション等のイベント駆動型アプリケーションは、ユーザ生成型アクション（例えば、マウスクリック、キーストローク等）及びシステム生成型アクション（例えば、プログラムのロード）等のイベント（例えば、システムハードウェア又はソフトウェアについての意味のある識別可能な出来事）に応答する。
【０００３】
本出願において特許請求される主題は、あらゆる欠点を解決する実施形態又は上記のような環境においてのみ動作する実施形態に限定されるものではない。そうではなく、この背景技術の記載は、本明細書に記載のいくつかの実施形態が実施され得る１つの例示的な技術領域を示すために提供されているに過ぎない。
【発明の概要】
【０００４】
一実施形態の一態様に従うと、デバイスは、１つ以上のプロセッサを含む。前記１つ以上のプロセッサは、記号環境（symbolic  environment）において、有効にされているイベント集合の１つ以上のイベントのうちのイベントを実行するよう構成され得る。さらに、前記１つ以上のプロセッサは、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合（persistent  set）及び訪問済みイベントを更新するよう構成され得る。前記１つ以上のプロセッサはまた、読み取り−書き込み独立関係にある（read-write  independent）、パス制約とイベントとの各ペアを破棄するよう構成され得る。
【０００５】
実施形態の目的及び利点が、少なくとも請求項において特に示される要素、特徴、及び組合せにより、実現及び達成される。
【０００６】
前述の総括的な説明及び以下の詳細な説明の両方ともが、例示的且つ説明的なものであり、特許請求される発明を限定するものではないことを理解されたい。
【図面の簡単な説明】
【０００７】
例示的な実施形態が、添付の図面を使用して、より具体的且つ詳細に記載及び説明される。
【図１Ａ】イベント駆動型アプリケーションのユーザインタフェースのスクリーンショットを示す図。
【図１Ｂ】商品テーブルに商品を追加し、商品の数を１つだけ増加させる関数の例示的なコードを示す図。
【図２Ａ】イベント駆動型アプリケーションのユーザインタフェースの別のスクリーンショットを示す図。
【図２Ｂ】商品テーブルから全ての商品を削除し、商品の数を０に設定する関数の例示的なコードを示す図。
【図３】図３Ａは、２つのパスを含む例示的な実行シナリオを示す図。図３Ｂは、２つのパスを含む別の例示的な実行シナリオを示す図。図３Ｃは、２つのパスを含むさらに別の例示的な実行シナリオを示す図。
【図４】図４Ａは、イベント系列のトレースを示す図。図４Ｂは、図４Ａのトレースの訪問済みイベント及び未訪問のイベントを示す図。図４Ｃは、図４Ａのトレースの未探索のイベントを示す図。図４Ｄは、イベント系列の新たな拡張されたトレースを示す図。
【図５Ａ】イベント駆動型アプリケーションを解析する例示的な方法のフローチャート。
【図５Ｂ】イベント駆動型アプリケーションを解析する例示的な方法のフローチャート。
【図６】例示的なコンピューティングデバイスのブロック図。
【発明を実施するための形態】
【０００８】
本明細書に記載の実施形態は、イベント駆動型アプリケーションを解析することに関する。より詳細には、本明細書に記載の実施形態は、記号ベースの動的半順序簡約を用いて、イベント駆動型アプリケーションを解析することに関する。
【０００９】
イベント駆動型アプリケーション（例えば、ウェブアプリケーション及びモバイルアプリケーション）が普及している。しかしながら、これらのアプリケーションは、広く認識されている状態空間の爆発に起因して、不具合をテストし、デバッグし、不具合の根本原因を明らかにするのが難しい。イベント駆動型アプリケーションを効果的にテストするためには、解析精度を損なわないようにしつつイベント系列空間を簡約することが重要である。多くの最適化機構の中で、動的半順序簡約（ＤＲＯＰ：dynamic  partial  order  reduction）が、状態空間の爆発を低減するための効果的な方法論と考えられる。ＤＲＯＰは、典型的には、必須のプログラムテスト及び検証、並びに並行ソフトウェアテストのモデル検査の領域において使用される。
【００１０】
最近では、ＤＲＯＰに基づくイベント駆動型アプリケーションのステートレスモデル検査が、実際的なウェブアプリケーションをテストするために使用されている。ＤＲＯＰは、解析のスケーラビリティを向上させることが可能であり得るが、従来の方法が、具体シナリオ（concrete  scenario）において適用され、したがって、解析精度を低減させてしまう。
【００１１】
本明細書に記載の様々な実施形態は、記号ベースの動的半順序簡約（例えば、記号実行と動的半順序簡約との組合せ）を用いることができ、これは、スケーラビリティを損なわないようにしつつイベント駆動型アプリケーションの解析の精度を向上させることができる。
【００１２】
本発明の実施形態が、添付の図面を参照しながら説明される。
【００１３】
図１Ａは、イベント駆動型アプリケーションのユーザインタフェースのスクリーンショット１００である。図１Ａに示されるように、このアプリケーションは、商品テーブルに商品（例えば、食料雑貨の商品）を追加するよう構成されている。ユーザは、商品の名前、数量、及び店を指定することができる。さらに、ユーザは、「商品追加」タブを選択することにより、商品テーブルに商品を追加することができる。
【００１４】
図１Ｂは、商品テーブルに商品を追加する関数の例示的なコード１２０を示している。図１Ｂに示されるように、商品について提供された名前が、有効であり（例えば、無効な文字を含まず）、提供された数量が、有効である（例えば、有効な数字を含む）場合、商品の総数（”total_product_num”）が、１だけ増加され得、その商品が、商品テーブルに追加され得る。
【００１５】
図２Ａは、このイベント駆動型アプリケーションのユーザインタフェースの別のスクリーンショット１５０である。図２Ａに示されるように、このアプリケーションは、商品テーブルから、全ての商品項目（例えば、食料雑貨の商品の全て）を削除するよう構成されている。図２Ｂは、商品テーブルから全ての商品項目を削除し、商品の数を０に設定する関数の例示的なコード１７０を示している。
【００１６】
図３Ａは、ポイント３０２、ポイント３０４、及びポイント３０６を含むパス３０１と、ポイント３０２、ポイント３０８、及びポイント３０６を含む別のパス３０３と、を含む例示的な実行シナリオ３００を示している。パス３０１において、ポイント３０２にて、商品テーブルに商品を追加する関数が呼び出され得る。しかしながら、この例において、商品テーブルに追加されようとしている商品の名前が、無効であり（例えば、無効な文字を含み）、シナリオは、ポイント３０４に進む。さらに、ポイント３０４にて、商品テーブルから全ての商品項目を削除する関数が呼び出され、シナリオは、ポイント３０６に進む。
【００１７】
パス３０３において、ポイント３０２にて、商品テーブルから全ての商品項目を削除する関数が呼び出され、シナリオは、ポイント３０８に進む。さらに、ポイント３０８にて、商品テーブルに商品を追加する関数が呼び出され得る。しかしながら、商品テーブルに追加されようとしている商品の名前が、無効であり（例えば、無効な文字を含み）、シナリオは、ポイント３０６に進む。
【００１８】
図３Ｂは、ポイント３２２、ポイント３２４、及びポイント３２６を含むパス３２１と、ポイント３２２、ポイント３２８、及びポイント３２６を含む別のパス３２３と、を含む例示的な実行シナリオ３２０を示している。パス３２１において、ポイント３２２にて、商品テーブルに商品を追加する関数が呼び出され得る。しかしながら、提供された数量が、無効であり（例えば、有効な数字ではなく）、シナリオは、ポイント３２４に進む。さらに、ポイント３２４にて、商品テーブルから全ての商品項目を削除する関数が呼び出され、シナリオは、ポイント３２６に進む。
【００１９】
パス３２３において、ポイント３２２にて、商品テーブルから全ての商品項目を削除する関数が呼び出され、シナリオは、ポイント３２８に進む。さらに、ポイント３２８にて、商品テーブルに商品を追加する関数が呼び出され得る。しかしながら、提供された数量が、無効であり（例えば、有効な数字ではなく）、シナリオは、ポイント３２６に進む。
【００２０】
シナリオ３００及びシナリオ３２０はそれぞれ冗長である。より詳細には、シナリオ３００（図３Ａ）に関して、パス３０１及びパス３０３はそれぞれ、ポイント３０６で終了し、したがって、これら２つのパスのうち１つのパスのみ探索することで十分である。同様に、シナリオ３２０（図３Ｂ）に関して、パス３２１及びパス３２３はそれぞれ、ポイント３２６で終了し、したがって、これら２つのパスのうち１つのパスのみ探索することで十分である。シナリオ３００及びシナリオ３２０の各々は、状態空間の爆発を不必要にもたらし得る。
【００２１】
図３Ｃは、ポイント３４２、ポイント３４４、及びポイント３４６を含むパス３４１と、ポイント３４２、ポイント３４８、及びポイント３５０を含む別のパス３４３と、を含む例示的な実行シナリオ３４０を示している。パス３４１において、ポイント３４２にて、商品テーブルに商品を追加する関数が呼び出され得る。このシナリオにおいて、商品テーブルに追加されようとしている商品の名前及び数量の両方が、有効であり、シナリオは、ポイント３４４に進む。さらに、ポイント３４４にて、商品テーブルから全ての商品項目を削除する関数が呼び出され、シナリオは、ポイント３４６に進む。
【００２２】
パス３４３において、ポイント３４２にて、商品テーブルから全ての商品項目を削除する関数が呼び出され、シナリオは、ポイント３４８に進む。さらに、ポイント３４８にて、商品テーブルに商品を追加する関数が呼び出され得る。さらに、商品テーブルに追加されようとしている商品の名前及び数量の両方が、有効であるので、シナリオは、ポイント３５０に進む。図示されるように、パス３４１及びパス３４３は、異なるポイントで終了する。
【００２３】
半順序簡約（ＰＯＲ）に関して、イベント群（例えば、イベントＸ及びイベントＹ）は、これらのイベントが、いずれの実行可能なイベント系列においても互いに対して影響を及ぼさない場合、独立関係にある。別の言い方をすると、イベント群（例えば、イベントＸ及びイベントＹ）が、互いを有効又は無効にせず、これらのイベントが、可換である（commutative）場合、これらのイベントは独立関係にある。
【００２４】
さらに、関係Ｉは、任意の（Ｘ，Ｙ）∈Ｉ及び任意のトレースに対し、これら２つのイベントのうちの一方のイベントにより書き込まれ、これら２つのイベントのうちの他方のイベントにより読み取られる又は書き込まれる共有位置が存在しない場合、読み取り−書き込み独立関係である。イベント群（例えば、イベントＸ及びイベントＹ）は、これらのイベントが両方とも有効にされ、依存関係にある（読み取り／書き込み独立関係にない）場合、競合する。
【００２５】
動的半順序簡約を用いて、実行時に、イベント間の依存関係を識別することができる。例えば、図４Ａは、イベント系列のトレース４００Ａを示している。図４Ｂは、訪問済みイベント４０２と、未訪問のイベント４０４、未訪問のイベント４０６、及び未訪問のイベント４０８と、を含むトレースτを示している。一実施形態に従うと、有効にされているイベント集合のうちの部分集合を含み得る永続集合と、各状態についての訪問済み遷移と、が更新され得る。永続集合は、互いを無効又は有効にする、読み取り−書き込み依存関係にあるイベント群を含み得る。
【００２６】
さらに、トレースτは、その最終状態が未探索のイベントを有するまで、簡約され得る。別の言い方をすると、プロセスは、未探索のイベント４０８（図４Ｃ参照）が見出されるまで、バックトラッキングすること（例えば、最初の未探索のイベントが見出されるまで、バックトラッキングすること）を含み得る。さらに、図４Ｄに示されるように、（τ及びイベント４０８を最大限まで拡張して）新たなトレース４００Ｄが探索され得る。
【００２７】
具体シナリオにおける読み取り−書き込み依存関係解析は、アグレッシブ過ぎる（too  aggressive）ことがあり、不完全なこともある。一例において、”name（名前）”:=”@@@”又は”quantity（数量）”:=”test”である場合、これらの入力を伴う”add（追加）”イベントと”remove_all（全て削除）”イベントとは、具体環境（concrete  environment）において、独立関係にあるとして間違って正当化される。例えば、”name”==”kiwi”且つ”quantity”==”10”である場合、”add”イベントと”remove_all”イベントとは、依存関係にある。
【００２８】
記号環境において、実行は、具体値実行中に使用される実際の値を得るのではなく、入力について記号値を使用することを含み得る。具体環境の一例において、”name”及び”quantity”が、無効な具体値をもって設定され（例えば、name==”a@b”  &&  quantity==”1&4”）、したがって、１つの具体パス（concrete  path）のみが実行され得る。記号環境の一例において、”name”及び”quantity”が、未知の変数として扱われ得、”add”イベントにおける複数のパス（例えば、この例では３つのパス）が、対応するパス制約をもって探索され得る。この例において、３つの状態が、これら３つのパスに対応し得る。
【００２９】
例えば、正規表現制約”!(/^[a-zA-Z0-9]+$/.test(name))”に関して、”name”が正規表現に合致しない場合、このシナリオにおいて、addイベントは、remove_allイベントと独立関係にある。例えば、name==”@@@”又は正規表現制約”!(/^[a-zA-Z0-9]+$/.test(name))”を満たす他の値は、（例えば、ＳＭＴソルバによって）後で判定され得る。
【００３０】
さらに、正規表現制約”(/^[a-zA-Z0-9]+$/.test(name)  &&  quantity.isNaN())”に関して、”name”が正規表現に合致するが、”quantity”が有効な数字ではない場合、addイベントは、remove_allイベントと独立関係にあり得る。
【００３１】
さらに、正規表現制約”(/^[a-zA-Z0-9]+$/.test(name)  &&  !quantity.isNaN())”に関して、”name”が正規表現に合致し、”quantity”が有効な数字である場合、addイベントは、remove_allイベントと依存関係にある。なぜならば、これらのイベントは、共有変数に対して作用するからである。
【００３２】
図５Ａ及び図５Ｂは、本明細書に記載の少なくとも１つの実施形態に従って構成される、イベント駆動型アプリケーションを解析する方法５００のフローチャートを示している。個別のブロックとして図示されているが、様々なブロックは、所望の実装に応じて、追加のブロックに分割されることもあるし、より少ないブロックに組み合わされることもあるし、省略されることもある。
【００３３】
いくつかの実施形態において、方法５００は、図６のコンピューティングデバイス６００等のシステム又はデバイスにより実行され得る。例えば、コンピューティングデバイス６００のプロセッサ６１０（図６参照）が、方法５００のブロックのうちの１つ以上のブロックにより表される機能及び動作を実行するための、メモリ６３０に記憶されているコンピュータ命令を実行するよう構成され得る。
【００３４】
方法５００は、ブロック５０２において開始し得る。ブロック５０２において、状態が、初期化され、現在状態として設定され得、方法５００は、ブロック５０４に進み得る。ブロック５０４において、現在状態についての有効にされているイベント集合が判別され得、方法５００は、ブロック５０６に進み得る。ブロック５０６において、イベント（例えば、イベントｅ）が、ランダムに選択されて実行され得、方法５００は、ブロック５０８に進み得る。例えば、このイベントは、記号実行によって実行され得る。
【００３５】
ブロック５０８において、パス制約とイベントとのペア（例えば、＜ｐｃ１，ｅ＞，＜ｐｃ２，ｅ＞，．．．）に基づく新たな状態の集合（例えば、＜Ｓ１，Ｓ２，．．．＞）が生成され得、方法５００は、ブロック５１０に進み得る。例えば、新たな状態の集合は、ブロック５０６におけるイベントの実行に応じて生成され得る。
【００３６】
ブロック５１０において、記号環境において、この集合における各状態が、反復処理され得、永続集合及び訪問済み集合が、（例えば、記号動的半順序簡約を用いて）更新され得、読み取り−書き込み独立関係にある、パス制約とイベントとのペア（例えば、＜ｐｃ１，ｅ＞，＜ｐｃ２，ｅ＞等）が破棄され得、方法５００は、ブロック５１２に進み得る。例えば、永続集合及び訪問済み集合は、次のプロセスに基づいて更新され得る。永続集合は、イベント系列において既に実行されているイベント群を比較することにより更新され得る。したがって、永続集合を更新する関数は、初期トレースとしての又はリプレイ（replay）からのトレースτを受け取った後に、トレースτに対して作用することができる。しかしながら、永続集合は、最後の実行のみからではなく、あるポイントに至るまで探索された全ての実行から、漸増的に構築され得ることに留意されたい。
【００３７】
このプロセスは、トレースτにおける各イベントτｉにわたって反復し、τｉのプレフィックスτｐについて永続集合を更新することができる。このプロセスは、イベントτｉと競合するイベントから、永続集合Ｔ（τｐ）を構築することができる。イベントτｉは、無効にされるイベントにより引き起こされる競合と、非可換なイベントにより引き起こされる競合と、である２つの種類の競合についてチェックすることにより、拡張され得る（extended）。
【００３８】
一実施形態において、イベントｅは、イベントτｉにより無効にされ得、したがって、イベントｅは、イベントτｉの前に探索されなければならない。別の実施形態において、２つのイベントτｉ及びτｊが、τｉの後のイベントを適切な系列λ及び系列μに並び替えることにより隣り合わせにされて競合し得るような、線形化（linearization）が存在し得る。イベントτｉ及びイベントτｊが隣り合うそのような線形化の存在を判定することは、τｉ  −＞  τｋ且つτｋ  −＞  τｊである、ｉとｊとの間のｋが存在しないことを判定することにより達成され得る。直感的には、これらは、２つの競合するイベントτｉ及びτｊの順序が逆にされることを許容し得る要件である。λが空の系列である場合、競合は、イベントτｉがτｐにおいて有効にされ、したがって、イベントτｊが永続集合に追加され得ることを示し得る。λが空でなく、λ１  −＞  ττｊである場合、λ１が永続集合に追加され得る。なぜならば、これは、イベントτｊがイベントτｉの前に実行され得る状態へのステップを行うからである。
【００３９】
ブロック５１２において、有効にされているイベント集合のイベント系列の境界に到達したかどうかが判定され得る。イベント系列の境界に到達したと判定された場合、方法５００は、ブロック５１６に進み得る。イベント系列の境界に到達していないと判定された場合、方法５００は、ブロック５１４に進み得る。
【００４０】
ブロック５１４において、イベント集合からの状態が、ランダムに選択され、現在状態として設定され得、方法５００は、ブロック５０４に戻り得る。
【００４１】
ブロック５１６において、初期イベント系列τが形成され得、方法５００は、ブロック５１８に進み得る。
【００４２】
ブロック５１８において、（例えば、バックトラッキングによって）未探索のイベントが見出されたかどうかが判定され得る。より詳細には、例えば、（例えば、バックトラッキングによって）第１の未探索のイベントが見出され得る。未探索のイベントが見出されなかったと判定された場合、方法５００は、終了し得る。未探索のイベントが見出されたと判定された場合、方法５００は、ブロック５２０に進み得る。
【００４３】
ブロック５２０において、ブロック５１４又はブロック５３０において見出されたイベントｂが実行され得、方法５００は、ブロック５２２に進み得る。例えば、このイベントは、記号実行によって実行され得る。
【００４４】
ブロック５２２において、パス制約とイベントとのペア（例えば、＜ｐｃ１，ｂ＞，＜ｐｃ２，ｂ＞，．．．）に基づく新たな状態の集合（例えば、＜Ｓ１，Ｓ２，．．．＞）が生成され得、方法５００は、ブロック５２４に進み得る。例えば、新たな状態の集合は、ブロック５２０におけるイベントｂの実行に応じて生成され得る。
【００４５】
ブロック５２４において、記号環境において、イベント集合における各状態が、反復処理され得、永続集合及び訪問済み集合が、（例えば、記号動的半順序簡約を用いて）更新され得、読み取り−書き込み独立関係にある、パス制約とイベントとのペア（例えば、＜ｐｃ１，ｂ＞，＜ｐｃ２，ｂ＞等）が破棄され得、方法５００は、ブロック５２６に進み得る。例えば、永続集合及び訪問済み集合は、ブロック５１０に関連して上述したプロセスに基づいて更新され得る。
【００４６】
ブロック５２６において、有効にされているイベント集合のイベント系列の境界に到達したかどうかが判定され得る。イベント系列の境界に到達した場合、方法５００は、ブロック５１８に戻り得る。イベント系列の境界に到達していない場合、方法５００は、ブロック５２８に進み得る。
【００４７】
ブロック５２８において、イベント集合からの状態が、ランダムに選択され、現在状態として設定され得、方法５００は、ブロック５３０に進み得る。
【００４８】
ブロック５３０において、有効にされているイベント集合が見出され得、イベントがランダムに選択され得、方法５００は、ブロック５２０に戻り得る。
【００４９】
本開示の範囲から逸脱することなく、方法５００に対して、変更、追加、又は省略が可能である。例えば、方法５００の動作は、異なる順序で実行されることもある。さらに、説明された動作及びアクションは、例として提供されているに過ぎず、これらの動作及びアクションのうちの一部は、開示された実施形態の本質を損なうことなく、任意的であることもあるし、より少ない動作及びアクションに組み合わされることもあるし、追加の動作及びアクションに拡張されることもある。
【００５０】
図６は、本開示の少なくとも１つの実施形態に従った例示的なコンピューティングデバイス６００のブロック図である。コンピューティングデバイス６００は、デスクトップコンピュータ、ラップトップコンピュータ、サーバコンピュータ、タブレットコンピュータ、組み込みコンピュータ、携帯電話機、スマートフォン、携帯情報端末（ＰＤＡ）、電子書籍リーダ、ネットワークスイッチ、ネットワークルータ、ネットワークハブ、他のネットワーキングデバイス、又は他の適切なコンピューティングデバイスを含み得る。
【００５１】
コンピューティングデバイス６００は、プロセッサ６１０、記憶デバイス６２０、メモリ６３０、及び通信デバイス６４０を含み得る。プロセッサ６１０、記憶デバイス６２０、メモリ６３０、及び／又は通信デバイス６４０は全て、これらのコンポーネントの各々が他のコンポーネントと通信できるように、通信可能に接続され得る。コンピューティングデバイス６００は、本開示に記載の動作のうちのいずれも実行することができる。
【００５２】
一般に、プロセッサ６１０は、様々なコンピュータハードウェア又はソフトウェアモジュールを含む、任意の適切な専用又は汎用のコンピュータ、コンピューティングエンティティ、又は処理デバイスを含み得、任意の適用可能なコンピュータ読み取り可能な記憶媒体に記憶されている命令を実行するよう構成され得る。例えば、プロセッサ６１０は、プログラム命令を解釈及び／又は実行し、且つ／又はデータを処理するよう構成されている、マイクロプロセッサ、マイクロコントローラ、デジタル信号プロセッサ（ＤＳＰ）、特定用途向け集積回路（ＡＳＩＣ）、フィールドプログラマブルゲートアレイ（ＦＰＧＡ）、又は、任意の他のデジタル回路若しくはアナログ回路を含み得る。図６において、プロセッサ６１０は、１つのプロセッサとして示されているが、プロセッサ６１０は、本開示に記載の任意の数の動作を個々に又は集合的に実行するよう構成されている任意の数のプロセッサを含み得る。
【００５３】
いくつかの実施形態において、プロセッサ６１０は、記憶デバイス６２０、メモリ６３０、又は記憶デバイス６２０とメモリ６３０との両方に記憶されているプログラム命令を解釈及び／又は実行し、且つ／又は、記憶デバイス６２０、メモリ６３０、又は記憶デバイス６２０とメモリ６３０との両方に記憶されているデータを処理することができる。いくつかの実施形態において、プロセッサ６１０は、記憶デバイス６２０からプログラム命令をフェッチして、プログラム命令をメモリ６３０にロードすることができる。プログラム命令が、メモリ６３０にロードされた後、プロセッサ６１０は、プログラム命令を実行することができる。
【００５４】
例えば、いくつかの実施形態において、イベント駆動型アプリケーションの解析のための処理動作のうちの１つ以上の処理動作は、プログラム命令として、データストレージ６２０に含められ得る。プロセッサ６１０は、処理動作のうちの１つ以上の処理動作のプログラム命令をフェッチして、１つ以上の処理動作のプログラム命令をメモリ６３０にロードすることができる。１つ以上の処理動作のプログラム命令が、メモリ６３０にロードされた後、プロセッサ６１０は、プログラム命令を実行することができ、その結果、コンピューティングデバイス６００は、プログラム命令により指示される処理動作に関連付けられた動作を実行することができる。
【００５５】
記憶デバイス６２０及びメモリ６３０は、コンピュータ実行可能な命令又はデータ構造を運ぶ又は記憶するコンピュータ読み取り可能な記憶媒体を含み得る。このようなコンピュータ読み取り可能な記憶媒体は、プロセッサ６１０等の汎用又は専用のコンピュータによりアクセスされ得る任意の利用可能な媒体を含み得る。限定ではなく例として、このようなコンピュータ読み取り可能な記憶媒体は、コンピュータ実行可能な命令の形態の所望のプログラムコード又はデータ構造を運ぶ又は記憶するために使用され得るものであって汎用又は専用のコンピュータによりアクセスされ得る、ＲＡＭ、ＲＯＭ、ＥＥＰＲＯＭ、ＣＤ−ＲＯＭ若しくは他の光ディスクストレージ、磁気ディスクストレージ若しくは他の磁気記憶デバイス、フラッシュメモリデバイス（例えば、ソリッドステートメモリデバイス）、又は、任意の他の記憶媒体を含む有形の又は非一時的なコンピュータ読み取り可能な記憶媒体を含み得る。上記の組合せも、コンピュータ読み取り可能な記憶媒体の範囲に含まれ得る。コンピュータ実行可能な命令は、例えば、プロセッサ６１０に所定の動作又は動作群を実行させるよう構成されている命令及びデータを含み得る。
【００５６】
いくつかの実施形態において、記憶デバイス６２０及び／又はメモリ６３０は、イベント駆動型アプリケーション解析に関連付けられたデータを記憶することができる。
【００５７】
通信デバイス６４０は、コンピューティングデバイス６００と別のデバイスとの間の通信を可能にする又は円滑にするよう構成されている、任意のデバイス、システム、コンポーネント、又はコンポーネントの集合を含み得る。例えば、通信デバイス６４０は、モデム、ネットワークカード（無線用又は有線用）、赤外線通信デバイス、光通信デバイス、無線通信デバイス（アンテナ等）、及び／若しくはチップセット（Ｂｌｕｅｔｏｏｔｈ（登録商標）デバイス、８０２．６デバイス（例えば、メトロポリタンエリアネットワーク（ＭＡＮ）用）、Ｗｉ−Ｆｉ（登録商標）デバイス、ＷｉＭＡＸ（登録商標）デバイス、セルラ通信設備等）、並びに／又は同様のデバイスを含み得るが、これらに限定されるものではない。通信デバイス６４０は、少しの例を挙げると、セルラネットワーク、Ｗｉ−Ｆｉ（登録商標）ネットワーク、ＭＡＮ、光ネットワーク等といった任意のネットワーク、及び／又は、リモートデバイスを含む、本開示に記載の任意の他のデバイスと、データが交換されることを可能にし得る。
【００５８】
いくつかの実施形態において、通信デバイス６４０は、ネットワーク内の通信を提供することができる。通信デバイス６４０は、１つ以上のインタフェースを含み得る。いくつかの実施形態において、通信デバイス６４０は、単一の物理コンポーネント上の複数の論理的特徴、例えば、単一の物理ケーブル又は光信号にわたる複数のインタフェースを含み得る。
【００５９】
本開示の範囲から逸脱することなく、図６に対して、変更、追加、又は省略が可能である。例えば、コンピューティングデバイス６００は、図示され本開示に記載の要素より多い又は少ない要素を含んでもよい。例えば、コンピューティングデバイス６００は、タブレット又は携帯電話機のスクリーン等の一体化された表示デバイスを含んでもよいし、コンピューティングデバイス６００から分離されコンピューティングデバイス６００に通信可能に接続され得る、外部モニタ、プロジェクタ、テレビジョン、又は他の適切な表示デバイスを含んでもよい。
【００６０】
本開示において使用される場合、「モジュール」又は「コンポーネント」という用語は、モジュール又はコンポーネントのアクションを実行するよう構成されている特定のハードウェア実装、及び／又は、コンピューティングシステムの汎用ハードウェア（例えば、コンピュータ読み取り可能な媒体等）に記憶され得る且つ／又はコンピューティングシステムの汎用ハードウェア（例えば、処理デバイス等）により実行され得るソフトウェアオブジェクト又はソフトウェアルーチンを指し得る。いくつかの実施形態において、本開示に記載の異なるコンポーネント、モジュール、エンジン、及びサービスは、コンピューティングシステム上で実行されるオブジェクト又はプロセスとして（例えば、別個のスレッドとして）実装され得る。本開示に記載のシステム及び方法のうちの一部は、（汎用ハードウェアに記憶される且つ／又は汎用ハードウェアにより実行される）ソフトウェアにより実装されるとして一般に説明されるが、特定のハードウェア実装又はソフトウェアと特定のハードウェア実装との組合せも可能であり企図されている。本開示において、「コンピューティングエンティティ」は、本開示において前に定義された任意のコンピューティングシステム、又は、コンピューティングシステム上で動作する任意のモジュール又はモジュールの組合せであり得る。
【００６１】
本開示及び特に請求項（例えば、請求項の本体部分）において使用される用語は、一般に、「オープンな」用語であるとして意図される（例えば、「〜を備える」という用語は、「〜を備えるが、〜に限定されるものではない」として解釈されるべきであり、「〜を有する」という用語は、「少なくとも〜を有する」として解釈されるべきであり、「〜を含む」という用語は、「〜を含むが、〜に限定されるものではない」として解釈されるべきである、等）。
【００６２】
本明細書において使用される場合、複数形の「データ（data）」という用語は、単数形の「データ（datum）」も含み得る（例えば、可算名詞）。別の言い方をすると、例えば、本明細書において使用される「データ（data）」という用語は、可算名詞又は不可算名詞を含み得る。
【００６３】
さらに、導入される請求項記載事項の特定の数が意図される場合、そのような意図は、当該請求項中に明示的に記載され、そのような記載がない場合、そのような意図は存在しない。例えば、理解の助けとして、請求項中に、請求項記載事項を導入するための「少なくとも１つの」及び「１つ以上の」といった導入句の使用が含まれることがある。しかしながら、このような導入句の使用は、「a」又は「an」といった不定冠詞による請求項記載事項の導入が、同一の請求項中に「１つ以上の」又は「少なくとも１つの」といった導入句と「a」又は「an」といった不定冠詞とが含まれるとしても、当該導入された請求項記載事項を含む特定の請求項が、当該請求項記載事項を１つしか含まない実施形態に限定されることを意味するとして解釈されるべきではない（例えば、「a」及び／又は「an」は、「少なくとも１つの」又は「１つ以上の」を意味するとして解釈されるべきである）。請求項記載事項を導入するために使用される定冠詞の使用についても同じことが当てはまる。
【００６４】
さらに、導入される請求項記載事項の特定の数が明示的に記載されている場合であっても、そのような記載は、少なくとも記載されている数を意味するとして解釈されるべきであることが、当業者には認識されよう（例えば、他の修飾語のない「２つの記載事項」という単なる記載は、少なくとも２つの記載事項又は２つ以上の記載事項を意味する）。さらに、「Ａ、Ｂ、及びＣ等のうちの少なくとも１つ」又は「Ａ、Ｂ、及びＣ等のうちの１つ以上」に類する表記が使用される場合、一般に、そのような構造は、Ａのみ、Ｂのみ、Ｃのみ、Ａ及びＢの両方、Ａ及びＣの両方、Ｂ及びＣの両方、又は、Ａ、Ｂ、及びＣの全て、等を含むことが意図される。
【００６５】
さらに、２つ以上の選択可能な用語を表すいかなる離接語又は離接句も、明細書、特許請求の範囲、又は図面のいずれであろうと、それら用語のうちの１つ、それらの用語の組合せ、又は、それらの用語の全てを含む可能性を意図するとして理解されるべきである。例えば、「Ａ又はＢ」という句は、「Ａ」若しくは「Ｂ」又は「Ａ及びＢ」の可能性を含むとして理解されるべきである。
【００６６】
本開示において記載された全ての例及び条件付き言語は、当該技術を促進させるために本発明者によって寄与されるコンセプト及び本発明を読者が理解するのを助ける教育上の目的のために意図され、そのような具体的に記載された例及び条件に限定されるものではないとして解釈されるべきである。本開示の実施形態が詳細に説明されたが、それら実施形態に対する様々な変形、置換、及び変更が、本開示の主旨及び範囲から逸脱することなく可能である。
【００６７】
以上の実施形態に関し、さらに以下の付記を開示する。
【００６８】
（付記１）
１つ以上のプロセッサを有するデバイスであって、前記１つ以上のプロセッサは、
記号環境において、有効にされているイベント集合のうちのイベントを実行し、
記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新し、
読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄する
よう構成されている、デバイス。
【００６９】
（付記２）
前記１つ以上のプロセッサは、記号実行のために前記イベントをランダムに選択するようさらに構成されている、付記１に記載のデバイス。
【００７０】
（付記３）
前記１つ以上のプロセッサは、前記有効にされているイベント集合のイベント系列の境界に到達したかどうかを判定するようさらに構成されている、付記１に記載のデバイス。
【００７１】
（付記４）
前記１つ以上のプロセッサは、前記有効にされているイベント集合の前記境界に到達した場合、初期イベント系列を生成するようさらに構成されている、付記３に記載のデバイス。
【００７２】
（付記５）
前記１つ以上のプロセッサは、前記イベント系列における未探索のイベントを識別するようさらに構成されている、付記４に記載のデバイス。
【００７３】
（付記６）
前記１つ以上のプロセッサは、記号実行によって前記未探索のイベントを実行するようさらに構成されている、付記５に記載のデバイス。
【００７４】
（付記７）
前記１つ以上のプロセッサは、前記有効にされているイベント集合における各状態を反復処理して、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの前記永続集合及び前記訪問済みイベントを更新するようさらに構成されている、付記１に記載のデバイス。
【００７５】
（付記８）
複数の動作を実行するための又は前記複数の動作の実行を制御するための、処理デバイスにより実行可能なコンピュータ命令を記憶している非一時的なコンピュータ読み取り可能な媒体であって、前記複数の動作は、
記号環境において、有効にされているイベント集合のうちのイベントを実行する動作と、
記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新する動作と、
読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄する動作と、
を含む、コンピュータ読み取り可能な媒体。
【００７６】
（付記９）
前記複数の動作は、記号実行のために前記イベントをランダムに選択する動作をさらに含む、付記８に記載のコンピュータ読み取り可能な媒体。
【００７７】
（付記１０）
前記複数の動作は、前記有効にされているイベント集合の境界に到達したかどうかを判定する動作をさらに含む、付記８に記載のコンピュータ読み取り可能な媒体。
【００７８】
（付記１１）
前記複数の動作は、前記有効にされているイベント集合の前記境界に到達した場合、イベント系列を生成する動作をさらに含む、付記１０に記載のコンピュータ読み取り可能な媒体。
【００７９】
（付記１２）
前記複数の動作は、前記イベント系列における未探索のイベントを識別する動作をさらに含む、付記１１に記載のコンピュータ読み取り可能な媒体。
【００８０】
（付記１３）
前記複数の動作は、記号実行によって前記未探索のイベントを実行する動作をさらに含む、付記１２に記載のコンピュータ読み取り可能な媒体。
【００８１】
（付記１４）
前記複数の動作は、前記有効にされているイベント集合における各状態を反復処理して、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの前記永続集合及び前記訪問済みイベントを更新する動作をさらに含む、付記８に記載のコンピュータ読み取り可能な媒体。
【００８２】
（付記１５）
イベント駆動型アプリケーションを解析する方法であって、
記号環境において、有効にされているイベント集合のうちのイベントを実行するステップと、
記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの永続集合及び訪問済みイベントを更新するステップと、
読み取り−書き込み独立関係にある、パス制約とイベントとの各ペアを破棄するステップと、
を含む、方法。
【００８３】
（付記１６）
前記有効にされているイベント集合における各状態を反復処理して、記号動的半順序簡約を用いて、前記有効にされているイベント集合のうちの前記永続集合及び前記訪問済みイベントを更新するステップをさらに含む、付記１５に記載の方法。
【００８４】
（付記１７）
前記有効にされているイベント集合のイベント系列の境界に到達したかどうかを判定するステップをさらに含む、付記１５に記載の方法。
【００８５】
（付記１８）
前記有効にされているイベント集合の前記境界に到達した場合、初期イベント系列を生成するステップをさらに含む、付記１７に記載の方法。
【００８６】
（付記１９）
前記イベント系列における未探索のイベントを識別するステップをさらに含む、付記１８に記載の方法。
【００８７】
（付記２０）
記号実行によって前記未探索のイベントを実行するステップをさらに含む、付記１９に記載の方法。
【符号の説明】
【００８８】
６１０  プロセッサ
６２０  記憶デバイス
６３０  メモリ
６４０  通信デバイス
【図１Ａ】
2018026116.tif 000003
【図１Ｂ】
2018026116.tif 000004
【図２Ａ】
2018026116.tif 000005
【図２Ｂ】
2018026116.tif 000006
【図３】
2018026116.tif 000007
【図４】
2018026116.tif 000008
【図５Ａ】
2018026116.tif 000009
【図５Ｂ】
2018026116.tif 000010
【図６】
2018026116.tif 000011