(57)【要約】有限な反復を有することが可能なソフトウェアを、基本ブロックを有するブーリアン表現に好都合に翻訳し、かつ、ＳＡＴベースのモデル検査をブーリアン表現に適用する、ソフトウェア・プログラムの形式的検証のための、システムおよび方法が開示される。
2007528059.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェア・プログラムの検証方法であって、
有限な反復を有することがある前記ソフトウェア・プログラムを、各基本ブロックが前記ソフトウェア・プログラム内の一連の１つまたは複数の命令を１組の並列な割当ておよび他の基本ブロックへの１組の遷移として表す複数の基本ブロックを含むブーリアン表現としてモデル化することと、
前記ソフトウェア・プログラムの前記ブーリアン表現にＳＡＴベースのモデル・チェッカーを適用することと
を含むソフトウェア・プログラムの検証方法。
【請求項２】
前記モデル・チェッカーは、有限モデル検査を使用するバックエンドＳＡＴソルバーである、請求項１に記載の方法。
【請求項３】
前記モデル・チェッカーは、前記基本ブロックの反復アンローリングによって進行し、各アンローリングは前記ソフトウェア・プログラムのブロック毎の実行である、請求項１に記載の方法。
【請求項４】
各基本ブロックはラベルを有し、プログラム・カウンタ変数が、前記モデル・チェッカーによる処理の間に前記ソフトウェア・プログラムの許容された実行の進行を追跡するために使用される、請求項３に記載の方法。
【請求項５】
前記プログラム・カウンタ変数は、前記モデル・チェッカーがまず前記ソフトウェア・プログラム内の制御流れに焦点を絞るように、前記モデル・チェッカーが適用されるときに増加したスコアを与えられる、請求項４に記載の方法。
【請求項６】
前記選択ビットによって識別された前記ソフトウェア・プログラム内の前記制御流れの一部に前記モデル・チェッカーが焦点を絞ることを可能にするように、各基本ブロックは前記プログラム・カウンタ変数にもとづく値に設定された選択ビットを割当てられる、請求項４記載の方法。
【請求項７】
前記モデル・チェッカーが適用される時に制約条件が加えられ、前記制約条件は前記モデル・チェッカーの、直接先行基本ブロックと後続基本ブロックの不可能な組み合わせの探索スペースを削減する、請求項４に記載の方法。
【請求項８】
前記制約条件は、前記ブーリアン表現内の前記基本ブロックのサブセットにのみ適用される、請求項７に記載の方法。
【請求項９】
前記ソフトウェア・プログラムは、前記ソフトウェア・プログラム内の有限な反復を処理するために、有限なスタックを使用してさらにモデル化される、請求項１に記載の方法。
【請求項１０】
前記ソフトウェア・プログラムが、前記ブーリアン表現が、抽象された変数とそれらの具体的な表現の中に残された変数の両方を含むように、前記モデル化の間に部分的に抽象される、請求項１に記載の方法。
【請求項１１】
前記ソフトウェア・プログラムの前記ブーリアン表現内の遷移関係は、ＳＡＴベースの列挙を使用して列挙される、請求項１に記載の方法。
【請求項１２】
前記ソフトウェア・プログラムの前記ブーリアン表現内の遷移関係は、次式
【数１】
2007528059.tif 000289
によって列挙され、表される、請求項１１に記載の方法。
【請求項１３】
前記ソフトウェア・プログラムの前記ブーリアン表現内の遷移関係は、次式
【数２】
2007528059.tif 000290
によって列挙され、表される、請求項１１に記載の方法。
【請求項１４】
前記ソフトウェア・プログラムの前記ブーリアン表現内の遷移関係における共通の計算は、計算を加速するために再利用される、請求項１に記載の方法。
【請求項１５】
前記ソフトウェア・プログラムの前記ブーリアン表現内の変数の大きさを制限するために、前記ソフトウェア・プログラムのモデル化より前に、範囲分析が実行される、請求項１に記載の方法。
【請求項１６】
前記ソフトウェア・プログラムを関連する要素に分解するために、前記ソフトウェア・プログラムのモデル化より前に、プログラム・スライシングが実行される、請求項１に記載の方法。
【請求項１７】
近似抽象モデル化が利用され、かつ、前記モデル・チェッカーが反例を生成すれば、前記反例が擬似的であるか否かが検査される、請求項１に記載の方法。
【請求項１８】
前記反例の検査は、副経路のテスト可能性をさらに含む、請求項１７記載の方法。
【請求項１９】
前記反例が擬似的であれば、前記モデル・チェッカーによって計算された非満足化可能性コアを使用して、改善が行われる、請求項１７に記載の方法。
【請求項２０】
有限な反復を有することがある、分析されるソフトウェア・プログラムを受信する入力モジュールと、
前記ソフトウェア・プログラムをブーリアン表現に翻訳するモデリング・モジュールであって、前記ブーリアン表現は複数の基本ブロックを有し、各基本ブロックは前記ソフトウェア・プログラム内の一連の命令を１組の並列な割当ておよび他の基本ブロックに対する１組の遷移として表す、モデル化・モジュールと、
前記ソフトウェア・プログラムの前記ブーリアン表現を受信し、処理する、ＳＡＴベースのモデル・チェッカーと
を有するソフトウェア検証システム。
【請求項２１】
前記モデル・チェッカーは、有限モデル検査を使用するバックエンドＳＡＴソルバーである、請求項２０に記載のシステム。
【請求項２２】
前記モデル・チェッカーは、前記基本ブロックの反復アンローリングによって前記ソフトウェア・プログラムの前記ブーリアン表現を処理し、各アンローリングは前記ソフトウェア・プログラムのブロック毎の実行である、請求項２０に記載のシステム。
【請求項２３】
各基本ブロックはラベルを有し、前記モデル・チェッカーによる処理の間に前記ソフトウェア・プログラムの許容された実行の進行を追跡するために、プログラム・カウンタ変数が使用される、請求項２２に記載のシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本願は、２００４年１月２２日に出願された、「ソフトウェアのモデリング、抽象、および分析のためのシステムおよび方法」と題する、米国仮特許出願番号第６０／５３８，５２４号の利益を主張し、その内容は参照によって本明細書に含まれる。
【０００２】
本願は、２００２年５月３０日に出願された、「有限モデル検査の効率的な処理法」と題する、米国ユーチィリティ特許出願番号第１０／１５７，４８６号に関し、その内容は参照によって本明細書に含まれる。
【０００３】
本発明は、ソフトウェアの形式的分析と検証のための技術に関する。
【背景技術】
【０００４】
モデル検査は、コンカレントシステムの検証のための自動的な技術である。モデル検査は、シミュレーション、試験、および演繹的推論に対していくつかの利点を有し、複雑な順序回路の設計および通信プロトコルを検査するために実際にうまく使用されている。E.M Clarke、0. Grumberg、および D.A. Peledの「モデル検査」、MIT Press、2000、を参照されたい。特に、モデル検査は自動的であり、設計に誤りがあれば、モデル検査はシステムの有効なデバッグに使用可能な反例（すなわち、システムの問題のある動作の証拠）を生成する。二分決定グラフ（ＢＤＤ）を使用する記号モデル検査は大きな状態空間を完全にカバする可能性を有するが、多くの場合実際には十分評価できない。別の方法として、有限長（bounded length）の反例の検索にのみ焦点を合わせた有限モデル検査（ＢＭＣ）がある。A. Biere、A. Cimatti、E.M Clarke、M. Fujita、および Y. Zhuの「ＢＤＤの代わりにＳＡＴ手順を使用する記号モデル検査」（Symbolic model checking using SAT procedures instead of BDDs）、Proc.of the 36th ACM/IEEE Design Automation Conference、pp. 317-20(1999)、を参照されたい。長さｋの反例が存在する場合にのみブーリアン数式が満足し得るように、この問題は事実上ブーリアン数式に変換される。実際には、反例が１つでも存在すれば、最も短い反例が得られるように、ｋは１からスタートしてインクリメントできる。しかし、反例が存在しない場合には、検証の完全性を保証するために、さらなる推論が必要である。ＢＭＣ法での満足化可能性のチェックは、バックエンドＳＡＴソルバーとして公知のものによって通常実行される。たとえば、M.K. Ganai、L. Zhang、P. Ashar、および A. Gupta、「高性能ＳＡＴソルバーのための回路ベースおよびＣＮＦベース・アルゴリズムの強度の結合」(Combining strength of circuit-based and CNF-based algorithms for a high performance SAT solver)、Design Automation Conference、 2002と、E. Goldberg および Y. Novikovの「Ｂｅｒｋｍｉｎ：高速かつロバストなＳＡＴソルバー」（Berkim: A fast and robust SAT solver）、Design Automation and Test in Europe、pages 132-39、2002と、J.P. Marques-Silva および K.A. Sakallah「ＧＲＡＳＰ：前置詞的満足化可能性のための探索アルゴリズム」（GRASP: A search algorithm for prepositional satisfiability）、 IEEE Transactions on Computers、48:506-21,1999と、M. Moskewicz、C. Madigan、Y. Zhao、L. Zhang、他 S. Malik「Ｃｈａｆｆ：能率的ＳＡＴソルバーの設計」（Chaff: Engineering an efficient SAT solver）,Design Automation Conference、2001、を参照されたい。
【０００５】
最近、有限モデル検査技術をＣプログラムのようなソフトウェアの形式的検証に適用することが提案されている。E. Clarke、D. Kroening、「ＡＮＳＩ−Ｃプログラムを参照として使用するハードウェア検証」（Hardware Verification using ANSI-C Programs as a Reference）、Proceedings of ASP-DAC 2003、pp. 308-11 (January 2003)、を参照されたい。この方法では、Ｃプログラムは、モノリシックなＳＡＴ公式、すなわち、ビット・ベクトル式に変換され、次に、このビット・ベクトル式は、Ｃプログラムがレジスタ・トランスファー・レベル（ＲＴＬ）のハードウェア設計と等価であることのチェックを含む、一貫性をチェックするために、ＳＡＴベースの有限モデル検査と共に使用される。Ｃプログラムの各個別のステートメントは、プログラムの最小構成要素であると考えられる。残念ながら、このステートメントをベースにした方法は、ループや関数の簡潔な処理の点で限界を有し、モデル検査における最近の進歩を完全には活用していない。
【発明の開示】
【課題を解決するための手段】
【０００６】
１つまたは複数の基本ブロックにもとづいてソフトウェア・プログラムをブーリアン表現に好都合に翻訳する、ソフトウェアのための検証システムと方法が開示される。ソフトウェア・プログラムの最小構成要素として個別のステートメントを扱うのではなく、各基本ブロックが、ソフトウェア・プログラム内の一連の命令を、１組の並列な割当ておよび他の基本ブロックに対する１組の遷移として表すことができる。次に、有限モデル検査を使用するバックエンドＳＡＴソルバーのような、モデル・チェッカーが、ブーリアン表現に適用できる。モデル・チェッカーは、基本ブロックを反復してアンローリング（unrolling）することによって進行し、各アンローリングはソフトウェア・プログラムのブロック毎の実行における１つの段階であると理解される。システムの状態は、現在のアクティブな基本ブロックと範囲内のすべての変数の評価を示す位置を含むように、定義することができる。したがって、各基本ブロック、ならびに、モデル検査の間にソフトウェア・プログラムの許容された実行の進行を追跡するために、導入されたプログラム・カウンタ変数に対してラベルを生成できる。モデル・チェッカーによる基本ブロックの各アンローリングは、好都合にも限定された数の後続点（successors）を有している。各アンローリングはソフトウェア・プログラム全体にモデル・チェッカーの満足化可能性（satisfiability）の問題をもたらすが、ソフトウェア・プログラムの制御流れを考慮することによって、新しいアンローリング内の多くの基本ブロックが到達不能であると宣言できる。したがって、検証の効率をさらに上げるために、モデル生成プロセスの知識を、モデル・チェッカーによって使用された決定ヒューリスティックス（decision heuristics）に組み入れることが可能である。
【０００７】
ソフトウェア・プログラムは、抽象されたデータ変数および現実のデータ変数の両方を好都合にも含む方法で抽出できる。これは、正確さと分析の容易さとの間のシームレスなトレードオフを可能にし、少数の抽象化改善反復（abstraction-refinement iterations）を使用しての正確な分析を場合によっては可能にする。ソフトウェアの分析のために述語抽出を使用することは、記号述語抽出を使用する基本ブロック間の遷移関係の計算と、近似的遷移関係の使用によって改良することが可能である。該２つの方法の組み合わせ、ならびに、ソフトウェア・プログラム全体の中で見出される多くの遷移関係を、計算を適切にスケジューリングしおよび一部の結果を記憶することによってさらに効率的に計算するヒューリスティックスを含めることは、遷移関係を計算するさらに効率的な方法となる。
【０００８】
コードの簡略化は、プログラムのセマンティクスに影響を与えない方法で自動的に適用できる。範囲分析は、ソフトウェア・プログラムのブーリアン表現内の変数の大きさを制限するために、モデル化より前に実行可能である。プログラムのスライシングは、要素が必ずしも原文の通り（textual）連続していない意味論的に意味のある成分にソフトウェア・プログラムを分解するために実行することができる。
【０００９】
擬似的な（spurious）遷移、フラグメント(fragments)および全経路にもとづく改善分析（refinement analysis）は、抽象改良反復ループの間に学習したクローズを継続して維持することによって、効率的に使用でき、反例によって導かれた抽象化改善フレームワーク（counter-example-guided abstraction refinement framework）のより効率的な実現を約束する。
【００１０】
ここに開示された検証システムおよび方法は、高速でさらに効率的な動作を備え、従来技術よりも広範囲のソフトウェア・アプリケーションに適用できる。本発明の以上のまたは他の利点は、下記の詳細説明と添付図面を参照することによって当業者には明白であろう。
【発明を実施するための最良の形態】
【００１１】
図１は、本発明の一実施形態による検証システムの動作を説明する抽象図である。本システムへの入力は、ソフトウェア・プログラム１０１と、チェックされるプロパティの表現１０５である。本システムの出力は、ソフトウェア・プログラム１０１が１９１においてプロパティを満たすことを証明するか、あるいは、１９２においてプロパティの誤りを立証する反例を提供するか（あるいは、分析は、タイム・アウトまたはメモリの使い果たしのようなリソース制約条件による明確な結果なしに終了することがある）、のいずれかの結果である。
【００１２】
分析されるソフトウェア・プログラム１０１は、Ｃプログラム言語のような、プログラム言語で書かれた１つのソース・コード・ファイルまたは１連のソース・コード・ファイルとして入力できる。本発明を有限な繰返し（bounded recursion）を可能にするＣプログラム言語のサブセットを特に参照して説明するが、本発明は、Ｃに制限されるものではなく、当業者によって他のプログラム言語に容易に拡張することが可能である。チェックされるプロパティ表現１０５は種々のソースから得ることができ、多数の異なる方法で指定することが可能である。たとえば、限定するものではないが、チェックすべき有利なプロパティは到達可能性（reachability）、すなわち、ソース・コードの特定の部分が到達可能か否かである。プロパティを指定するための有利なメカニズムは、ソース・コードを、プロパティ・モニタ１０５を含むように修正すること、すなわち、システムのための選択されたプロパティをモニタするコードの小部分を修正することによる。たとえば、到達可能性プロパティが関係している場合には、プロパティ・モニタ１０５は、到達可能性を分
析されるソース・コードの行における、「ＥＲＲＯＲ＿ＬＡＢＥＬ」のようなラベルによって与えることが可能である。プロパティ・モニタ１０５を組み立てる方法は、たとえば、スクリプトを使用することによって、容易に自動化できる。図１では、限定するものではないが、チェックされるプロパティは到達可能性プロパティであると仮定している。
【００１３】
本システムは、以下に詳細に説明する静的解析１１０、モデル化段階１２０、および抽象化段階１３０の形式で、ソフトウェア・プログラムの自動化された分析を実行する。結果は、１５０において、バックエンド・モデル・チェッカーによって分析できるブーリアン表現へのプログラムの翻訳である。
【００１４】
本発明による１つの態様の実施形態によれば、ソフトウェア・プログラム１０１は、システムによって１つまたは複数の「基本ブロック」に変換される。従来技術で行われるように、個々のステートメントをソフトウェア・プログラムの最小構成要素として扱わないで、ソフトウェアの各基本ブロックは、ソフトウェア・プログラムからの一連の連続した命令を含むことができる。基本ブロックは、一連の（多分空の）割当て（assignment）を表すことができ、他の基本ブロックに先行する保護された一連の（多分空の）（条件付きの）遷移がこれに続く。連続した割当てを単一の基本ブロックに寄せ集めることによって、これらの命令を一連の並列割当てに書き換えることができる。これは、このような割当てが基本ブロック内の以前の命令として現れるならば、たとえば、基本ブロック内の命令の割当ての左側に現れるいくつかの変数を、該命令が同じ基本ブロックに以前に割り当てられている表現式に置換することによって、行うことが可能である。本システムの状態は、有利なことに、現在のアクティブな基本ブロックと有効範囲内のすべての変数の評価を示す位置を含むように定めることができる。有限長スタック（処理ごとに）は、関数呼出しスタックをモデル化するために、広域変数の集合に加えることができ、このことは有限な繰返しのモデル化を可能にする。
【００１５】
図１の１５０にける、ソフトウェア・プログラムのブーリアン表現のモデル検査は、ソフトウェア・プログラムの個々のステートメントではなく、基本ブロックをアンローリング（unrolling）することによって進行する。ラベルを各基本ブロックに対して生成可能であり、複数の基本ブロックで構成される状態遷移グラフの進展をモニタするために、プログラム・カウンタ変数を導入することができる。プログラム・カウンタ変数は、モデル検査の間、ソフトウェア・プログラムの許容された実行の進行を追跡するために使用することができる。モデル検査の間のアンローリングは、ソフトウェア・プログラムのブロック毎の実行における１つの段階であると理解される。これは、有限モデル検査の前後関係において、各基本ブロックに対して、限られた数の考えられる後続点(successors)のみが存在するので、ソフトウェア・プログラムを処理する効率的な方法である。単一の初期のブロック・ラベルが所与のもとすると、新しいアンローリングには、限られた数の到達可能な考えられる次のブロックのみが存在する。各アンローリングはソフトウェア・プログラム全体に満足化可能性の問題を引き起こすが、ソフトウェア・プログラムの制御フローを考慮するだけで、新しいアンローリング内の多くのブロックを到達不能であると名言することができる。したがって、探索スペースをかなり削ることができる。
【００１６】
さらに、図１の１５０におけるモデル検査は、モデル生成プロセスの情報を決定ヒューリスティックスに組み込む方法で進行することができる。プログラム・カウンタ変数は、新しいアンローリングにおいて多くの到達不可能な基本ブロックを除くために、モデル・チェッカーによって使用でき、その結果モデル・チェッカーがプログラム・カウンタ変数にもとづいて決定することができる可能性を増大させる。
【００１７】
上述のように、図１は、モデル・チェッカー１５０によってチェックされたプロパティが到達可能性プロパティであると仮定している。モデル・チェッカー１５０が、ソフトウェア・プログラム１０１の指定されたセクションが抽象化されたブーリアン表現では到達できないと証明すれば、そのセクションはソフトウェア・プログラム１０１の元のソース・コード内では到達できないことが保証され、したがって、検証手順は図１の１９１において終了する。モデル・チェッカー１５０が反例を発見すれば、１６０において、反例が擬似的であるか否かのチェックが行われる。１６０における反例の分析が、経路がオリジナルのソフトウェア・プログラムにおいて実際に実行可能であると判定すれば、具体的な反例が発見され、それによって検証手順は図１の１９２において終了する。そうでない場合、ブーリアン表現は、モデル・チェッカー１５０に対する新しい表現を得るために１７０において改善される。
【００１８】
本発明はどのような特定のモデル検査アーキテクチャーに限定されないが、有限な検証と有限でない検証を共に実行するＳＡＴベースおよびＢＤＤベースの高度な方法を利用するブーリアン検証フレームワークを使用するのが有利である。このようなシステムの例は、２００２年５月３０日に出願された、「有限モデル検査の効率的な処理法」(EFFICIENT APPROACHES FOR BOUNDED MODEL CHECKING)と題する、米国ユーティリティ特許出願番号第１０／１５７，４８６号と、Aarti Gupta、Malay K. Ganai、Zijiang Yang、および Pranav Ashar の「証明分析と共にＳＡＴベースのＢＭＣを使用する反復抽象化」(Iterative Abstraction using SAT-based BMC with Proof Analysis)(Proceedings of International Conference on Computer-Aided Design (ICCAD)、pp.416-423 (Nov. 2003))に記載されたダイバーシステムであり、その内容は参照によって本明細書に含まれる。
【００１９】
図１を参照して、静的解析１１０、モデル化１２０、および抽象１３０に関連する処理を、以下に詳細に説明する。また、１７０における擬似的な反例と１８０における改善に対する分析の処理を、さらに詳細に以下に説明する。
【００２０】
静的解析      ソフトウェア１０１をさらに処理する前に、いくつかのコード簡略化を行うことが望ましい。たとえば、入れ子にされた、すなわち他の関数呼出しの中に埋め込まれた関数呼出しを、仮の変数を付け加えることによって、取り除くことが有利なことがある。さらに、副次的作用を伴うステートメントを、副次的作用を伴うステートメントを含まない等価なコードに書き直すことが有利なこともある。G.C. Necula、S. McPeak、S.P. Rahul、およびW. Weimerによる「ＣＩＬ：Ｃプログラムの分析と変換のための中間言語およびツール」（CIL: Intermediate language and Tools for Analysis and Transformation of C Programs）、Proceedings of the 11th International Conference on Computer Construction, LNCS, pp. 213-28, Springer-Verlag (2002)、を参照されたい。
【００２１】
図１に表すように、静的解析１１０はソフトウェア上で実行される。１１１において、ソフトウェアの制御流れ図が計算され、ソフトウェアのモデル化のために、後続の処理で使用される。制御流れ図を作る間、すべての変数が、全体的に定義されているとして処理が可能であるように、変数がソフトウェア・プログラム全体に対して固有の名前を有するように、変数に名前を付け直すことが望ましい。分析の目的のために使用できる有限のモデルを保証するために、たとえば再帰的なデータ構造の長さの限界を指定することによって、再帰的なデータ構造を平坦化する（flatten out）ことがさらに望ましい。
【００２２】
本発明による他の態様によれば、分析フレームワークの一部として、プログラム・スライシング１１２および範囲分析１１３のような前処理を行うことも有利である。１連のプログラム要素に対してプログラムの「スライス」とは、プログラム要素の考慮している集合のメンバーに使用される複数の変数の値に何らかの影響を与えるかもしれないプログラム要素のみを含むプログラムの投射（projection）である。「プログラム・スライシング技術の調査」（A Survey of Program Slicing Techniques）、Journal of Programming Languages、Vol.3, No.3、pp.121-189 (Sept. 1995)、を参照されたい。このように、スライシングは、システムが、原文が必ずしも連続ではない複数の要素から成る、プログラムの意味論的に意味のある分解を見出すことを可能にする。ソフトウェア内のさまざまなステートメントを表すために必要なビットの数を制限するために、範囲分析技術も使用することができる。R. Rugina とM.C.Rinardの「ポインタ、配列インデックス、およびアクセスされたメモリ領域の記号バウンド分析」（Symbolic Bounds Analysis of Pointers）、SIGPLAN Conference on Programming Language Design and Implementation、pp. 182-95(2000)、を参照されたい。
【００２３】
モデル化      図１に示すように、ソフトウェアのモデル化１２０は、２種類の論理、すなわち制御論理１２１およびデータ論理１２２を考慮する。制御論理１２１は、基本ブロックの制御流れ図によって表すことができる制御の流れを記述する。データ論理１２２は、有限の範囲が与えられた変数の割当てを記述する。ソフトウェア・プログラムがＮ個の基本ブロックから成ると仮定すると、各基本ブロックは
【００２４】
【数１】
2007528059.tif 000003
【００２５】
ビットのラベルによって表すことができる。
【００２６】
【数２】
2007528059.tif 000004
【００２７】
ビットのプログラム・カウンタ変数は、基本ブロックのグラフ内の進行をモニタするために、導入することができる。制御論理は、基本ブロック・グラフ、および基本ブロック間の遷移のいくつかを保護する条件が所与として、このプログラム・カウンタ変数の遷移関係を定める。したがって、遷移は、ソフトウェア・プログラムを表す基本ブロック・グラフ内の制御の転送を模している。プログラム・カウンタ変数は、モデル検査段階の間にソフトウェア・プログラムの許容された実行の進行を追跡するために使用することができる。ソース・コードの各基本ブロックは、前述のプログラム・カウンタ変数および基本ブロック・ラベルが所与として、データ変数および制御論理の密にビット・ブラスト（bit-blasted）されたバージョンによって置換できる。
【００２８】
類似のモデル化方法が、（Ｖｅｒｉｓｏｆｔ、Ｊａｖａ（登録商標）パス・ファインダー、Ｂｏｇｏｒなどのような）従来技術のソフトウェア・モデル検査ツールで探求されているが、非有限のモデル検査設定に限定される。ソフトウェア・モデル化はここでは、バックエンド・モデル・チェッカーをカスタマイズすることによって、ソフトウェア検証の効率をさらに改善しつつ、ＳＡＴベースの有限モデル検査の最近の進歩を利用する方法で説明する。
【００２９】
上述したように、各基本ブロックは、他の基本ブロックに通ずる保護された（条件付きの）一連の遷移の（多分空の）を有する割当て（assignment）の一連の（多分空の）集合を含んでいる。基本ブロックは、次のようによって形式上構成することが可能である。プログラム内のすべての変数の集合は
【００３０】
【数３】
2007528059.tif 000005
【００３１】
によって表される。
【００３２】
【数４】
2007528059.tif 000006
【００３３】
内のすべての変数の、型が一致した（type-consistent）の評価は
【００３４】
【数５】
2007528059.tif 000007
【００３５】
によって表され、型が一致する（type-consistent）全ての評価の集合は
【００３６】
【数６】
2007528059.tif 000008
【００３７】
によって表され、許容されるＣ表現の集合はΣによって表される。次に、基本ブ
ロックの並列割当ては、
【００３８】
【数７】
2007528059.tif 000009
【００３９】
として、
【００４０】
【数８】
2007528059.tif 000010
【００４１】
と書くことができる。集合
【００４２】
【数９】
2007528059.tif 000011
【００４３】
は、ブロックの割当て集合と呼ぶことができる。基本ブロック
【００４４】
【数１０】
2007528059.tif 000012
【００４５】
の局所的にアクティブな変数の集合は
【００４６】
【数１１】
2007528059.tif 000013
【００４７】
と表すことができ、型が一致する評価の集合は
【００４８】
【数１２】
2007528059.tif 000014
【００４９】
と表すことができる。関数
【００５０】
【数１３】
2007528059.tif 000015
【００５１】
は、Ｖａｒｓ（σ）を使用するＣ表現σ∈Σ内に現れる変数の集合を表す。集合
【００５２】
【数１４】
2007528059.tif 000016
【００５３】
は、σで言及した変数およびアドレス・デリファレンス（dereference）の、ポインタ、ポインタのポインタ、等に対応する変数を含んでいる。この関数は、
【００５４】
【数１５】
2007528059.tif 000017
【００５５】
と同様に、
【００５６】
【数１６】
2007528059.tif 000018
【００５７】
に当然のことながら一般化される。割当て集合
【００５８】
【数１７】
2007528059.tif 000019
【００５９】
を有する特定のＣブロックに対して、要求された変数
【００６０】
【数１８】
2007528059.tif 000020
【００６１】
の集合は
【００６２】
【数１９】
2007528059.tif 000021
【００６３】
と定義することができ、使用されていない変数
【００６４】
【数２０】
2007528059.tif 000022
【００６５】
の集合は
【００６６】
【数２１】
2007528059.tif 000023
【００６７】
と定義することができる。
【００６８】
この構造において、プログラムの状態は、現在の基本ブロックを記述している位置
【００６９】
【数２２】
2007528059.tif 000024
【００７０】
およびデータ変数
【００７１】
【数２３】
2007528059.tif 000025
【００７２】
の型が一致する評価を含むように定めることができ、ここで、位置
【００７３】
【数２４】
2007528059.tif 000026
【００７４】
における有効範囲外の変数には未定義の値⊥が割当てられる。初期状態の集合は、
【００７５】
【数２５】
2007528059.tif 000027
【００７６】
であり、ここで、プログラムの初期状態は、
【００７７】
【数２６】
2007528059.tif 000028
【００７８】
内の各変数がその仕様と型が一致する値をとることができる単一の位置
【００７９】
【数２７】
2007528059.tif 000029
【００８０】
において完全にランダムであると考えられる。有限長スタック（処理ごとに）は、関数呼出しスタックをモデル化するために、全体の変数の集合に加えることができ、その結果、有限な繰返しのモデル化を可能にする。
【００８１】
制御論理      ソフトウェア・プログラムのための制御流れ図は、有限グラフ
【００８２】
【数２８】
2007528059.tif 000030
【００８３】
であり、ここで、
【００８４】
【数２９】
2007528059.tif 000031
【００８５】
は基本ブロック／位置から成り、
【００８６】
【数３０】
2007528059.tif 000032
【００８７】
は制御の転送を示す基本ブロック同士の間のエッジを表す。最初と最後の命令を除いて、各基本ブロック内の命令は、固有の先行点(predecessor)と後続点(successor)を有する。図２は、
【００８８】
【数３１】
2007528059.tif 000033
【００８９】
等のような、いくつかのプログラミング・ステートメントのための基本ブロックの構造に対する擬似コードを説明している。主な関数ＣＲＥＡＴＥ＿ＢＡＳＩＣ＿ＢＬＫＳは、再帰的である。第１のパラメタ
【００９０】
【数３２】
2007528059.tif 000034
【００９１】
は、現在のステートメントに対するエントリ・ブロックである。第２のパラメタ
【００９２】
【数３３】
2007528059.tif 000035
【００９３】
は現在のステートメントである。
【００９４】
【数３４】
2007528059.tif 000036
【００９５】
はその型に応じて、
【００９６】
【数３５】
2007528059.tif 000037
【００９７】
の一部になったり、ならなかったりする。この関数は、基本ブロックおよび条件の複数の対から成り、かつ、出力エッジを、未だ作成されていない次の基本ブロックに正確に接続するために使用される、
【００９８】
【数３６】
2007528059.tif 000038
【００９９】
と呼ばれる集合を返す。
【０１００】
【数３７】
2007528059.tif 000039
【０１０１】
は、次のステートメントの第１の基本ブロックであると仮定する。すると、任意の
【０１０２】
【数３８】
2007528059.tif 000040
【０１０３】
に対して、
【０１０４】
【数３９】
2007528059.tif 000041
【０１０５】
から条件
【０１０６】
【数４０】
2007528059.tif 000042
【０１０７】
付きの
【０１０８】
【数４１】
2007528059.tif 000043
【０１０９】
への保護された遷移が存在する。以下はシンタックスが図２においてどのように処理されるかを説明している。
【０１１０】
【数４２】
2007528059.tif 000044
【０１１１】
条件
【０１１２】
【数４３】
2007528059.tif 000045
【０１１３】
は、以前のステートメントと条件の間に分岐がないので、エントリ・ブロックと結合する。制御は
【０１１４】
【数４４】
2007528059.tif 000046
【０１１５】
に対して分岐するので、新しい基本ブロック
【０１１６】
【数４５】
2007528059.tif 000047
【０１１７】
をそれぞれ
【０１１８】
【数４６】
2007528059.tif 000048
【０１１９】
に対するエントリ・ブロックであると初期化することが有利である。
【０１２０】
【数４７】
2007528059.tif 000049
【０１２１】
の基本ブロックは、次に再帰的に作られる。条件
【０１２２】
【数４８】
2007528059.tif 000050
【０１２３】
が真であるとするエッジ
【０１２４】
【数４９】
2007528059.tif 000051
【０１２５】
と、条件
【０１２６】
【数５０】
2007528059.tif 000052
【０１２７】
が偽であるとするエッジ
【０１２８】
【数５１】
2007528059.tif 000053
【０１２９】
が存在する。最後に、ｉｆステートメントの出口ブロックは、
【０１３０】
【数５２】
2007528059.tif 000054
【０１３１】
の出口ブロックの和集合である。
【０１３２】
【数５３】
2007528059.tif 000055
【０１３３】
【数５４】
2007528059.tif 000056
【０１３４】
の一部となるｉｆステートメントでの条件と異なり、ｗｈｉｌｅステートメント内の条件
【０１３５】
【数５５】
2007528059.tif 000057
【０１３６】
は、新しいブロック
【０１３７】
【数５６】
2007528059.tif 000058
【０１３８】
を、それが２つ以上の基本ブロックのデスティネーションであるので起動する。制御は
【０１３９】
【数５７】
2007528059.tif 000059
【０１４０】
の後に
【０１４１】
【数５８】
2007528059.tif 000060
【０１４２】
に移ることも移らないこともあるので、新しいエントリ・ブロック
【０１４３】
【数５９】
2007528059.tif 000061
【０１４４】
は初期化され、
【０１４５】
【数６０】
2007528059.tif 000062
【０１４６】
に対する基本ブロックが再帰的に作られる。
【０１４７】
【数６１】
2007528059.tif 000063
【０１４８】
を、
【０１４９】
【数６２】
2007528059.tif 000064
【０１５０】
の
【０１５１】
【数６３】
2007528059.tif 000065
【０１５２】
個の出口ブロックであるとする。無条件のエッジ
【０１５３】
【数６４】
2007528059.tif 000066
【０１５４】
が存在する。新しい基本ブロック
【０１５５】
【数６５】
2007528059.tif 000067
【０１５６】
が初期化され、
【０１５７】
【数６６】
2007528059.tif 000068
【０１５８】
ステートメントの直後のステートメントを含むブロックとなる。条件
【０１５９】
【数６７】
2007528059.tif 000069
【０１６０】
が真であるとする
【０１６１】
【数６８】
2007528059.tif 000070
【０１６２】
および条件
【０１６３】
【数６９】
2007528059.tif 000071
【０１６４】
が偽であるとする
【０１６５】
【数７０】
2007528059.tif 000072
【０１６６】
の２つの条件付きエッジが存在する。
【０１６７】
【数７１】
2007528059.tif 000073
【０１６８】
【数７２】
2007528059.tif 000074
【０１６９】
によって符号を付けられたステートメントが構文解析済みであれば、無条件のエッジ
【０１７０】
【数７３】
2007528059.tif 000075
【０１７１】
が作られ、ここで
【０１７２】
【数７４】
2007528059.tif 000076
【０１７３】
はラベル付きステートメントを含む基本ブロックである。そうでない場合、
【０１７４】
【数７５】
2007528059.tif 000077
【０１７５】
ステートメント、すなわち、
【０１７６】
【数７６】
2007528059.tif 000078
【０１７７】
を含む基本ブロックは、ハッシュ・テーブル
【０１７８】
【数７７】
2007528059.tif 000079
【０１７９】
に蓄積される。ハッシュ・テーブル内のエントリのキーは、
【０１８０】
【数７８】
2007528059.tif 000080
【０１８１】
ステートメントのラベル・ストリングであり、コンテンツは、同じデスティネーションを有する
【０１８２】
【数７９】
2007528059.tif 000081
【０１８３】
ステートメントを含む基本ブロックのリストである。ハッシュ・テーブルは
【０１８４】
【数８０】
2007528059.tif 000082
【０１８５】
ステートメントが構文解析されるときに、エッジを作るために使用される。
【０１８６】
【数８１】
2007528059.tif 000083
【０１８７】
新しい基本ブロック
【０１８８】
【数８２】
2007528059.tif 000084
【０１８９】
は、ラベル付きステートメントに対して初期化される。ラベル付きステートメントが
【０１９０】
【数８３】
2007528059.tif 000085
【０１９１】
ステートメントのデスティネーションであるように、新しいブロックを作ることが望ましく、このことは、２つ以上の基本ブロックのラベル付きステートメントのデスティネーションを作る。基本ブロックは、２つ以上のラベル付きステートメントを含まないことに注意されたい。このステートメントへのデスティネーションを有する
【０１９２】
【数８４】
2007528059.tif 000086
【０１９３】
ステートメントを含むハッシュ・テーブル
【０１９４】
【数８５】
2007528059.tif 000087
【０１９５】
内に基本ブロックが存在すれば、無条件のエッジが
【０１９６】
【数８６】
2007528059.tif 000088
【０１９７】
に対するブロックの各々に対して作られる。
【０１９８】
【数８７】
2007528059.tif 000089
【０１９９】
プログラム・コードの簡略化の後には、２つの型の関数呼出し、すなわち、
【０２００】
【数８８】
2007528059.tif 000090
【０２０１】
のみが存在する。図３は、非再帰的な関数呼出しに対して複数の基本ブロックを生成する擬似コードを述べている。パラメタの受渡しがあれば、基本ブロック
【０２０２】
【数８９】
2007528059.tif 000091
【０２０３】
に対して対応する仮パラメタに実パラメータを割当てるステートメントが加えられる。図３では、値呼び（call-by-value）のみが考慮されていることに注目されたい。呼び出された関数の基本ブロックが呼び出されていなければ、行３において、そのために基本ブロックを作ることができる。
【０２０４】
【数９０】
2007528059.tif 000092
【０２０５】
から
【０２０６】
【数９１】
2007528059.tif 000093
【０２０７】
内の第１の基本ブロックへの無条件のエッジが作られる。関数呼出しが、
【０２０８】
【数９２】
2007528059.tif 000094
【０２０９】
型であれば、
【０２１０】
【数９３】
2007528059.tif 000095
【０２１１】
内のリターン式を
【０２１２】
【数９４】
2007528059.tif 000096
【０２１３】
に割当てることによって、ステートメントを追加することができる。このステートメントは、関数呼び出しステートメントの出口ブロックであるブロック
【０２１４】
【数９５】
2007528059.tif 000097
【０２１５】
に追加される。
【０２１６】
【数９６】
2007528059.tif 000098
【０２１７】
デフォルトによって、割当てのようなステートメントは、新しい基本ブロックを作らない。このような場合には、ステートメントは単にエントリ・ブロックに追加される。
【０２１８】
図４は、基本ブロックを作る処理を例示するサンプルのＣコードを示す。コードは３つの関数から成り、制御流れ情報はコメントで示される。コメントは、現在の基本ブロックと次の基本ブロックのインデックスを示す書式
【０２１９】
【数９７】
2007528059.tif 000099
【０２２０】
内にあり、ここで、
【０２２１】
【数９８】
2007528059.tif 000100
【０２２２】
は現在のステートメントが属する基本ブロックのインデックスである。異なるステートメントは、同じ基本ブロック、たとえば、関数
【０２２３】
【数９９】
2007528059.tif 000101
【０２２４】
内の最初の２つの割当て、に属してもよい。各関数呼出しは、単一のステートメントであるが、２つの基本ブロックに対応することに注目されたい。１つの基本ブロックはパラメタの受渡しを保持し、他の基本ブロックはリターニング・ポジションを保持する。
【０２２５】
【数１００】
2007528059.tif 000102
【０２２６】
は、現在の基本ブロックのデスティネーションのリストである。
【０２２７】
【数１０１】
2007528059.tif 000103
【０２２８】
ステートメントは、２つのデスティネーション基本ブロックを有する。どちらが選択されるかは、条件論理に頼る。各関数における
【０２２９】
【数１０２】
2007528059.tif 000104
【０２３０】
ステートメントは、この関数に対する複数の呼出し位置に対応する複数のデスティネーションを有してもよい。
【０２３１】
図５は、計算された制御流れ図に加えてサンプルのＣコードの別の例を右側に示している。この例も、基本ブロックが、さまざまな型に対してどのように計算されるかを示している。各基本ブロックは、図５において、基本ブロックに隣接する六角形の中に示される
固有の番号によって識別される。制御流れ図のソース・ノードは基本ブロック０であり、シンク・ノードは強調された基本ブロック８である。図５の例は、非再帰的な関数呼出しが呼出し関数の制御流れの中に含まれる方法を図で示している。前処理分析は、関数「ｆｏｏ」が再帰的な方法で呼び出されていないと判定する。２つのリターン点は、変数「ｒｔｒ」を使用して固有のリターン位置を特別なパラメタとして渡す符号化によって、スコアされる。
【０２３２】
制御論理は、
【０２３３】
【数１０３】
2007528059.tif 000105
【０２３４】
ビットを使用して表現することが可能である。ここで
【０２３５】
【数１０４】
2007528059.tif 000106
【０２３６】
はプログラム内の基本ブロックの数である。図６は、制御論理の真理値表を表す。図６において、
【０２３７】
【数１０５】
2007528059.tif 000107
【０２３８】
は現在の状態変数を示し、
【０２３９】
【数１０６】
2007528059.tif 000108
【０２４０】
は次の状態変数を示し、ここで、
【０２４１】
【数１０７】
2007528059.tif 000109
【０２４２】
である。表のｊ番目の行は、条件
【０２４３】
【数１０８】
2007528059.tif 000110
【０２４４】
に関する制御流れ図のエッジ
【０２４５】
【数１０９】
2007528059.tif 000111
【０２４６】
を表し、ここで、
【０２４７】
【数１１０】
2007528059.tif 000112
【０２４８】
は
【０２４９】
【数１１１】
2007528059.tif 000113
【０２５０】
に対する割当てであり、
【０２５１】
【数１１２】
2007528059.tif 000114
【０２５２】
は
【０２５３】
【数１１３】
2007528059.tif 000115
【０２５４】
に対する割当てである。真理値表にもとづいて、次の状態変数の各々に対する次の状態論理を
【０２５５】
【数１１４】
2007528059.tif 000116
【０２５６】
として作ることが可能である。
【０２５７】
【数１１５】
2007528059.tif 000117
【０２５８】
データ論理は次のように作ることができる。簡略化の後の変数のすべては、有限のドメインを有する。
【０２５９】
【数１１６】
2007528059.tif 000118
【０２６０】
は現在の状態ビットであり、
【０２６１】
【数１１７】
2007528059.tif 000119
【０２６２】
は次の状態ビットであるとして、変数
【０２６３】
【数１１８】
2007528059.tif 000120
【０２６４】
を表すために
【０２６５】
【数１１９】
2007528059.tif 000121
【０２６６】
ビットが使用できると仮定する。
【０２６７】
【数１２０】
2007528059.tif 000122
【０２６８】
は、ブロック
【０２６９】
【数１２１】
2007528059.tif 000123
【０２７０】
に割り当てられ、残りのブロック
【０２７１】
【数１２２】
2007528059.tif 000124
【０２７２】
には割り当てられないとする。ブロック
【０２７３】
【数１２３】
2007528059.tif 000125
【０２７４】
において、
【０２７５】
【数１２４】
2007528059.tif 000126
【０２７６】
に割当てられた論理は
【０２７７】
【数１２５】
2007528059.tif 000127
【０２７８】
である。さらに、
【０２７９】
【数１２６】
2007528059.tif 000128
【０２８０】
は、基本ブロック
【０２８１】
【数１２７】
2007528059.tif 000129
【０２８２】
のインデックスであるとする。
【０２８３】
【数１２８】
2007528059.tif 000130
【０２８４】
に対するデータ論理は
【０２８５】
【数１２９】
2007528059.tif 000131
【０２８６】
となる。
【０２８７】
図７は、変数割当て論理を得るための組合せ回路を作る擬似コードを示している。図７は、いくつかの共通式、ビット毎のAND「＆」、和「＋」、等式「＝」、定数、および変数、にもとづいて回路を作る方法を示している。関数「AND_gate(bit1,bit2)」は、２つの入力bit1、およびbit2を有するANDゲートを作る。同様に、「OR_gate()」および「XOR_gate()」は、それぞれ、２入力のORおよびXORゲートを作る。図７の行２−６は、形式
【０２８８】
【数１３０】
2007528059.tif 000132
【０２８９】
の式を処理する。それは、部分式
【０２９０】
【数１３１】
2007528059.tif 000133
【０２９１】
に対する回路を最初に再帰的に作る。ベクトル
【０２９２】
【数１３２】
2007528059.tif 000134
【０２９３】
は、
【０２９４】
【数１３３】
2007528059.tif 000135
【０２９５】
に対する回路の出力であるとする。結果のベクトルは、
【０２９６】
【数１３４】
2007528059.tif 000136
【０２９７】
と同じビット幅を有する。各々の結果のビットは、２つの入力が
【０２９８】
【数１３５】
2007528059.tif 000137
【０２９９】
の対応するビットであるＡＮＤゲートの出力である。図７の行８−１７は、形式
【０３００】
【数１３６】
2007528059.tif 000138
【０３０１】
の式を処理する。それは、各ビット
【０３０２】
【数１３７】
2007528059.tif 000139
【０３０３】
に対する加算器を作る。
【０３０４】
【数１３８】
2007528059.tif 000140
【０３０５】
に対する論理は、
【０３０６】
【数１３９】
2007528059.tif 000141
【０３０７】
であり、初期値は零である。図７の行１９-２４における等式について、結果のベクトルは、１ビットのみを有する。ステートメントが定数であれば、結果のベクトルは定数の２進表現である。最後に、ステートメントが変数であれば、新しい信号が生成される。
【０３０８】
モデル化の実施形態はいくつかの特別処理で、ポインタ変数に拡張することができる。ポインタ変数が宣言されると、追加の変数を導入できる。追加の変数の数は、ポインタの数と同じとすることが可能である。たとえば、宣言
【０３０９】
【数１４０】
2007528059.tif 000142
【０３１０】
は、ポインタｐに対して、それぞれがそれ自身のデータ論理を有する４つの変数
【０３１１】
【数１４１】
2007528059.tif 000143
【０３１２】
を作る。
【０３１３】
【数１４２】
2007528059.tif 000144
【０３１４】
に対しても同数の変数をつくることができる。新たに作られた変数のすべては、正規の有限ドメイン変数である。しかし、
【０３１５】
【数１４３】
2007528059.tif 000145
【０３１６】
は、
【０３１７】
【数１４４】
2007528059.tif 000146
【０３１８】
の参照された値を暗黙的に示している。同じ関係は、
【０３１９】
【数１４５】
2007528059.tif 000147
【０３２０】
に対しても当てはまる。ポインタへの割当ては、文字どおりの値（face value）と参照された値（referenced value）を変化させ、これは付加的な割当てをもたらすことに注目されたい。プログラムの中に割当て
【０３２１】
【数１４６】
2007528059.tif 000148
【０３２２】
があれば、次の３つの割当て
【０３２３】
【数１４７】
2007528059.tif 000149
【０３２４】
が生成される。同様に、
【０３２５】
【数１４８】
2007528059.tif 000150
【０３２６】
は、
【０３２７】
【数１４９】
2007528059.tif 000151
【０３２８】
を含む４つの割当てをもたらす。Ｃコード内のデリファレンスも、付加的な変数と割当てをもたらす。ｒは、整数変数であるとする。割当て
【０３２９】
【数１５０】
2007528059.tif 000152
【０３３０】
は、
【０３３１】
【数１５１】
2007528059.tif 000153
【０３３２】
のデリファレンスされた値を示す新しい変数
【０３３３】
【数１５２】
2007528059.tif 000154
【０３３４】
を最初に生成し、次に２つの割当て
【０３３５】
【数１５３】
2007528059.tif 000155
【０３３６】
を作る。
【０３３７】
上述したように、コード簡略化処理は、各基本ブロックの連続的な割当てを並列にさせる。次の例の割当てを考える。
【０３３８】
【数１５４】
2007528059.tif 000156
【０３３９】
すでに説明したように、ポインタは、「＆ａ」および「＆ｘ」と示す２つの新しい変数が作られるように、処理することができる。追加の割当ては、エイリアシング（aliasing）と新たに導入された変数のために、推測されなければならない。行１における最初の割当ては、
【０３４０】
【数１５５】
2007528059.tif 000157
【０３４１】
になる。ｐ＝＆ａは、
【０３４２】
【数１５６】
2007528059.tif 000158
【０３４３】
を暗示するので、２つの新しい割当て
【０３４４】
【数１５７】
2007528059.tif 000159
【０３４５】
が推測される。行２における割当ては、
【０３４６】
【数１５８】
2007528059.tif 000160
【０３４７】
による割当て
【０３４８】
【数１５９】
2007528059.tif 000161
【０３４９】
だけでなく、エイリアシングによる条件付き割当ても生成する。ｐは＆ａと等しいことがあるので、ａが割当てられたときに、
【０３５０】
【数１６０】
2007528059.tif 000162
【０３５１】
は、新しい値を割当てられる可能性がある。これは、条件付き割当て
【０３５２】
【数１６１】
2007528059.tif 000163
【０３５３】
をもたらす。＆ｂがコード中に現れないので、
【０３５４】
【数１６２】
2007528059.tif 000164
【０３５５】
を考慮する必要がないことに注目されたい。すべての割当てを以下に列挙する。
【０３５６】
【数１６３】
2007528059.tif 000165
【０３５７】
１≦ｍ≦４として、ｍ.1と符号が付けられた割当ては、オリジナルの割当てであり、他の割当ては推測である。
【０３５８】
条件付き割当ての条件のいくつかは、同じ基本ブロック内の前の割当てにもとづいて除去することができる。たとえば、1.1における割当てが、条件が真であることを強制するので、2.3および2.4における条件
【０３５９】
【数１６４】
2007528059.tif 000166
【０３６０】
は、除去することができる。したがって、2.3および2.4における割当ては、それぞれ
【０３６１】
【数１６５】
2007528059.tif 000167
【０３６２】
まで評価することができる。2.1および2.3における割当ては共に、4.2における条件
【０３６３】
【数１６６】
2007528059.tif 000168
【０３６４】
が真であることを意味している。同様に、4.3および4.4における条件は真である。したがって、条件付き割当ては次の形式に単純化することが可能である。
【０３６５】
【数１６７】
2007528059.tif 000169
【０３６６】
次に、連続的な割当てを並列割当てに変換するために、すべての考えられるリード・アフタ・ライト・ハザードは除去される。そうすることによって、同じ変数が同じ基本ブロックに前もって割当てられていれば、右辺の読み取り変数は割当てられた値に置換される。その結果、3.1および3.2における割当ては、それぞれ
【０３６７】
【数１６８】
2007528059.tif 000170
【０３６８】
に変更される。さらに、基本ブロックを１つの最小構成段階であると考えれば、いくつかの割当ては冗長である。特に、後の段階における割当ては、前の割当てを上書きする恐れがある。前の割当てを除去した後の最終的な割当てを以下に示す。
【０３６９】
【数１６９】
2007528059.tif 000171
【０３７０】
ここで、割当ては並列に実行可能であると考えられることに注目されたい。
【０３７１】
本発明は上述した特定のモデル化に制限されないことに注目するべきである。たとえば、そして限定することなく、ヒープを１連のロケーションとするモデル化するようなもっと従来からの別の変換を使用することもできる。
【０３７２】
抽象      抽象（abstraction）は、モデル検査における条件急増問題（state explosion problem）を減少させるための、恐らく最も重要な技術である。述語抽象化（predicate abstraction）は、複雑な潜在的に無限状態システムから有限状態モデルを抽出するための、強力で人気のある技術であることが明らかになっている。図１に示すように、抽象化段階１３０は、述語抽象化１３２の技術を利用する。この方法は、抽象のために使用される興味のある述語を識別する能力と、抽象遷移を正確に計算する能力に依存する。抽象システムにおいて遷移関係を計算するために大規模で本質的に費用がかかるさまざまな定理試験装置（theorem prover）への呼出しを使用するソフトウェアに対する述語抽象化の初期の研究に対して、ここに開示するように、遷移関係を計算するためには、ＳＡＴベースの方法によることが有利である。さらに、以下に詳細に説明するように、近似的な抽象モデルの計算を可能にし、いくつかの共通の計算を再利用するために、さまざまな遷移関係の列挙法の具体化を制約して、その結果より高速の計算を可能にすることが有利である。
【０３７３】
ｎ個のブーリアン述語
【０３７４】
【数１７０】
2007528059.tif 000172
【０３７５】
の集合を考える。これらのブーリアン述語に対する真理値は、考慮しているブロックを入力するときに、ブーリアン述語に対する値を仮定して各ブロックを選んだ後に更新されるべきである。これらの変数およびそれらの参照とデリファレンス
【０３７６】
【数１７１】
2007528059.tif 000173
【０３７７】
に広がる述語に対する変数の集合
【０３７８】
【数１７２】
2007528059.tif 000174
【０３７９】
をマップする、関数Ｐｒｅｄｓ
【０３８０】
【数１７３】
2007528059.tif 000175
【０３８１】
を定義する。並列な割当て
【０３８２】
【数１７４】
2007528059.tif 000176
【０３８３】
を所与のものとすると、述語
【０３８４】
【数１７５】
2007528059.tif 000177
【０３８５】
に対する所要の変数の集合は、
【０３８６】
【数１７６】
2007528059.tif 000178
【０３８７】
となる。
【０３８８】
【数１７７】
2007528059.tif 000179
【０３８９】
の変数は直接
【０３９０】
【数１７８】
2007528059.tif 000180
【０３９１】
に影響を与えるが、述語の集合
【０３９２】
【数１７９】
2007528059.tif 000181
【０３９３】
によって
【０３９４】
【数１８０】
2007528059.tif 000182
【０３９５】
として与えられる完全な精度に到達するためには、より多くの述語と変数を分析に含めることが必要であり、上式は、反復して計算することもできる。これは、１組の述語
【０３９６】
【数１８１】
2007528059.tif 000183
【０３９７】
に対して、
【０３９８】
【数１８２】
2007528059.tif 000184
【０３９９】
に一般化できる。
【０４００】
【数１８３】
2007528059.tif 000185
【０４０１】
の集合と、１組の述語
【０４０２】
【数１８４】
2007528059.tif 000186
【０４０３】
は、したがって、
【０４０４】
【数１８５】
2007528059.tif 000187
【０４０５】
と定義できる。並列の割当てに対しては、更新されるべき述語の集合は
【０４０６】
【数１８６】
2007528059.tif 000188
【０４０７】
と定義でき、所要の述語の集合は
【０４０８】
【数１８７】
2007528059.tif 000189
【０４０９】
と定義でき、未使用の述語の集合は
【０４１０】
【数１８８】
2007528059.tif 000190
【０４１１】
と定義できる。
【０４１２】
各述語
【０４１３】
【数１８９】
2007528059.tif 000191
【０４１４】
に対して、新しいブール変数
【０４１５】
【数１９０】
2007528059.tif 000192
【０４１６】
をプログラムの抽象に加えることができる。集合
【０４１７】
【数１９１】
2007528059.tif 000193
【０４１８】
に対して、集合
【０４１９】
【数１９２】
2007528059.tif 000194
【０４２０】
にもとづいて抽象を考える。表記上の都合によって、ブーリアン表現の評価は、多くの場合に集合よりもベクトル
【０４２１】
【数１９３】
2007528059.tif 000195
【０４２２】
であると考える。次の論議は、これらのブール変数
【０４２３】
【数１９４】
2007528059.tif 000196
【０４２４】
に対する現在の状態から次の状態の関係を説明して、遷移関係の計算を実現する２つの方法を開示している。これに関連して、新しい基本ブロックを入力するときのブール変数の現在の状態はブール変数の評価を示し、次の状態は基本ブロックのすべてのステートメントを実行した後、すなわち、基本ブロックを抜ける直前の同じブール変数の評価を示す。抽象の初期状態は完全にランダム、すなわち、
【０４２５】
【数１９５】
2007528059.tif 000197
【０４２６】
に対するどの真理組み合わせも有効であることに注目すべきである。
【０４２７】
より形式的には、抽象化の目的のために、集合
【０４２８】
【数１９６】
2007528059.tif 000198
【０４２９】
を
【０４３０】
【数１９７】
2007528059.tif 000199
【０４３１】
のスーパー・セットとして定義する。記号⊥は、具体的な状態空間内の同じ記号に対応する、すなわち、所与の基本ブロック内で有効範囲外である場合には、⊥に対する述語評価に対応する。記号「？」は、述語は所与の基本ブロック内で定義されるが、本明細書では真（１）あるいは偽（０）に対するその評価に興味を有しないということを示すために使用される。この表記法は、近似的抽象化（approximate abstraction）の説明のために使用できる。
【０４３２】
したがって、長さ
【０４３３】
【数１９８】
2007528059.tif 000200
【０４３４】
の述語
【０４３５】
【数１９９】
2007528059.tif 000201
【０４３６】
のベクトルに対する抽象状態
【０４３７】
【数２００】
2007528059.tif 000202
【０４３８】
の集合は、
【０４３９】
【数２０１】
2007528059.tif 000203
【０４４０】
である。具体的な状態空間と同様に、所与の位置
【０４４１】
【数２０２】
2007528059.tif 000204
【０４４２】
に対する述語の範囲に対して整合性（consistent）があるベクトル
【０４４３】
【数２０３】
2007528059.tif 000205
【０４４４】
のみを含む、位置に特有の集合
【０４４５】
【数２０４】
2007528059.tif 000206
【０４４６】
を定める。したがって、初期抽象状態の集合は
【０４４７】
【数２０５】
2007528059.tif 000207
【０４４８】
である。
【０４４９】
ブーリアン述語ベクトル
【０４５０】
【数２０６】
2007528059.tif 000208
【０４５１】
の具体化
【０４５２】
【数２０７】
2007528059.tif 000209
【０４５３】
は、次式
【０４５４】
【数２０８】
2007528059.tif 000210
【０４５５】
に対する真の割当ての集合である。
【０４５６】
【数２０９】
2007528059.tif 000211
【０４５７】
内のすべての変数の有効範囲が既知であると仮定すると、K.L. McMillan「無限の記号モデル検査におけるＳＡＴ方法の適用」（Applying SAT Methods in Unbounded Symbolic Model Checking）、14th Int'l Conference on Computer Aided Verification、Vol. 2404 of Lecture Notes in Computer Science、pp. 250-64 (2002)に記載されたアルゴリズムを使用して、すべてのこのような割当てを列挙するために使用できる、ビット・ブラストされた表現式が生成できる。範囲分析の構造は、プログラム内の各変数とステートメントに対する適切なビット幅を見出すために使用できる。さらに、これらの定義をＢの代わりに集合Ｔに拡張することと、抽象状態
【０４５８】
【数２１０】
2007528059.tif 000212
【０４５９】
にそれを拡張することは、容易であることに注目されたい。具体的な遷移関係
【０４６０】
【数２１１】
2007528059.tif 000213
【０４６１】
を考慮すれば、述語
【０４６２】
【数２１２】
2007528059.tif 000214
【０４６３】
のベクトルが
【０４６４】
【数２１３】
2007528059.tif 000215
【０４６５】
として与えられるとすると、抽象遷移関係
【０４６６】
【数２１４】
2007528059.tif 000216
【０４６７】
を定義することが可能である。
【０４６８】
【数２１５】
2007528059.tif 000217
【０４６９】
が表現式であり、
【０４７０】
【数２１６】
2007528059.tif 000218
【０４７１】
はｋ個の変数の集合であり、
【０４７２】
【数２１７】
2007528059.tif 000219
【０４７３】
がｋ個の表現式であると、
【０４７４】
【数２１８】
2007528059.tif 000220
【０４７５】
はσ内の変数
【０４７６】
【数２１９】
2007528059.tif 000221
【０４７７】
に対する表現式σiのポイント毎の置換えによって得られた表現式を示す。
【０４７８】
割当て集合
【０４７９】
【数２２０】
2007528059.tif 000222
【０４８０】
、更新された述語
【０４８１】
【数２２１】
2007528059.tif 000223
【０４８２】
の集合、および所要の述語
【０４８３】
【数２２２】
2007528059.tif 000224
【０４８４】
の集合を有するブロックの場合、集合
【０４８５】
【数２２３】
2007528059.tif 000225
【０４８６】
は、それぞれ
【０４８７】
【数２２４】
2007528059.tif 000226
【０４８８】
に対応する、集合
【０４８９】
【数２２５】
2007528059.tif 000227
【０４９０】
に分割することができる。
【０４９１】
【数２２６】
2007528059.tif 000228
【０４９２】
における現在の状態ブール変数に依存して、ブール変数
【０４９３】
【数２２７】
2007528059.tif 000229
【０４９４】
に対するブール変数
【０４９５】
【数２２８】
2007528059.tif 000230
【０４９６】
の次の状態に対して、遷移関係
【０４９７】
【数２２９】
2007528059.tif 000231
【０４９８】
を
【０４９９】
【数２３０】
2007528059.tif 000232
【０５００】
として表わすブーリアン式を得ることができる。
（一度に１つの述語が考慮されているとすれば、集合
【０５０１】
【数２３１】
2007528059.tif 000233
【０５０２】
は、すべての述語にもとづいて計算され、緩和し（relaxed）得ることに注目すべきである。すなわち、１つの述語
【０５０３】
【数２３２】
2007528059.tif 000234
【０５０４】
を考慮すれば、集合
【０５０５】
【数２３３】
2007528059.tif 000235
【０５０６】
は
【０５０７】
【数２３４】
2007528059.tif 000236
【０５０８】
である。）同様に、
【０５０９】
【数２３５】
2007528059.tif 000237
【０５１０】
におけるすべてのブール変数の次の状態に対する遷移関係
【０５１１】
【数２３６】
2007528059.tif 000238
【０５１２】
を、
【０５１３】
【数２３７】
2007528059.tif 000239
【０５１４】
における現在の状態のブール変数に依存して、
【０５１５】
【数２３８】
2007528059.tif 000240
【０５１６】
として表すブーリアン式を得ることができる。
【０５１７】
上記の遷移関係は、
【０５１８】
【数２３９】
2007528059.tif 000241
【０５１９】
を定義することによって、ブール変数にのみ及ぶように限定することが可能である。表記の便宜上、表記
【０５２０】
【数２４０】
2007528059.tif 000242
【０５２１】
を使用して、任意の集合
【０５２２】
【数２４１】
2007528059.tif 000243
【０５２３】
に対する集合
【０５２４】
【数２４２】
2007528059.tif 000244
【０５２５】
を示す。したがって、本明細書では、集合
【０５２６】
【数２４３】
2007528059.tif 000245
【０５２７】
を示すために、
【０５２８】
【数２４４】
2007528059.tif 000246
【０５２９】
を使用する。
【０５３０】
各基本ブロックに対して、１つの遷移関係
【０５３１】
【数２４５】
2007528059.tif 000247
【０５３２】
がこのように生成される。遷移関係のすべての満たす割当て（satisfying assignment）
【０５３３】
【数２４６】
2007528059.tif 000248
【０５３４】
は、具体的なシステム（考慮中のＣブロック）と、ブーリアン述語の現在の集合が与えられたとしてその抽象における遷移を表す。
【０５３５】
【数２４７】
2007528059.tif 000249
【０５３６】
を計算するために、このような満足させる割当てをブール変数
【０５３７】
【数２４８】
2007528059.tif 000250
【０５３８】
に投射することができ、したがって、抽象満足割当て（abstract satisfying assignment）
【０５３９】
【数２４９】
2007528059.tif 000251
【０５４０】
を
【０５４１】
【数２５０】
2007528059.tif 000252
【０５４２】
と定義することによって、抽象化されたシステム内に１つの考えられる遷移を得ることができる。抽象システム内のすべての考えられる遷移を見出すことにのみ関心があるので、列挙アルゴリズムの効率的な実現例を使用できる。上記の McMillan 文献を参照されたい。抽象遷移の列挙は、以前の解を再現させないいわゆるブロッキング・クローズ（blocking causes ）の反復加算によって進行する。ブーリアンの式
【０５４３】
【数２５１】
2007528059.tif 000253
【０５４４】
にブロッキング・クローズ
【０５４５】
【数２５２】
2007528059.tif 000254
【０５４６】
を加算した後に、ＳＡＴソルバーは、このような割当てがまだ存在すれば、強化した問題公式化（enriched problem formulation）の別の満足割当てを見出すように、求められることができる。ＳＡＴソルバーを使用する遷移関係の列挙は、費用が掛かり指数関数的に多くの、定理照明装置への呼出しの使用と比べて、遷移関係を計算する効率的な方法である。
【０５４７】
さまざまな遷移関係の列挙の実現例は、実現例にいくつかの共通の計算を再利用するよう強いることによって、さらに改良することができ、その結果全体の計算を高速化することができる。考慮しているブール変数の集合がしばしば一部しか同じでない場合、多くの遷移関係を計算する必要があるので、プログラム全体を意味深く観察して、これらの遷移関係の列挙のインテリジェントなスケジューリングと、抽出された意味の適切なメモリ管理が、プログラム全体で見たとき抽象化の全手順の計算時間を著しく短くする可能性がある。
【０５４８】
多くの場合、ｎ個の述語の集合は、これらの述語の２n個の多くの整合性がある抽象解釈（consistent abstract interpretations）があることを意味しないことに注目すべきである。実際、結局のところ、多くの場合に重複する述語あるいは並列述語が多数存在し、これらの評価の多くの組み合わせはどのような具体的な状態にも対応していない。複数の述語が互いに並列であるか否かを分析する単純な前処理段階は、実行時間をかなり節約することができる。たとえば、大きさが８、８、９、９の４組の並列な述語と１つの非並列の述語に分割できる３５個の関連する述語を含んだ場合を考える。この前後関係での並列な述語は、２ｘ−ｙ−４ｚ／５＝２、２ｘ−ｙ＞５＋４ｚ／５、および２ｘ−０．８ｚ＜ｙのような述語を含んでいる。このような９つの並列な述語の組においては、たとえば、最大で１０の整合性がある評価が存在するが、完全な検索では２9の多くの組み合わせをループすることになる。前述の場合には、３５個の述語は、したがって、最大で２・９2・１０2＜２14の多くの抽象無矛盾状態（abstract consistent state）を表すことができるこれは分析を、計算のこの時点において、２21＞２・１０6の１以上減少させる。この節減は何回かの遷移関係計算に再使用できるので、節減された計算時間の合計はこの倍数である。
【０５４９】
並列な述語の上述の分析に加えて、具体的な状態空間における述語の別の整合性がない評価がしばしば存在する。たとえば、
【０５５０】
【数２５３】
2007528059.tif 000255
【０５５１】
形式の述語である１組の区切り述語（separation predicate）の場合、これらの述語の集合の有効な組み合わせを決定することができる。実行可能な有効な組み合わせの集合のこのような減少は、実行可能な組み合わせの集合が簡潔に表現できれば、後の処理段階に有用であり得る。実行可能な組み合わせの完全な列挙も可能かもしれないが、実行可能な組み合わせの結果として生ずる集合は、十分に簡潔ではないことがある。列挙の間にいくつかの関係と意味を発見し、これらを後の計算段階のために記憶することも有用である。
【０５５２】
現在の状態のブール変数から次の状態のブール変数への遷移関係の列挙の場合、実行可能なブーリアン述語の真理組み合わせ（truth combination）の大きさを減少させる効果は、これらの変数の現在の状態の表現と次の状態の表現の両方に現れる。さらに、さまざまな基本ブロック計算の分析と、さまざまな遷移関係の列挙のインテリジェントなスケジューリングは、抽象の計算の間に大幅に時間を節約することができる。たとえば、多くのソフトウェア・アプリケーションにおいて、いくつかの類似の形式でしばしば見られる下記のコード・フラグメントを考える。
【０５５３】
【数２５４】
2007528059.tif 000256
【０５５４】
説明のために、ここでは、ｘ＞２を表すｂ1とｘ＞３を表すｂ2の２つの述語を考える。次に、表現式ｘ＞１は、
【０５５５】
【数２５５】
2007528059.tif 000257
【０５５６】
と書かれた、コード・フラグメントのｔｈｅｎ−ｐａｒｔにおいて
【０５５７】
【数２５６】
2007528059.tif 000258
【０５５８】
に対する前状態が真であることを表わし、一方
【０５５９】
【数２５７】
2007528059.tif 000259
【０５６０】
も表わしている。このように、２つの列挙を１つに組み合わせることによって、遷移関係の１つの全計算を節約することができる。したがって、次の式を列挙することができる。
【０５６１】
【数２５８】
2007528059.tif 000260
【０５６２】
（これは、さらに前処理を実行できる単純な場合であることに注目すべきである。これらは、説明をわかりやすくするために省略されている。より多くの述語を組み入れると、節減の規模が増加することにも注目すべきである。）計算が、以上に説明した方法で組み合わせられなくても、考慮しているブーリアン述語と命令の集合は、異なる基本ブロックを表すさまざまな遷移関係におけるものと部分的に同じである場合が多い。これらの場合の分析と最初に共通部分の列挙を可能にするスケジューリングは、すべての遷移関係に対して必要とされる全体の計算量を最少にするために使用できる。
【０５６３】
全体の実行時間は、抽象化時間を減少させるために近似的な抽象モデルの計算を可能にすることによってさらに減少させることができる。たとえば、現在の状態のブーリアン述語変数と次の状態のブーリアン述語変数の間の全遷移関係に対して考えられる解の集合を列挙することは実行不可能な場合があるが、次の状態のブーリアン述語変数のサブセットのみ、あるいは、個々の次の状態のブーリアン述語変数のみが同時に考慮される場合、複数の遷移関係を列挙することによって、実行時間を減少させるこができる。たとえば、これら遷移関係の全部を列挙できなくても、いくつかの遷移関係を指定しないでおくことができ、したがって次のモデル検査段階に対する非決定的な選択が可能になる。他方、いくつかの抽象化された満足割当てをさらなる考慮から除外することによって、遷移関係全体にもとづいて近似をさらに計算できる。このような決定は通常、考慮されるべきクローズ（clasues）の所定の最大の長さにもとづいて行われる。近似的抽象化を計算するためには、非満足化可能性に対して次の式をチェックすることのみが必要であることに注目されていた。抽象状態（ｌ1，ｂ1）と（ｌ2，ｂ2）の間の抽象状態空間の遷移は、次式
【０５６４】
【数２５９】
2007528059.tif 000261
【０５６５】
が満たされない場合にのみ、近似的遷移関係、すなわち（ｌ1，ｂ1）→（ｌ2，ｂ2）に含まれる。有効な述語の数を小さい定数に制限することによって、すなわち、述語ベクトル表現内に所定数の「０」あるいは「１」を有し、他の適切なところに？と⊥を有する過抽象状態（over abstract state）のみを反復することによって、遷移関係の過度近似（over-approximation）を簡単に作ることができる。この反復の間に、現在の状態（ｌ1、ｂ1）内の有効ビットの数と、次の状態（ｌ2、ｂ2）内の有効ビットの数を識別することができる。遷移関係の近似
【０５６６】
【数２６０】
2007528059.tif 000262
【０５６７】
が可能であるから、近似的遷移関係を
【０５６８】
【数２６１】
2007528059.tif 000263
【０５６９】
として示すことができ、一般に遷移関係
【０５７０】
【数２６２】
2007528059.tif 000264
【０５７１】
を使用して到達可能性分析を行うことができる。
【０５７２】
反例分析と改善      このように、考慮している抽象化モデルの過度近似を可能にすることは、抽象の計算の実行時間を減少させるが、擬似的な反例がモデル検査段階の間に出現するおそれも増加させる。したがって、図１に記載したように、システムは、１６０においてこのような擬似的な反例に対する分析検索を実行し、１７０においてさらに改善を実行する。
【０５７３】
擬似的な反例の概念は、副経路（sub-path）あるいは「フラグメント」の可能性に対する試験に一般化できる。形式的には、１組の安全でない位置
【０５７４】
【数２６３】
2007528059.tif 000265
【０５７５】
を、
【０５７６】
【数２６４】
2007528059.tif 000266
【０５７７】
が初期抽象状態であり、
【０５７８】
【数２６５】
2007528059.tif 000267
【０５７９】
であるように、一連のｋ個の抽象状態
【０５８０】
【数２６６】
2007528059.tif 000268
【０５８１】
として与えられるとして
１組の述語
【０５８２】
【数２６７】
2007528059.tif 000269
【０５８３】
に対する抽象状態空間
【０５８４】
【数２６８】
2007528059.tif 000270
【０５８５】
内に長さｋの抽象経路を定義する。したがって、長さｋの抽象反例は、安全でない位置で終わる経路、すなわち、
【０５８６】
【数２６９】
2007528059.tif 000271
【０５８７】
である。しかし、近似的遷移関係が許容されるので、近似的な抽象経路、および近似的な抽象反例を、
【０５８８】
【数２７０】
2007528059.tif 000272
【０５８９】
の代わりに関係
【０５９０】
【数２７１】
2007528059.tif 000273
【０５９１】
を使用して、類似的に定義する。反例分析のために、長さｋの反例のフラグメントに対応する表現式を定義する。具体的な状態空間内の遷移関係→の時限バージョン（timed version）、あるいはタイム・ステップ、あるいはアンローリングｉ（ただし、０≦ｉ＜ｋ−１）を、時限変数あるいはアンロールした変数（timed or unrolled variables）にわたって
【０５９２】
【数２７２】
2007528059.tif 000274
【０５９３】
として定義する。近似的な抽象経路
【０５９４】
【数２７３】
2007528059.tif 000275
【０５９５】
内の基本ブロックの順序は既知であるので、効率化のために、制御流れ図内の適切な遷移に対するじ実現において、さまざまな時限関係（timed relation）
【０５９６】
【数２７４】
2007528059.tif 000276
【０５９７】
を、
【０５９８】
【数２７５】
2007528059.tif 000277
【０５９９】
までの基本ブロック遷移に、さらに制限することができる。したがって、フラグメントは、
【０６００】
【数２７６】
2007528059.tif 000278
【０６０１】
に対して、
【０６０２】
【数２７７】
2007528059.tif 000279
【０６０３】
と定義することができる。
表現式
【０６０４】
【数２７８】
2007528059.tif 000280
【０６０５】
が、いくつかの対
【０６０６】
【数２７９】
2007528059.tif 000281
【０６０７】
に対して満たされないならば、反例が真に擬似的であることが判明する。
【０６０８】
従来技術による分析と改善法は、形式ｊ＝ｉ＋１のフラグメントを考慮した擬似的な遷移を考えていることに注目すべきである。さらに、従来の接頭辞反例分析法（prefix counter-example analysis approach）は、形式ｉ＝０のフラグメントのみを、僅かな追加（with a minor addition）と共に考慮している.すなわち、第１の抽象状態を含めるとき、反例を介する考えられる経路は、初期状態の集合の中で開始することを検証することも必要である。しかし、本例の場合、基本ブロック
【０６０９】
【数２８０】
2007528059.tif 000282
【０６１０】
内
【０６１１】
【数２８１】
2007528059.tif 000283
【０６１２】
のすべての明確に定義された状態は初期状態であると定義されるので、このチェックはここでは省略可能である。このように、完全な反例分析のためには、システムは単に式
【０６１３】
【数２８２】
2007528059.tif 000284
【０６１４】
を考慮する。
【０６１５】
擬似的な反例に対するより良い理由を発見し、したがってより強い述語を生成するために投資された、追加の研究は、反例に導かれた抽象化改善法の全体において、到達可能性を立証あるいは反証するために必要な反復の数を、大幅に減少させることができる。フラグメントのこの種類の分析は、反例が長くなるにつれて、ますます重要になるであろう。擬似的な反例の根拠は一連の比較的少数の抽象状態における局部的な問題であるが、すべての他の反例に導かれた改善法で、これまでのところ主張されているように、接頭部分析（prefix analysis）は、真の理由を歪がませ、新しい述語のサブ特性（sub-quality）の集合を見つけてしまうことがある。非常に類似した擬似的なフラグメントを有する類似の反例は、事前の分析と改善段階の間に明らかにされていなければ、次の反復において再度出現することがある。
【０６１６】
ＳＡＴソルバー（solver）がモデル・チェッカーとして利用される場合、ＳＡＴソルバーは、満たすことができない、さもなければ非満足化可能性コア（unsatisfiability core）として知られる、満たされない副式を生成することがある。ＳＡＴソルバーによって計算された非満足化可能性コアを使用することによって、擬似的な反例の改善はさらに焦点が絞られる。
【０６１７】
カスタマイズされた決定ヒューリスティックス      システムによって生成されたブーリアン表現は、ここで説明する特定の翻訳にもとづく多くの共通の特徴を含んでいる。上述したプログラム・カウンタは制御流れ図内の進行を追跡するが、オリジナルのソフトウェアには、モデル検査の効率を改善できる追加の情報がある。有限モデル検査の前後関係において、性能を改善できるさまざまなヒューリスティックスがある。
【０６１８】
ＰＣ変数のスコア      ＳＡＴソルバーがデータ・フローではなく制御流れに対応する変数を最初に決定する可能性を増加させる単純な決定ヒューリスティックは、新しいアンローリングの各々が、コード全体が制御流れ図の静的解析にもとづいて到達されることを許容しないことを利用している。このヒューリスティックは、ｐｃ変数のビットに対するスコア（score）を増加させることによって実現でき、このことはバックエンドＳＡＴソルバーに、これらの変数を決定変数として最初に選ばせる。このヒューリスティックは、モデル・チェッカーが制御流れ図の静的到達可能性の計算に最初に集中するようにさせ、したがって、多くのトレース（traces）を素早く除去することが可能である。システム内でｐｃ変数を他の変数よりも高くスコアすることに加えて、さまざまな時間フレームにわたって変数のスコアの変化させ方を制御することも有利なことがある。たとえば、ｐｃ変数の関連性を前の時間フレームよりも後の時間フレームで増加させることは、上述したＤＩＶＥＲツールに固有のＳＡＴソルバー決定を利用している。
【０６１９】
ワン・ホット符号化      有用な他のヒューリスティックは、ＳＡＴソルバーがフルｐｃ上で決定を行うことを可能にするｐｃ変数のワン・ホット（oneーhot）符号化である。すでに回路に存在している２進コード化されたｐｃ変数に加えて、各基本ブロックに対して新しい選択ビットを追加することができる。選択ビットは、基本ブロックがアクティブであれば、すなわち、ｐｃ変数ビットのある組み合わせが有効であれば、設定することが可能である。ｐｃ変数を介して一定の基本ブロック選択ビットがすべての他の基本ブロック選択ビットを自動的に無効にするので、これはワード・レベルの決定のためのメカニズムを提供する。基本ブロック選択ビットを設定するためにシステム内の他の変数と比較してスコアを増加させることによって、ＳＡＴソルバーが最初に位置についての速い決定を行うように影響を与えることが可能である。このヒューリスティックの明白な欠点は、ソフトウェア・プログラムの基本ブロックごとにブーリアン・モデルに対して１つの選択ビットを含める必要があることである。
【０６２０】
さらに、制御流れ図から予め計算された静的到達可能性情報を考慮することによって、これらの基本ブロック選択ビットに対するスコアを、ある程度のデータ処理ができるように（intelligently）増加させることが可能である。制御流れ図の深度ｋにおいて対応する基本ブロックに実際に静的に到達可能ならば、深度ｋにおいてこれらの基本ブロック選択ビットに対してスコアを増加させる必要があるのみである。これは、制御流れ図上のさまざまな深度において連絡可能な基本ブロックの追加的なＢＦＳを必要とする。
【０６２１】
図５に示す制御流れ図を考える。制御流れ図の各基本ブロックには、ワン・ホット符号化を説明するために使用される固有の番号を付与することができる。ｂiは基本ブロックｉに対する選択ビットを表し、ｃi，０≦ｉ≦３は４個の必要とするプログラム・カウンタ変数ビットを表すとする。各基本ブロックに対しては制約条件が追加可能であり、基本的な選択変数を２進コード化されたプログラム・カウンタ・ラベルの等しいとする。たとえば、
【０６２２】
【数２８３】
2007528059.tif 000285
【０６２３】
ここで、１にｂ0を割当てるＳＡＴソルバーによる決定は、プログラム・カウンタ上のワード・レベルの決定に対応し、これは直ちに、本例におけるｂ6＝０を含めて、ｂi＝０，ｉ＞０を意味する結果をもたらす。
【０６２４】
さらに、前の時間フレーム内よりも後の時間フレーム内で変数を記録（score）することの既に説明した利点と同様に、このヒューリスティックで説明した選択ビットのスコアに同じ方法を使用することも可能である。
【０６２５】
ＣＦＧ遷移の明示的なモデル化      制御流れ図内の不可能な先行基本ブロックの組み合わせを除外するように探索スペースを制約することによって、バックエンドＳＡＴソルバーの分析を支援することはさらに有利である。これらの制約条件は補足的な高レベル情報を収集し、ＳＡＴソルバーの探索スペースの削減に有効である。各深度において、特定の基本ブロックを考慮するためのＳＡＴソルバーの選択は、予想される先行ブロックの数の制限を可能にし、すべての他の基本ブロックを直ちに考慮の対象外にする。ＳＡＴソルバーが最初にｐｃ上で決定する可能性を増加させることによって、新しいアンローリングの各々がコード全体に対して各深度において到達可能であることを許容しないことを利用することができる。ソフトウェアのブーリアン・モデルは、ｐｃ変数に関して出力遷移（outgoing transition）を既に符号化しているので、基本ブロックへの入力遷移（incoming transition）にもとづいて、これらの制約条件を追加することが望ましい。
【０６２６】
［００７２］たとえば、０≦ｉ≦３としてｃi'は次の状態のｐｃ変数ビットを示すと仮定して、次の制約条件
【０６２７】
【数２８４】
2007528059.tif 000286
【０６２８】
が図５の基本ブロック７に追加される。同様に、基本ブロック３に対して、次の制約条件
【０６２９】
【数２８５】
2007528059.tif 000287
【０６３０】
を追加する。ここで、ｇは、「ｘ＞４」の表現式を意味する。このような制約条件は、これらの両方のヒューリスティックスが利用されていれば、基本ブロックのワン・ホット符号化された選択ビットに関しても追加可能である。したがって、基本ブロック７に対する制約条件は、単純に
【０６３１】
【数２８６】
2007528059.tif 000288
【０６３２】
となる。この制約条件の追加によって、ＳＡＴソルバーがb7’を１に割当てれば、すなわち、現在のブロックは７であれば、先行（predecessor）ブロックはブロック３あるいは４の１つであることが必要である。
【０６３３】
このヒューリスティックは、ヒューリスティックを適用する基本ブロックのサブセットを選択することによって、カスタマイズ可能である。あまりにも多くの追加の制約は、効率を改善するよりも、ＳＡＴソルバーに重荷を負わせることがあるので、このカスタマイズは、利用者が、生成された追加の制約の量を微調整することを可能にしている。たとえば、そし限定することなく、利用者が次の選択を指定することが可能である。
・制御流れ図内のすべての基本ブロックに対する追加の制約条件を含む。
・複数の入力遷移を有する基本ブロックに対してのみ追加の制約条件を含む。この選択は、ＳＡＴソルバーが、いくつかの選択があるときに、入力エッジの１つを選ぶことを必要とすある。これは、ＳＡＴソルバーが一度に１つの実行可能な経路に速く焦点を合わせることを可能にする。
・１つの入力遷移を有する基本ブロックに対してのみ追加の制約条件を含む。この選択は、複数の入力エッジが存在しない場合に、ＳＡＴソルバーが、逆方向に経路を速く伝搬させるのを助ける。この処理は、このような基本ブロック内のｐｃ変数に対する不必要な決定を直ちに緩和する。
さらに、別の最適化は、その深度において実際に到達可能な深度における基本ブロックへの追加の制約条件を制限することである。ワン・ホット符号化ヒューリスティックについて上述した最適化に類似している、この最適化は、到達可能な基本ブロックの追加のＢＰＳを必要とする。
【０６３４】
本発明による例示的な図面と具体的な実施形態を説明し図示したが、本発明の範囲は説明した特定の実施形態に限定されないことが理解されるべきである。したがって、これら実施形態は限定するものではなく説明のためと見なされるべきであり、種々の変形がこれらの実施形態において、後に続く特許請求の範囲に記載した本発明の範囲およびその構造上および機能上の等価物から逸脱することなく、当業者によってなされることが理解されるべきである。ただ多くの変形例の１つとして、本発明による前後関係においてＣ以外のプログラム言語が容易に利用できることが理解されるべきである。
【図面の簡単な説明】
【０６３５】
【図１】本発明の実施形態によるソフトウェア・プログラムで実行される処理を図示する抽象図を示す。
【図２】ソフトウェア・プログラムから基本ブロックを作る擬似コードである。
【図３】非再帰的な関数呼出しを含むソフトウェア・プログラムから基本ブロックを作る擬似コードである。
【図４】コードのために生成される制御流れ情報を示すＣコードの例である。
【図５】コードのために生成される制御流れ図を含むＣコードの他の例である。
【図６】制御論理の真理値表である。
【図７】変数割当て論理を得る組合せ回路を作る擬似コードである。
【図１】
2007528059.tif 000291
【図２】
2007528059.tif 000292
【図３】
2007528059.tif 000293
【図４】
2007528059.tif 000294
【図５】
2007528059.tif 000295
【図６】
2007528059.tif 000296
【図７】
2007528059.tif 000297