(57)【要約】本発明は、モデル検査で用いられるソフトウェアコードのモデルプログラム解析に関する。最初に、遷移システム（ステップ２２）およびデータの拡張マークアップ言語（ＸＭＬ）（ステップ２４）が生成される。次に、（マークアップ）クエリ言語を用いてデータのＸＭＬ表現をクエリることによって遷移システムのラベル（ステップ２６）が生成される。遷移システムのラベルおよび構造は、次いで、ソフトウェアコードを解析するモデル検査技術に対する入力値として使用される（ステップ２８）。本発明の利点は、遷移システムをラベルする問題が、ＸＭＬドメインに変換できるので、ソフトウェアコードに関する詳細な情報が、周知なＸＭＬドメインで実行可能な形式のクエリを用いて抽出可能なことである。同時に、ＸＭＬドメインへの変換は、効率的なモデル検査技術の使用を妨げない。【選択図】図１
2010504572.tif 000002
【特許請求の範囲】
【請求項１】
データのモデル検査で用いられる遷移システムを生成する方法において、
前記データから前記遷移システムを生成するステップと、
前記データの拡張マークアップ言語（ＸＭＬ）表現を生成するステップと、
クエリ言語を用いて、データのＸＭＬ表現をクエリすることによって前記遷移システム用のラベルを生成するステップと、
前記データを解析するために、モデル検査技術への入力値として、前記遷移システムの前記ラベルおよび前記構造を使用するステップと、
を具えることを特徴とする方法。
【請求項２】
前記データがソースコードであることを特徴とする請求項１に記載の方法。
【請求項３】
前記モデル検査技術が、基礎的なソースコードの静的解析を含むことを特徴とする請求項２に記載の方法。
【請求項４】
前記ソースコードの静的解析が、
前記ソースコードのソフトウェアバグの類があるか、または、ないか識別するステップと、
前記ソースコードのセキュリティ脆弱性を発見するステップと、
前記ソースコードのメトリクスを決定するステップと、および／または、
前記ソースコードのタイミング解析を実行するステップと、
を具えることを特徴とする請求項３に記載の方法。
【請求項５】
前記方法が、前記ソースコードが記載されるとき、または、コンパイル時に実行されることを特徴とする請求項２乃至４のいずれか一項に記載の方法。
【請求項６】
前記クエリするステップが、前記データのＸＭＬ表現のクエリを実行することによって行われ、前記クエリが、前記データの静的特性を検査することを特徴とする請求項１乃至５のいずれか一項に記載の方法。
【請求項７】
前記方法が、前記ソースコードの抽象構文木表現を生成する開始ステップを更に具え、前記遷移システムを生成するステップおよび前記データのＸＭＬ表現を生成するステップが、前記データの抽象構文木表現に基づいていることを特徴とする請求項２乃至６のいずれか一項に記載の方法。
【請求項８】
クエリするステップが、前記データの前記基礎的な抽象構文木表現のツリーパターンを識別するクエリを用いて行われることを特徴とする請求項７に記載の方法。
【請求項９】
クエリするステップが、前記データのＸＭＬ表現に関するクエリを実行することによって行われ、前記クエリが、前記データのＸＭＬ表現で提供される前記クエリにマッチするノードの識別子を返すことを特徴とする請求項１乃至８のいずれか一項に記載の方法。
【請求項１０】
前記ラベルを生成するステップが、前記データのＸＭＬ表現での前記クエリに適合したノードに対応するノードを、前記遷移システムにおいて、ラベルするステップを含むことを特徴とする請求項９に記載の方法。
【請求項１１】
前記遷移システムにおいてラベルされるべき前記ノードは、前記データのＸＭＬ表現の同一ノード識別子によって識別されることを特徴とする請求項１０に記載の方法。
【請求項１２】
前記ノードが、前記データの前記抽象構文木表現の同一識別子によっても識別されることを特徴とする請求項１及び７に記載の方法。
【請求項１３】
前記遷移システムを生成するステップおよび前記データの前記ＸＭＬ表現を生成するステップが、少なくとも部分的に同時に行われることを特徴とする請求項１乃至１２のいずれか一項に記載の方法。
【請求項１４】
クエリするステップが、前記データの前記ＸＭＬ表現に関するクエリを実行させることで行われ、前記方法が、所定のクエリセットから前記クエリを選択するステップを更に含むことを特徴とする請求項１乃至１３のいずれか一項に記載の方法。
【請求項１５】
クエリするステップが、前記データのＸＭＬ表現に関するクエリを実行することによって行われ、前記クエリがユーザによって生成されることを特徴とする請求項１乃至１４のいずれか一項に記載の方法。
【請求項１６】
前記遷移システムが、コントロールフローグラフ、データフローグラフまたは情報フローグラフであることを特徴とする請求項１乃至１５のいずれか一項に記載の方法。
【請求項１７】
前記クエリ言語がＸＭＬパス言語（ＸＰａｔｈ）であることを特徴とする請求項１乃至１６のいずれか一項に記載の方法。
【請求項１８】
前記データのＸＭＬ表現を生成するステップが、クエリを実行可能にするために必要となる前記ＸＭＬ表現の前記データ構造を生成するステップのみを具えることを特徴とする請求項１乃至１７のいずれか一項に記載の方法。
【請求項１９】
請求項１乃至１８のいずれか一項に記載の方法に従って動作するように、コンピュータシステムを制御する、前記コンピュータシステムにインストールされたソフトウェア。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、データのモデル検査で用いられる遷移システムの生成に関する。特に、限定するものではないが、データはソフトウェアコードでもよく、静的プログラム解析など、モデル検査はプログラム解析の一部を形成してもよい。本発明は、本発明の方法を実行するためにコンピュータシステムにインストールされたソフトウェアに関する。
【背景技術】
【０００２】
ソフトウェア製品の開発は、市場投入までの開発期間の短縮および開発費用の低減の２つの目的によって非常に駆り立てられる。しかしながら、現在の最も優れたソフトウェア開発の実施は、依然として、費用が高く、時間を消費し、製品開発の後期または製品開発後にも、不必要な費用が生じる。
【０００３】
理由の１つは、ソフトウェアバグなどの、ソフトウェアのソースコードのエラーまたは欠陥であり、この２つを検出するのには費用と時間がかかる。従って、このようなソフトウェアのバグを発見するとき、あるいは、結果として欠陥がないことを保証することは、ソフトウェア開発において極めて重要である。
【０００４】
コンサルティング会社のｓｔａｋｅ社（現在はＳｙｍａｎｔｅｃが取得）によってなされたリサーチ［ＡＳ］は、例えば、バグに関するセキュリティを解決するのに、実施フェーズよりも検査フェーズ中の方が約２倍となり、開発後、１０倍もの費用がかかる。これは、顧客の信用の損失または責任（ｌｉａｂｉｌｉｔｉｙ）の発生などの間接的なコストを含んでいない。
【０００５】
動的テストは、プログラム解析の１つの手法である。入力値のセットが付与されると、テストすべきソフトウェアが実行され、その動作（ｂｅｈａｖｉｏｕｒ）が観察される。特に、出力（すなわち、プログラムを実行した結果）は、規定されたものと比較される。動的テストはほとんどコードの機能修正に関する。動的テストは、「このプログラムは、入力値の平方根を計算するか？」または「このプログラムはアルファベット順に従業員のリストをリターンするか？」などの質問に答えを提供する。通常、テストは、網羅的である。このことは、可能性の全てのシナリオをテストする方法があることを意味しているのではない。さらに、適切なテストを作成することは面倒であり、これらのテストを実行するのには時間を消費する。
【０００６】
静的解析は、その名称が示すように、プログラムを解析する静的な手法である。これは、所定のコードフラグメントが得られるときのみ、コンパイル時またはコンパイル前であっても行うことができる。静的解析は、コードを「みる（ｌｏｏｋｉｎｇ）」高度な方法として記載されており、コードを試験し、その動作を予測することができる。巧みな方法でコード構造を観察することによってのみ、多くの特性を検査することができる（例えば、「宣言した変数の全ては、プログラムが最初に変数を使用する時点に到達するまでに、初期化されているか？」、「プログラミングガイドラインは尊重されているか？」、「ポインタなどの所定のプログラミング構造は安全に処理されるか？」）。
【０００７】
静的解析によって解決される問題の種類は、通常、動的テストによって解決されるものとは異なる。しかしながら、多くの静的特性は、動的特性に直接的な影響を与える。例えば、ポインタの誤操作によって、機能的な必要条件を妨害するプログラムクラッシュとなる可能性がある。さらに、静的な解析は、通常、網羅的である（特性妨害（バグ）が見つからなかった場合、バグは生じないことを保証する）。
【０００８】
静的解析の問題は、モデル検査の問題として記載されていることが理論的に示されている［ＳＳ９８］。モデル検査は、所定の特性に関して非常に効率のよい方法で広域で有限なステートスペース（ｓｔａｔｅ  ｓｐａｃｅ）を検索することができる技術である。通常、ステートスペースは、遷移システム（すなわち、ラベルで注釈を付けられたグラフ）として表現され、これらの特性は、これらのラベルに関する時相論理式で示される。静的解析問題をモデル検査問題に変換することは、２つの利点がある。第１に、モデル検査問題を効率的に解決する入手可能なフリーツールがあり、第２に、多くの静的解析問題は、時相論理式として自然な方法で示される。
【０００９】
図１１に描写されているラベル付（注釈付）コントロールフローグラフ（ＣＦＧ）を検討する。ＣＦＧは、プログラムの（制御）構造を示し、ループコード、分岐コードまたは直線コードの位置についての情報を保持する。ＣＦＧは、通常、「より深い」情報（例えば、変数ｉが宣言されるまたは変数ｉが使用されるなど）を保持していない。この注釈は、例えば、ｉが宣言されるか、または使用される全ての位置に加えられるラベルである。
【００１０】
静的解析／モデル検査特性は、「変数ｉが宣言される場合、変数ｉは将来どこかで使用されなければならない」であってもよい。この特性は、時相論理の自然言語表現であり、以下のように、より形式的な表記に見られ：
ＡＧ（ｉ＿ｄｅｃｌａｒｅｄ  →  ＥＦ ｉ＿ｕｓｅｄ）
ＡＧは（非形式的に）「常に」およびＥＦ「未来の将来どこかで」を意味する。ラベルｉ＿ｄｅｃｌａｒｅｄ、および、ｉ＿ｕｓｅｄは、これらが真を表す（ｔｒｕｅ）ところのプログラムに結合される。このようなラベルで注釈されたＣＦＧ（遷移システムである）が与えられると、モデル検査は、上記のように自動的に式を検査することができる。
【００１１】
ドキュメント、作用、材料、装置、物品、または、本明細書に含まれるものなどに関する議論は、本発明の内容を示すことを目的とするのみである。これらのいずれか、または、全てが、本願の各請求項の優先日よりも前に存在していたとして、先行技術の基礎の一部を形成するか、本発明の属する分野において一般的な周知な知識であると、認めることはできない。
【発明の概要】
【００１２】
本発明は、データのモデル検査で用いられる遷移システムを生成する方法に関し、この方法は、
データから遷移システムを生成するステップと、
データの拡張マークアップ言語（ＸＭＬ）表現を生成するステップと、
（マークアップ）クエリ言語を使用して、データのＸＭＬ表現をクエリするステップによって、遷移システム用のラベルを生成するステップと、
データを解析するためにモデル検査技術に対する入力値として遷移システムのラベルおよび構造を使用するステップと、
を具える。
【００１３】
本発明の利点は、遷移システムにラベルを付す問題をＸＭＬドメインに変換可能であるので、周知なＸＭＬドメインで実行可能なフォーマット形式のクエリを用いて、データに関する詳細な情報を抽出可能であることである。同時に、ＳＭＬドメインへの変換は、効率的なモデル検査技術を使用することを妨げない。
【００１４】
データは、ソースコードでもよい。ソースコードの静的解析は、
ソースコードにソフトウェアバグの類があるか、または、ないことを特定し、
ソースコードのセキュリティ面の脆弱性を発見し、
ソースコードのメトリクス（ｍｅｔｒｉｃｓ）を決定し、および／または、
ソースコードのタイミング解析をすることができる。
【００１５】
この方法は、ソースコードが書かれているとき、または、コンパイル中に実行可能である。
【００１６】
データのＸＭＬ表現をクエリするステップが、データのＸＭＬ表現のクエリを実行するステップを具え、前記クエリが、例えば、変数および機能宣言の位置、変数と数値の比較、変数またはデータ構造の初期化、変数またはデータ構造の修正、および、変数、データ構造、関数または数値などの各種プログラムエレメントの使用など、ソースコードの静的特性を検査することができる。他の静的特性は、関数呼び出し（一般的な関数、または、例えばメモリ管理を扱う特定の関数）および制御構文（例えば、ｉｆ、ｓｗｉｔｃｈ、ｒｅｔｕｒｎ、または、全てのループ構文）を具える。
【００１７】
本発明の方法は、抽象構文木（ａｂｓｔｒａｃｔ  ｓｙｎｔａｘ  ｔｒｅｅ）を生成する開始ステップと、遷移システムを生成するステップと、を具え、データのＸＭＬ表現を生成するステップは、データの抽象構文木表現に基づいていてもよい。
【００１８】
クエリは、データに関する時相論理を規定できる。クエリは、データの基礎的な抽象構文木表現のツリーパターンを特定することができる。
【００１９】
クエリは、当該クエリにマッチするノードの識別子を返すことができる。ラベルを生成するステップは、クエリがマッチしたノードに対応するノードに、遷移システムにおいて、ラベルを付けるステップを具える。この遷移システム中のノードは、ＸＭＬ表現および遷移システム中の同一のノード識別子によって識別可能である。ノードは、抽象構文木中の同一識別子によって識別できる。
【００２０】
本発明の方法のステップは、並行して実行可能である。
【００２１】
クエリは、ライブラリなど、所定のクエリセットからユーザが選択したクエリであってもよい。代替としてはまたは付加的に、クエリは、ユーザによって生成されてもよい。クエリは、ソフトウェアユーザインターフェースを用いて、選択されるか、または、生成可能である。
【００２２】
遷移システムは、コントロールフローグラフでもよい。代替としては、遷移システムは、データフローグラフまたは情報フローグラフでもよい。
【００２３】
クエリ言語は、ＸＰａｔｈでもよい。モデル検査技術に使用されるラベルを生成するために、クエリ言語としてＸＰａｔｈを用いた本発明の実施例の利点は、
１．ＸＰａｔｈは、強力なクエリ言語であるので、複雑な指定が可能となり、複雑な特性を検査することができる。例えば、プログラム解析において、クエリはループカウンタが修正されるループを発見可能であり、または、関連した表現の実行順序が未定義で、未定義な結果または望ましくない結果となる構文（ｓｔａｔｅｍｅｎｔ）を発見できる。この実施例は、簡便な拡張可能性および柔軟性があるので、開発者は解決法を自身の要求に適応することができる。
２．ＸＰａｔｈ言語は、Ｗ３Ｃ勧告を用いた受容された標準規格である。予め入手可能な効率的でフリーの（ＬＧＰＬ）ＸＰａｔｈの実現方法もある。これは、本発明が、ゼロからの設計を必要とする方法と比較して、使用するのに訓練を多く必要としないという利点がある。
３．この実施例は、ソースコードの完全自動解析に関連している。これは、アプリケーションが、ユーザの背景知識を必要とせず、解析目的でコードを改装（ｒｅｆｉｔ）またはモデリングする必要はないことを意味する。さらに、特性の仕様（必要条件）が付与されると、通常、解析はテストよりも早く、コンパイル時間とほとんど同じオーダであり、テストケースジェネレーションなどを必要としない。本発明は、静的プログラム解析用技術の一部を解決する。
【００２４】
データを表すＸＭＬを生成するステップは、ＸＭＬ表現のデータ構造を生成するステップのみを具え、前記データ構造でクエリを実行できる。
【００２５】
さらなる側面において、本発明は、コンピュータシステムを制御するために、コンピュータシステムにインストールされたソフトウェアを具え、上述した発明に従って処理できる。
【図面の簡単な説明】
【００２６】
図１１は、小さな例示的プログラムの周知なラベル付コントロールフローグラフである。ここで、本発明の例は、以下の図面に関して記載される。
【図１】図１は、本発明の方法のフローチャートである。
【図２】図２は、サンプルプログラムのソースコードを示す。
【図３】図３は、図２のサンプルプログラムの抽象構文木である。
【図４】図４は、図２のサンプルプログラムと同様のプログラムのコントロールフローグラフ（ＣＦＧ）である。
【図５】図５は、図２のサンプルプログラムの単純化された拡張マークアップ言語（ＸＭＬ）表現である。
【図６】図６は、図４のＣＦＧにラベルを付けるために、図５のＸＭＬ表現に適用可能な２つの仮の（ｐｓｅｕｄｏ）クエリを示す。
【図７】図７は、ラベル付ＣＦＧを示す。
【図８】図８は、サンプルソースコードのＸＭＬ表現のさらなる例である。
【図９】図９は、図８のＸＭＬ表現に適用可能なＸＰａｔｈクエリである。
【図１０】図１０は、コードの一般的な構造および特性入力モデル変換を図示する。
【図１１】図１１は、小さな例示的プログラムの周知なラベル付コントロールフローグラフである。
【発明を実施するための形態】
【００２７】
モデル検査を使用して、ソースコード中のソフトウェアの静的なバグを検出する本発明を使用する例は、図１のフローチャートに記載される。このフローチャートは、連続ステップのフローとして記載されているが、実際には、いくつかのステップを並行して実行出来ることを私達は指摘する。例えば、図１のステップ２２およびステップ２４は並行して実行出来る。
【００２８】
図２に示されるサンプルプログラムのソースコードを検討する。このサンプルプログラムは、図３に示される抽象構文木（ＡＳＴ）に自動的に変換される（ステップ２０）。ＡＳＴはラベル付ツリーであり、ノードはプログラムオペレータによってラベル付けされ、リーフノードは、そのオペランド（すなわち、変数又は定数）を示す。ＡＳＴは、プログラムを構文解析する（すなわち読み込む）ときに生成される中間構造であり、コントロールフローグラフ（ＣＦＧ）の自然な先行モデル（ｐｒｅｃｕｒｓｏｒ）である。ＡＳＴ中の全てのノードは、ノードＩＤ（図示せず）と呼ばれる固有の識別子を有する。
【００２９】
次に、私達は、図４に示されるように、ＣＦＧを自動的に生成する（ステップ２２）。このＡＳＴの例においては、ＡＳＴの情報は、ノードＩＤを含むＣＦＧ形式に翻訳される。この目的は、ＣＦＧをラベル付（注釈）して、私達は、オリジナルのソースコードのソフトウェアのバグを検出するために、モデル検査技術を適用することができる。これを行うのに、私達は、図５に示されるように、ＡＳＴからＸＭＬドキュメントを生成する（ステップ２４）。ＸＭＬドキュメント（図５）はＡＳＴの直接翻訳である。このように、ＸＭＬドキュメントは、図２のＡＳＴとして全く同一の情報を有する。再び、これはノードＩＤを具えている。このＸＭＬドキュメントにおいて、ノードＩＤは、用語「ｉｄ」を含むマーカーによってフラグをたてられる。
【００３０】
次に、私達は、ＣＦＧにラベルを付す（ステップ２６）ので、私達はモデル検査技術を適用することができる。私達は、時相論理を用いてソースコードのＸＭＬドキュメントバージョンをクエリすることによって、ＣＦＧの位置を識別する。パターンマッチングは、より大きな構造（我々の場合においてはＡＳＴ）の所定のパターン（我々の場合においてはツリー構造）の存在を検査する動作である。ツリー構造は非常に強力で、複雑なパターンを定義することができる。この方法は、抽象構文木のパターンマッチングプログラムコンストラクトに基づいている。
【００３１】
本発明の中心部分は、ツリーパターンマッチングアルゴリズムと、異なるドメインすなわちＸＭＬドキュメントプロセシングからのクエリ言語と、を使用することである。この実施例においては、我々のラベルを識別するクエリ言語としてＸＰａｔｈを使用する。ＸＰａｔｈ（ＸＭＬ  Ｐａｔｈ  Ｌａｎｇｕａｇｅ）は、ＸＭＬドキュメントの一部をアドレスし、非常に簡便な方法でツリーパターンを指定できる簡潔な（非ＸＭＬ）構文である。フリーに入手できる（ＬＧＰＬ）使用可能な効率的な実現方法（ｉｍｐｌｅｍｅｎｔａｔｉｏｎ）もある。
【００３２】
図６は、ツリーパターンを識別するソースコードのＸＭＬ表現に適用できる２つの仮の（ｐｓｅｕｄｏ）クエリを示す。第１のクエリは、変数「ｆ」が定義されるインスタンスに位置する。ＸＰａｔｈ構文での上記クエリの表現は、以下のように表すことができる：
／／Ｄｅｃｌ／Ｖａｒ［＠ｎａｍｅ＝’ｆ］
【００３３】
第２のクエリは、コード中に変数「ｆ」が使用される位置を発見する。ＸＰａｔｈ構文中の図５のコードに適合する上記クエリの簡略化したバージョンの表現は、以下のように（簡略化して）リード（ｒｅａｄ）される：
／／Ｃｏｍｐａｒｅ／／ｃｏｍｐａｒｅ／＊［＠ｎａｍｅ＝’ｆ］]｜／／Ａｓｓｉｇｎ／Ｏｐ２／＊［＠ｎａｍｅ＝’ｆ］
【００３４】
クエリはノードＩＤを返し、ここで、このノードＩＤは、ＣＦＧ中の対応するノードＩＤと直接対応している。各々のクエリは、当該クエリがマッチするＸＭＬドキュメントに含まれるノードＩＤを返す。ＣＦＧの対応する位置は、次いで、ＣＦＧ中の同一ＩＤを有するノードを見つけることによって容易に識別される。さらに、このノードは、クエリに対応する適宜なラベルが付与される。得られるラベル付ＣＦＧは図７に示される。
【００３５】
ここで、ＣＦＧがラベルされるので、周知のモデル検査技術がＣＦＧに適用され（ステップ２８）、ソフトウェアバグの識別子など、プログラム解析を実行することができる。
【００３６】
さらに実施例を記載する。図８においては、私達は、ＡＳＴの一部のＸＭＬ表現をみることできる。変数ｉが宣言されているノードを見つける（マッチする）ための各々のＸＰａｔｈクエリは、図９に示されるように構成される。
【００３７】
ここで、上記ＸＰａｔｈクエリは、ＣＦＧ中のどのノードがｉ＿ｄｅｃｌａｒｅｄでラベルされるか規定する。図８において、ＸＭＬフラグメントに適用されるとき、ｃｆｇｉｄ「３３」を有するノード＜Ｄｅｃｌ＞がラベルされ、ｃｆｇｉｄ「４７」のノードはラベルされない。従って、上記識別子「３３」およびラベルを有するＣＦＧ中のノードは、対応している。
【００３８】
上述のように、特性セットが付与されたソースコードを注釈付モデルに変換することは、多数のステージで行われる（ステップ２０〜２８）。ソースコードを構文解析（ｐａｒｓｅ）することで、ＣＦＧを構築するための前提条件であるＡＳＴを得る。この静的解析特性は、構文解析ツリーのＸＭＬ表現のＸＰａｔｈクエリを用いてどのノードを注釈しなければならいかを決定する原子命題を規定する。ＡＳＴのＸＭＬ表現およびクエリは、共に、ＸＰａｔｈエンジンによって使用され、どの状態でどの原子命題が有効であるか決定する。ＣＦＧ構造と共にこの情報は、モデル検査入力値の構成単位（ｂｕｉｌｄｉｎｇ  ｂｌｏｃｋ）である。
【００３９】
コードの一般的構造および本発明を用いた特性入力値モデル変換は、図１０に示される。
【００４０】
この方法を最適化するのに、ＡＳＴを表すＸＭＬドキュメントを生成する必要はないが、代替としては、クエリを実行するのに使用されるＸＰａｔｈライブラリによって直接使用可能である対応するデータ構造を構築する。この最適化に伴って、全ＸＭＬドキュメントは、１つのステップで生成される必要はないが、次のステップにおいて、ＸＰａｔｈライブラリは、これらのファイルを再度、構文解析しなければならない。ＸＰａｔｈ構造に直接進むことによって、オーバーヘッドをセーブする。この調節（ｍｏｄｉｆｉｃａｔｉｏｎ）は、ＡＳＴとＸＰａｔｈとの間の灰色のリンクとして図１０に記載されている。
【００４１】
本発明はソフトウェアとして提供できる。ソフトウェアがコンピュータシステムにインストールされる場合、このコンピュータシステムを操作して、上記方法を実行可能である。このコンピュータは、モニタなどの出力デバイスを具え、ユーザにユーザインターフェースを提供する。インターフェースを用いて、ユーザはユーザ自身のＸＰａｔｈクエリを実行し、ユーザ自身の特性（クエリ）を構築できる。コンピュータシステムは、クエリライブラリを保存するための保存手段を具えることができる。この方法の一部は、ユーザがソースコードを書いているときに実行することができる。代替としては、この方法はコンパイル中に実行してもよい。
【００４２】
本発明は、ＯＣａｍｌ用のＦｒｉｓｃｈのＸＰａｔｈライブラリなど、クエリライブラリを使用して、対象となるパターンに関するインターナルＸＭＬデータ構造をクエリすることできる。ＸＭＬおよびＸＰａｔｈは両方とも、十分に標準化された言語である。このような標準化言語を用いることで、本発明は、ＯＣａｍｌに統合されるソフトウェアライブラリを使用し、ＸＭＬデータのＸＰａｔｈクエリを実行するインターフェースを提供できる。
【００４３】
本発明は、ＣおよびＣ＋＋を含むソースコードのプログラミング言語の範囲に適用できる。Ｊａｖａ（登録商標）などのＣおよびＣ＋＋と同様な他の命令型プログラミング言語の他に、この技術は、アセンブル言語プログラムにも適応することができる。アセンブル言語の場合、クエリは、低レベルアセンブリプログラム由来の縮重ＡＳＴではそれほど強力ではない。
【００４４】
定量的モデル検査は、最適な動作（ｂｅｈａｖｉｏｕｒ）の確認と関連している。原子命題を有するステートを注釈するのではなく、このモデルは、ステートおよび遷移に重点をおいて注釈される。このドキュメントに記載される技術は、定量的モデル検査に重点をおくのにも使用可能である。
【００４５】
本発明を使用してバグをテストする場合、本発明は、なぜバグが発生し、どのようにバグが修正できるかを説明するために使用することができる。例えば、詳細な説明は、エラーを強調表示するだけでなく、エラーとなる潜在的な実行パスを含むその位置を指摘することができる。これは、ソフトウェア開発の生産性を向上させようとするユーザにとって有益な支援となる。
【００４６】
広義に記載される本発明の意図または範囲から逸脱せずに、特定の実施例に示されるように、多数の変形および／または修正が本発明になされることを当業者であれば理解されたい。例えば、図１に示されるステップのいくつかは、示されているように連続的ではなく、並行して実行出来る。
【００４７】
例えば、プログラム解析の部分として、本発明の方法は、プログラムの欠陥、セキュリティの脆弱性、一般的なプログラム解析（すなわち、プログラムに関するコンピュータメトリクス）およびタイミング解析（すなわち、プログラムの最悪な場合の実行または最適化に関するステートメントの生成）を発見するために使用することができる。
【００４８】
従って、本実施例は、例示を目的とするものであって、限定を意味するものではない。
【００４９】
参考文献
[ＡＰＭＶ０４] 
G. Antoniol, M. Di Penta, G. Masone, and U. Villano. Compiler Hacking for Source Code Analysis. Software Quality Journal, 12:383-406, 2004.
[ＡＳ] 
Calculating the Total Cost of Development. http://wp.bitpipe.com/resource/org l 039183786_34/CTCD_WP_0902_bρ x.pdf.
[Ｆｒｉ００]
Alain Frisch. XPath Library for OCaml. http://www.eleves.ens.fr/home/frisch/soft.htmWxpath, 2000. 
［ＳＳ９８］
D. Schmidt and B. Steffen. Program Analysis as Model Checking of Abstract Interpretations. In Proc. of Static Analysis Symposium (SAS'98), Pisa, Italy, 1998. 
【図１】
2010504572.tif 000003
【図２】
2010504572.tif 000004
【図３】
2010504572.tif 000005
【図４】
2010504572.tif 000006
【図５】
2010504572.tif 000007
【図６】
2010504572.tif 000008
【図７】
2010504572.tif 000009
【図８】
2010504572.tif 000010
【図９】
2010504572.tif 000011
【図１０】
2010504572.tif 000012
【図１１】
2010504572.tif 000013
【国際調査報告】
2010504572.tif 000014
2010504572.tif 000015