(57)【要約】ソフトウェアモデルに特有の多数の特性を用いるソフトウェアモデル用シンボリック離接型イメージ計算方法。特に、ソフトウェアモデル全体がサブモジュールの離接集合に分解され、遷移関係の別の集合が構築される。イメージ／到達可能性分析が実行され、元のイメージ計算は、他から独立した個々のサブモジュールで実行可能なイメージ計算ステップの集合に分割される。好都合に、元のモデルをサブモジュールに分解する間に、変数の局所性を利用する。この分解を多方向ハイパーグラフ分割問題として定式化することにより、サブモジュールの小さい集合を有利に作製し、同時に各個別のサブモジュール内の生きている変数の数を極小化する。従来技術では必要な連接遷移関係を生成せずに、本発明の方法は、ソフトウェアモデルから直接に離接遷移関係の集合を生成する。さらに別の利益をもたらす新規な探索戦略に加えて、生きている変数の排他的な使用を利用する。【特許請求の範囲】
【請求項１】
順序システムを検査する方法であって、
１つの分割のみが一度に遷移できるように、前記順序システムのモデルを離接分解する段階と、
連接遷移関係及び存在量化を使用せずに、離接的に分割された遷移関係を直接構築する段階と、
全体の計算を個別の分割の計算に分解することにより、シンボリックイメージ計算を行う段階と、
を有する方法。
【請求項２】
前記順序システムは、コンピュータソフトウェアから導出されたモデルを有する請求項１に記載の方法。
【請求項３】
前記離接分解する段階は、ハイパーグラフ分割の使用によって、前記システムのモデルを１または複数のブロックを有する分割に分解する段階をさらに含む、請求項１に記載の方法。
【請求項４】
ハイパーグラフ分割の使用によって、複数の分割に共有される生きている変数の数を極小化する段階をさらに有する、請求項３に記載の方法。
【請求項５】
ハイパーグラフ分割の使用によって、複数の分割に共有される割り当てられた変数の数を極小化する段階をさらに有する、請求項３に記載の方法。
【請求項６】
ハイパーグラフ分割の使用によって、複数の異なる分割内のブロック間の遷移の数を極小化する段階をさらに有する、請求項３に記載の方法。
【請求項７】
ｘがθ(ｂj，ｂk)内あるいはδ(ｂj)への代入の右辺内に出現しかつｂiからｂjの間ではｘの値が決して変化しないような、ｂiからｂjへの実行経路が存在する場合にのみ、変数ｘがブロックｂi内で生きている変数である、請求項４に記載の方法。
【請求項８】
前記シンボリックイメージ計算の段階は、
関連する変数に対してのみ前記遷移関係を有する変数の集合を制限する段階と、
生きている変数に対してのみ到達可能な状態を有する変数の集合を制限する段階と、
を有する、請求項７に記載の方法。
【請求項９】
遷移関係の前記関連する変数は、対応するブロックの前記代入または条件付き式のいずれかに現れる変数のみを有する、請求項８に記載の方法。
【請求項１０】
前記シンボリックイメージ計算は、reach_frontier戦略を使用する到達可能性分析を有する、請求項１に記載の方法。
【請求項１１】
前記シンボリックイメージ計算は、reach_lockstep戦略を使用する到達可能性分析を有する、請求項１に記載の方法。
【請求項１２】
前記シンボリックイメージ計算は、到達可能性分析を有し、ＢＤＤベースの表現を使用する、請求項１に記載の方法。
【請求項１３】
前記シンボリックイメージ計算は、到達可能性分析を有し、複数のシンボリック表現を使用する、請求項１に記載の方法。
【請求項１４】
前記複数のシンボリック表現は、ＢＤＤ、プレスバーガーの式、及び実領域内の線型制約条件を含む、請求項１３に記載の方法。
【請求項１５】
前記離接分解する段階は、ハイパーグラフ分割の使用によって、ソフトウェアモデルを分解する段階をさらに有する、請求項２に記載の方法。
【請求項１６】
ハイパーグラフ分割の使用によって、任意の複数の分割の間で共有される前記生きている変数の数を極小化する段階をさらに有する、請求項１５に記載の方法。
【請求項１７】
ハイパーグラフ分割の使用によって、任意の複数の分割の間で共有される前記割り当てられた変数の数を極小化する段階をさらに有する、請求項１５に記載の方法。
【請求項１８】
ハイパーグラフ分割の使用によって、複数の異なる分割内のブロックの間の前記遷移の数を極小化する段階をさらに有する、請求項１５に記載の方法。
【請求項１９】
前記シンボリックイメージ計算は、
関連する変数に対してのみ前記遷移関係を有するプログラム変数の集合を制限する段階と、
生きている変数に対してのみ前記到達可能な状態を有するプログラム変数の集合を制限する段階と、
を有する、請求項２に記載の方法。
【請求項２０】
前記到達可能性分析は、reach_frontier戦略を使用する、請求項２に記載の方法。
【請求項２１】
前記到達可能性分析は、reach_lockstep戦略を使用する、請求項２に記載の方法。
【請求項２２】
前記シンボリックイメージ分析は、到達可能性分析を有し、ＢＤＤベースの表現を使用する、請求項２に記載の方法。
【請求項２３】
前記シンボリックイメージ分析は、到達可能性分析を有し、複数のシンボリック表現を使用する、請求項２に記載の方法。
【請求項２４】
前記複数のシンボリック表現は、ＢＤＤ、プレスバーガーの式、及び実領域内の線型制約条件を含む、請求項２３に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、一般に、コンピュータソフトウェア検証の分野に関し、特にコンピュータソフトウェアのモデル検査の離接的(disjunctive)方法に関する。
【背景技術】
【０００２】
モデル検査(model checking)は、利用者により指定された性質を有限状態モデルが満足させることを証明するための正式な方法である。二分決定グラフ（ＢＤＤ；Binary Decision Diagram）及びブーリアン充足可能性ソルバ（Boolean Satisfiability Solver；ＳＡＴ）に基づくシンボリック状態空間走査アルゴリズムの発展の結果として、モデル検査は、ハードウェア検証のための有効な技術として広く認められるようになった。しかし、その有用性はハードウェアに限定されず、したがってモデル検査は、特に（例えば、SystemCでの）トランザクションレベルのシステム設計や埋め込みソフトウェア（例えば、C/C++）で、ソフトウェア検証のためにも使用されつつある。
【０００３】
当業者には公知のように、モデル検査方法に関連する複雑さは、使用される特定のモデルの状態変数（すなわちメモリ要素）の数に関して一般に指数関数的に増加する、モデル化される状態空間のサイズに依存する。この指数関数的な依存性は、この技術分野において記憶量「爆発」(memory "blow up")として公知のものを、容易に引き起こすおそれがある。これは、比較的大きなシステムに対してモデル検査を適用する場合に克服すべき主要な障害である。
【０００４】
指数関数的な依存性ならびに結果として生ずるメモリ爆発に部分的に対処した１つの方法は、ＢＤＤの使用である。ＢＤＤベースのシンボリックモデル検査は、K. McMillanによって、1993年にKluwerにより出版された「Symbolic Model Checking（シンボリックモデル検査）」と題する書籍により最初に説明された。F. Ivancic, I. Shlyakhter, A. Gupta, M. K. Ganai, V. Kahlon, C. Wang and Z. Yangによって、「Model Checking C Program Using F-Soft（F-Softを使用するモデル検査Ｃプログラム）」と題するProceedings of IEEE International Conference on Computer Design, 2005の論文において説明されたように、ＢＤＤベースのシンボリックモデル検査は、ブール関数における状態の集合を表すシンボリックグラフアルゴリズムを使用することにより、状態空間をシンボリックに詳しく考察する。したがって、それらの複雑さは、状態の数の代わりにＢＤＤ表現のサイズに依存する。またシンボリックモデル検査は、より大きなモデルを効率的に管理することが可能であるが、前述の爆発(blow-up)問題の影響を受けることも同様である。
【０００５】
結果として、形式検証の研究者は、このＢＤＤ爆発を避けるヒューリスティックな（発見的な）手法を探索した。このような手法の１つは、イメージ計算を行う効率的なアルゴリズム、すなわちシンボリックモデル検査における基本計算を含んでおり、これは特にハードウェアモデルに対して広範囲に研究され調査されている（例えば、O. Coudert et al., "Verification of Sequential Machines Based on Symbolic Execution（シンボリック実行に基づく順序機械の検証）," in Automatic Verification Methods for Finite State Systems（有限状態システムに対する自動検証方法）, J. Sifakis, ed., pp. 365-373, Springer-Verlag, 1989を参照）。
【０００６】
しかし、ソフトウェアモデルは、既存のモデルチェッカの適用を著しく困難にするいくつかの独自の特徴を示す。第１に、ソフトウェアモデルにおける状態変数（すなわちメモリ要素）の数は、ハードウェアモデルで見られるものよりもはるかに多い。さらに、ハードウェアモデルと比較して、ソフトウェアモデルは、通常、はるかに深い順序深度(sequential depth)を有する。したがってビット幅の大きなカウンタを用いなくても、多くの場合、たったの数クロックサイクルで、ハードウェアモデルの任意の状態に到達することができる。しかしながら多くのソフトウェアモデルでは、特定の状態に到達するに要するステップの数は、著しく大きい可能性がある。したがって従来のＢＤＤベースのモデル検査アルゴリズムは、ソフトウェアモデルでは、特によく機能を発揮するわけではない（例えば、S. Edwards et al., "Using A Hardware Model Checker To Verify Software（ソフトウェアを検証するためのハードウェアモデルチェッカの使用）," Proceedings of the 4th International Converence on ASIC (ASICON '01), IEEE, October 2001を参照）。
【発明の開示】
【発明が解決しようとする課題】
【０００７】
結果として、ソフトウェアモデルに対してより直接的に適用可能なモデル検査の新しい手法が、この技術分野における著しい進歩を意味するであろう。このような手法が、本発明の主題である。
【課題を解決するための手段】
【０００８】
本発明の原理によって、ソフトウェアモデルに特有の多数の特徴を利用する、ソフトウェアモデルのためのＢＤＤベースの離接イメージ計算(disjunctive image computation)方法が開発された。
【０００９】
詳しくは、また本発明の方法によれば、ソフトウェアモデルの全体がサブモジュールの離接集合に分解され、それに対して遷移関係の別の集合が作製される。イメージ／到達可能性分析が実行され、元のイメージ計算は、すべての他のサブモジュールから独立して個々のサブモジュールに対して実行可能な、イメージ計算ステップの集合に分割される。
【００１０】
都合の良いことに、本発明の方法は、元のモデルをサブモジュールに分解する間に、変数の局所性を利用する。各サブモジュールの遷移関係内の生きている変数(live variable)の数は劇的に減少し、イメージ計算の性能の著しい改善をもたらす。この分解を多方向ハイパーグラフ(hypergraph)分割(partition)問題として定式化することにより、サブモジュールの小さい集合を有利に作製し、同時に各個別のサブモジュール内の生きている変数の数を極小化する。
【００１１】
従来技術とは著しく異なり、従来技術では必要とされるような連接(conjunctive)遷移関係を作製せずに、本発明の方法は、ソフトウェアモデルから直接に離接遷移関係の集合を作製する。本発明の方法は、生きている変数の排他使用を用いて、元のモデルをサブモジュールの集合に分解する。さらに本発明の方法は、この方法にさらなる利益をもたらす、いくつかの新規な境界(frontier)及びロックステップ(lockstep)シンボリック探索戦略を応用する。
【００１２】
本発明のより完全な理解は、添付図面を参照することによって実現される。
【発明を実施するための最良の形態】
【００１３】
本発明による方法を論じるに当たって、ハードウェアには備えられていないいくつかの有用な特徴を順序ソフトウェアは有することが指摘される。第１に、ソフトウェアにおけるプログラム変数は、多くの場合、より高度の局所性(locality)を示す。特に、多くの変数は、局所変数として定義されるか、あるいは全体のプログラムの一部においてのみ有効である。この局所性情報は、ソースコード内で利用できるから、検索が比較的容易である。さらにソフトウェアと組み合わされた状態遷移は、事実上、順序的(sequential)である。すなわちプログラムの任意の点において、非常に限定された数の状態変数のみが、その値を変更することができる。他方、ハードウェア内の変数は同時に更新され、これは、変数の値が他から独立して更新されることは、まれにしかあり得ないことを意味する。都合の良いことに、本発明による方法は、ソフトウェアのこれらの特徴を利用する。
【００１４】
図１は、本発明の方法に関連する段階を表す高レベルのフローチャートである。特に、ソフトウェアモデル１１０は、変数の局所性を最大化するために、ハイパーグラフ分割を使用して、離接分解される（１２０）。次に、遷移関係の集合（１３０）が、何らの連接的な中間段階なしに、直接組み立てられる。最後に、必要な計算を有利に加速するために、ＢＤＤと複数のシンボリック表現、変数のライブスコープ（生きている範囲；variable live scope）、境界及びロックステップ分析(frontier and lockstep analysis)のような高度な技術を使用して、イメージ／到達可能性分析が実行される（１４０）。
【００１５】
［ソフトウェアモデル検査］
しかし本発明の方法の動作を理解するために、まず本発明における検証モデルがソフトウェアプログラムからどのように組み立てられるかを説明し、次に、ソフトウェアモデルと、使用されるシンボリックモデル検査アルゴリズムとを正式に定義しなければならない。
【００１６】
ソフトウェアモデル：
本発明のソフトウェアモデル化方法によれば、（この例ではＣプログラミング言語で記述されている）プログラムは、あらゆる複雑な制御構造と式を除去するために、最初に前処理される。このような前処理には、副作用を有するステートメントを副作用のない等価なステートメントに書き直すことと、エイリアシングを介してポインタと配列とを等価な単純な変数の集合で置換することを含んでいる。さらに変数もリネーム（変名）されて、その結果、変数の名前はプログラム全体を通じて一意のものとなる。最後に、プログラム内に再帰的なデータ構造が存在すれば、利用者により指定される限界に到るまで、それらは平滑(flattened out)にされる。前処理が完了した後、ソフトウェアプログラムは、整数(integer)／文字(char)型の単純な変数のみを含んでいる。この時点で、本実施形態の現在の実装が浮動小数点算術演算を無視していることが指摘されるが、本発明はそのように限定されるものではない。
【００１７】
ＢＤＤが基本的なシンボリック表現(symbolic representation)として使用される場合、プログラム内の各単純な変数は、次に二進状態変数の集合により符号化される。特定のプログラム変数を符号化するために必要なビットの数は、変数の範囲に依存する。例えば、何らかの種類の範囲分析の適用により変数の範囲が評価されない限り、整数変数は３２ビットを必要とし、他方、文字変数は８ビットだけを必要とするであろう。これらのプログラム変数に加えて、プログラムの位置、すなわち、プログラムカウンタの値を符号化するために、二値変数の集合が作られる。整数算術演算は、予め定義された論理ブロック（例えば加算器や乗算器）をインスタンス生成することにより変換される。
【００１８】
変数の符号化に引き続いて、プログラムの制御フローグラフ(control flow graph)が構築され、制御フローグラフから検証モデルが構築される。制御フローグラフにおいて、ステートメントは基本ブロック(basic block)に分類され、基本ブロックのそれぞれは、複数のステートメントを有してもよい。都合のよいことに、同じ基本ブロック内のすべてのステートメントが並列に実行可能であるように、基本ブロックが構築される。
【００１９】
重要なことに、（それぞれの個別のステートメントに対してではなく）それぞれの基本ブロックに対して、プログラムカウンタの値が、１つだけ割り当てられる。したがって、シンボリック探索の間に経験する順序深度は減少する。この符号化方式の結果として、有限モデルは、二進状態変数の集合とそれらに対応する次の状態の関数とに関して暗黙的に表現される。
【００２０】
次の状態の関数を作るために、最初に、制御フローグラフを状態遷移表として表す。このような表の例が図２に示されている。ここで、Ｐ＝｛ｐ1，ｐ2，ｐ3｝はプログラムカウンタ（ＰＣ）変数の現在の値を表し、Ｑ＝｛ｑ1，ｑ2，ｑ3｝は次の状態の値を表す。列「ガード(guard)」は、基本ブロックの間の遷移が行われる状態を含む。図２に示すこの例においては、プログラムは、（二進符号化が000bである）ブロック０に始まる。式（ｘ＝＝５）が真であると評価されれば、プログラムはブロック１（001b）に進み、他の場合には、プログラムはブロック４（100b）に進む。この表に基づいて、それぞれ、δq1，δq2，δq3と表されるＰＣ変数の次の状態の関数は、次式で与えられる。
【００２１】
【数１】
2009505227.tif 000002
【００２２】
ここで、（Ｐ≡０）は、Ｐが０と評価されることを意味し、その等価なブーリアン式は次式で与えられる：
【００２３】
【数２】
2009505227.tif 000003
【００２４】
プログラム変数の次の状態の関数は、類似の方法で構築される。例えばｘiは、ブロック１と５の中でのみ、それぞれ、ｅｘｐｒ1とｅｘｐｒ5に割り当てられると仮定する。δyi（ここでｙiは対応する次の状態の変数である）により示されるｘiの次の状態は、次式で与えられる。
【００２５】
【数３】
2009505227.tif 000004
【００２６】
すなわちｘiの値は、それが明示的に割り当てられていないブロック内で変化しないままであるべきである。次の状態の変数が｛ｙ1，ｙ2，…，ｙN｝であるプログラム変数の全体の集合を示すためにＸ＝｛ｘ1，ｘ2，…，ｘN｝を使用すれば、ｘiに対する次の状態の関数の構造は、二進状態変数の次の状態の論理を示す図３により示される。
【００２７】
図３を参照すれば、δyiはｘiの次の状態の関数を示すことが判る。ＭＵＸは、制御信号が（Ｐ≡ｊ）であるように設定された場合にマルチプレクサの出力がｅi,j(Ｘ)に等しいような、マルチプレクサである。
【００２８】
これを定式化するために、本実施形態のモデルを次のように表す。（１）現在の状態のプログラム変数Ｘ＝｛ｘ1，ｘ2，…，ｘN｝の集合、及び現在の状態のＰＣ変数Ｐ＝｛ｐ1，ｐ2，…ＰM｝の集合；並びに、（２）次の状態のプログラム変数Ｙ＝｛ｙ1，ｙ2，…，ＹN｝の集合、及び次の状態ＰＣ変数Ｑ＝｛ｑ1，ｑ2，…，ｑM｝の集合。ＰＣ値が整数ｊ∈｛１，２，…，Ｋ｝であるとし、ｅi,j(Ｘ)をブロックｊ内でｘiに割り当てられる式であるとすれば、次のようになる
【００２９】
【数４】
2009505227.tif 000005
【００３０】
［シンボリックモデル検査］
シンボリックモデル検査において、モデルの状態遷移グラフは（Ｔ，Ｉ）によってシンボリックに表され、ここで、Ｔ(Ｘ，Ｐ，Ｙ，Ｑ)は遷移関係の特性関数であり、Ｉ(Ｘ，Ｐ)は初期状態述語(initial state predicate)である。
【００３１】
【数５】
2009505227.tif 000006
【００３２】
を、それぞれ、Ｘ，Ｐ，Ｙ，Ｑの付値(valuation)であるとする。現在の状態の変数の付値が
【００３３】
【数６】
2009505227.tif 000007
【００３４】
を真にすれば、対応する状態
【００３５】
【数７】
2009505227.tif 000008
【００３６】
は初期状態である。同様に、
【００３７】
【数８】
2009505227.tif 000009
【００３８】
は、状態
【００３９】
【数９】
2009505227.tif 000010
【００４０】
から状態
【００４１】
【数１０】
2009505227.tif 000011
【００４２】
への遷移がある場合にのみ、真である。なお、遷移関係と状態の集合は、ともにブール関数により表され、そのブール関数はＢＤＤにより表される。
【００４３】
Ｔ(Ｘ，Ｐ，Ｙ，Ｑ)は、すべての遷移ビット関係(transition bit-relation)の連接であるから、
【００４４】
【数１１】
2009505227.tif 000012
【００４５】
ここで、Ｔyiはプログラム変数に対するビット関係であり、ＴqiはＰＣ変数に対するビット関係である。ビット関係は次のように定義されることが指摘される。
【００４６】
【数１２】
2009505227.tif 000013
【００４７】
本発明の手法の多くは、到達可能性の性質、例えば、あるプログラムの位置が到達可能であるか否かを検査することを含んでいる。これらの到達可能性の性質は、到達可能性分析として知られている処理によって調べられる。
【００４８】
当業者は十分理解できるように、到達可能な状態は、初期状態から始めて、既に到達している状態のイメージに繰り返して加算することにより、〈Ｔ，Ｉ〉によってシンボリックに計算可能である。状態の集合Ｄのイメージであってグラフ内のＤの後続値のすべてを含むイメージは、ＥＸTＤにより示される。次に、到達可能性分析は、次式により表される不動点(fix-point)計算に定式化される。
【００４９】
【数１３】
2009505227.tif 000014
【００５０】
ここで、μＺは最小不動点を表し、Ｚは補助反復変数である。すなわち、結果が成長を停止するまで既に到達している状態の後続値に繰り返して加算したときに到達する点である。
【００５１】
次に、Ｄのイメージは以下のように計算される。
【００５２】
【数１４】
2009505227.tif 000015
【００５３】
Ｔは多くのビット関係の連接であるから、イメージ計算は、一連の結合定量化(conjoin-quantify)演算を含んでいる。これらの演算の順序が異なると、中間産出物(intermediate product)に対して、非常に異なるピークＢＤＤサイズがもたらされるおそれがある。ピーク時のメモリ使用量を低く維持するようにこれらの演算を順序付けることは、定量化スケジューリング問題(quantification scheduling problem)とも呼ばれ、多くの研究の中心であり、成熟した方法に加えて多数のヒューリスティックな手法が公に利用可能であり、当業者には公知である。
【００５４】
［離接イメージ計算］
残念ながら、これまでに概略を説明したソフトウェアモデル検査の単純な実装例は、実際には、良く能力を発揮しない。これを検証するために、埋め込みソフトウェアプログラムのための検証モデルを構築した。ＰＰＰ（ポイント・ツー・ポイント・プロトコル；Point-to-Point Protocol）と呼ばれる本実施形態でのモデルは、それに適用されるＶＩＳにおいて古典的なシンボリック到達可能性分析を有する。特に、有限状態モデルは、１４３５の二進状態変数を有する。
【００５５】
図４は、この検証モデルから収集されたデータを示す。図４には、各ＢＦＳ（幅優先探索；Breadth-First Search）ステップを表す３つの曲線が示されている。１）生きている(live)ＢＤＤノードのピーク数、２）到達可能な状態に対するＢＤＤサイズ、３）中間産出物に対する最大ＢＤＤサイズ。これらの中で、第１の値は全メモリ使用量を表す。
【００５６】
図４の曲線は、ソフトウェアモデルに対して従来のシンボリックモデル検査技術を適用した場合の代表的なものである。図４にプロットされたすべての３つの指標は、ＢＦＳステップとともに指数関数的に増加しており、到達可能性分析が継続するにつれて、到達可能な状態に対するＢＤＤのサイズが急速に増加することを示している。ソフトウェアモデル内のプログラム変数が多いために、このような指数関数的な増加は、メインメモリを急速に使い果たすおそれがあることを、当業者は十分に理解している。当然ながら、ＢＤＤ演算の複雑さはＢＤＤのサイズに依存するので、ＣＰＵ時間も同様に増加する。結果として生ずるメモリ量爆発を軽減するために、遷移関係と到達可能な状態の両方を減少させなければならない。
【００５７】
遷移関係の離接分割された表現がＢＤＤサイズを減少させることが可能であることが、当業者には一般的に知られている（例えば、J. Burch, "Using BDD's To Verify Multipliers（乗算器を検証するためのＢＤＤの使用）," in 1991 International Workshop on Formal Methods In VLSI Design, Miami, FL, Jan. 1991を参照）。しかし残念ながらこのような方法は、各処理が原子分割(atomic partition)として処理される非同期システムにのみ適用できる。
【００５８】
当業者は容易に理解できるように、離接分割の計算は、非自明(non-trival)な課題である。しかし幸いにも、順序プログラムに対しては、次の状態の関数の自然分解(natural decomposition)が存在する。なお、図３において、δyiは式の集合の和集合であり、その中の１つのみが任意のプログラムの位置においてアクティブである。したがって、同様な方法で遷移関係Ｔを離接成分の和集合に分解できれば、コストを要するイメージ計算は、より安価なイメージ計算の集まりに分割可能である。この結果は、存在量化(existential quantification)が∨（しかし∧ではない）の中に分布している事実に起因しており、したがって、個別のイメージサブセットは、孤立した小さい遷移関係成分(transition relation component)を使用して計算可能である。また、個々のイメージサブセットは、計算がより容易であるから、イメージ計算を通じてのピーク時のメモリ使用量は、好都合に減少する。
【００５９】
変換関係(translation relation)の分解：
前述の次の状態の関数の作成によれば、
【００６０】
【数１５】
2009505227.tif 000016
【００６１】
である。ここで、（ｊ／Ｐ）は整数ｊでＰを置換することを表す。同様に、ｆ(Ｘ／Ｙ)は、関数ｆ内においてＹ変数のすべてをＸ変数で置換することを示すために使用される。なお実際には、ｅi,j(Ｘ)は、（Ｐ≡ｊ）に関してδi(Ｘ，Ｐ)の余因数(cofactor)である。
【００６２】
（Ｐ≡ｊ）に関してｆの余因数を(ｆ)(P≡j)により示せば、遷移ビット関係の余因数は、次式で与えられる。
【００６３】
【数１６】
2009505227.tif 000017
【００６４】
全体の遷移関係Ｔ(Ｘ，Ｐ，Ｙ，Ｑ)は、次のように離接分解可能である。
【００６５】
【数１７】
2009505227.tif 000018
【００６６】
すなわち、個々の遷移関係選言肢(transition relation disjunct)は次式で与えられる。
【００６７】
【数１８】
2009505227.tif 000019
【００６８】
存在量化を∨の中に分配することにより、
【００６９】
【数１９】
2009505227.tif 000020
【００７０】
を得る。
【００７１】
実際には（基本ブロックの数は何千にもなり得るので）、すべての個々の基本ブロックに対して遷移関係選言肢を作ることはできない。基本ブロックは、より大きい遷移関係選言肢の集合を形成するために、ヒューリスティックに混合される。同時に、離接分解の利点はできるだけ多く維持されなければならない。
【００７２】
なお、(Ｔ)(P≡j)及び(Ｔyi)(P≡j)は、Ｔ及びＴyiを最初に構築することなしに、ソフトウェアモデルから直接構築される。基本ブロックが、より大きいクラスタに分類される場合、サブモジュール（｛Ｔi｝）に対する離接遷移関係も（各ブロックに対してそれらを構築し、次に混合する代わりに）直接構築される。それを行うためには、各々のクラスタ（あるいはサブモジュール）、対応する基本ブロック、及びすべてのプログラム変数ｘiに対する対応するｅi,jを識別する必要があるのみである。なお、遷移関係選言肢Ｔi自体もＢＤＤの連接として表すことが可能である。
【００７３】
離接遷移関係を構築するこの方法は、従来技術による方法とは異なっている。詳しくは、S. Barner and I. Rabinovitz, "Efficient symbolic model checking of software using partial disjunctive partitioning（部分的な離接分割を使用するソフトウェアの効率的なシンボリックモデル検査）," in the 2003 Correct Hardware Design and Verification Methods Converenceに述べられているような従来技術の手法では、１つの遷移関係選言肢が、既存の連接遷移関係に基づいて、各プログラム変数に対して構築される。
【００７４】
この従来技術の手法は、最初にＴyiを作ることを必要とし、定量化演算に依存するので、その構築自体の計算コストがかさむおそれがある。さらに、分割は、多くの場合にプログラムの異なる部分に分散したステートメントを含み、それは変数の局所性の利用を困難にする。本明細書では、後で、変数の局所性なしで、到達可能な状態のＢＤＤ表現が著しく大きくなり、かつ有限状態モデルの順序深度がより長くなる可能性があることを説明する。
【００７５】
到達可能な状態の分解：
到達可能な状態は、多くの到達可能な状態のサブセットの和集合としても離接的に表現できる、特に、それぞれのサブモジュールに対して１つずつ、
【００７６】
【数２０】
2009505227.tif 000021
【００７７】
のようにも表現できる。
【００７８】
到達可能な状態の分割された表現の下では、イメージ計算の結果は、すべての到達可能性ステップにおいて、図５に疑似コードで示すように、再分配される必要がある。ここで図５を参照すると、Ｒiはブロックｉに関連する到達可能な状態のサブセットを表し、Ｔiはその遷移関係を表し、ｉｍｇは、連接分割された遷移関係に対する標準的なイメージ計算手順を表している。
【００７９】
Ｋ個の離接サブモジュールとＫ個の到達可能なサブセットを仮定すると、各到達可能性ステップにおける標準的なイメージ計算の数は、最大でＫである。さらに、結果はすべてのサブモジュールに再分配されなければならず、再分配に費やされる努力はＯ(Ｋ2)である。制御フロー構造に基づくこのアルゴリズムの最適化は、再分配の複雑さをＯ(Ｅ)とすることができる。ここでＥは、制御フローグラフのエッジの数である。
【００８０】
基本ブロックが混合（マージ）される場合、到達可能な状態のサブセットも混合されるべきである。それにもかかわらず、結果として生ずるより大きいサブセットは、離接分割のままである。モノリシックなＢＤＤと比較して、この分割された表現は、総合的なＢＤＤサイズを大幅に減少させる可能性がある。
【００８１】
都合の良いことに、この離接イメージ計算アルゴリズムを実現する際に、２つの異なる手法がある。第１の手法では、すべての遷移関係は、（それらの到達可能なサブセットと同様に）同じＢＤＤ変数の順序にしたがう。この場合、単一のＢＤＤマネージャが、すべてのＢＤＤを保持するために割り当てられる。あるいは、異なるＢＤＤ変数の順序を異なるサブモジュールに対して（それらの個々の遷移関係と到達可能な状態のサブセットを構築するために）、使用できる。この場合に、別々のＢＤＤマネージャが、それぞれの離接サブモジュールに対して割り当てられる。
【００８２】
複数のＢＤＤマネージャを使用して、異なるＢＤＤに対して異なる変数順序を有することにより、ＢＤＤサイズをより小さく維持することができる。これは、好都合にも、このイメージ計算のメモリ消費量をはるかに少なくすることを可能にし、計算を加速する可能性がある。しかし、新しい到達可能な状態を伝搬する間に、異なるマネージャの間でＢＤＤを転送する必要がある。これは、１つのＢＤＤに対してよい順序は別のＢＤＤに対しては極端に悪いことがあるので、問題を生じるおそれがある。したがって、動的な変数の再順序付け(dynamic variable reordering)が転送処理の間に起動することがある。
【００８３】
当業者は十分理解できるように、頻繁な再順序付けはＣＰＵ時間を多く費やすおそれもある。この意味で、複数のマネージャに基づく方法は、実際には、ＣＰＵ時間とメモリとのドレードオフの関係にある。単一のＢＤＤマネージャに基づく方法と複数のＢＤＤマネージャに基づく方法をともに実現した。
【００８４】
図４は、分割された到達可能なサブセットを用いて到達可能性分析を行う手順を示している。図４に示される手順は、到達可能な状態を１フレームずつ（ＦＢＦ；Frame-By-Frame）計算する。あるいは到達可能性分析は、１マシーンずつ（ＭＢＭ；Machine-By-Machine）実行することも可能である。すなわち、１つの個別のサブモジュールに対してそれが収束するまで分析は実行され、その後、結果が他のサブモジュールに伝搬される。この処理は、いずれのサブモジュールにおいても新しい状態が発見されないようになるまで、反復される。ＭＢＭ分析の利点は、異なるサブモジュールの間でのトラフィック（データ転送）を極小化することである。したがってこの方法は、分散形態での実装が用いられている場合には、魅力的である。都合の良いことに、従来技術のＡＲＣＥアルゴリズムとは極めて対照的に、本実施形態の到達可能性分析の結果は常に正確である。
【００８５】
変数の局所性を用いた簡略化：
次に、無関係な変数の早期の定量化と、変数のライブスコープ(variable live scope)の使用とが、どのように到達可能な状態のサブセットを単純化することができるかを説明する。
【００８６】
定義１：  ＸRjと記される、ブロックｊに関して関連する変数の集合は、ブロックｊに現れる変数を（代入文であるいは条件付きの式で）含む。
【００８７】
他方、集合ＸIj＝Ｘ＼ＸRjは、ブロックｊとは無関係の変数を表す。各基本ブロックに現れるプログラム変数の数が少ない可能性があるが、その遷移関係選言肢は、常に、モデルのすべての状態変数を常に含んでいる。なぜならば、
【００８８】
【数２１】
2009505227.tif 000022
【００８９】
【数２２】
2009505227.tif 000023
【００９０】
であるからである。
【００９１】
ブロックｊの中にはない変数に対しては、ｘiの値が変化しないことを確実にするために、ビット関係(Ｔ)(P≡j)は
【００９２】
【数２３】
2009505227.tif 000024
【００９３】
に還元(reduce)される。ブール関数
【００９４】
【数２４】
2009505227.tif 000025
【００９５】
は、２つの変数と１つのＸＯＲ演算子を含み、したがって３つのノードを有するＢＤＤにより表現できる。
【００９６】
しかし、これらのＢＤＤの多数を一緒に結合させる(conjoin)ことは、大きなＢＤＤを作るおそれがある。悪い変数順序が使用される場合、ＸＯＲ演算子は、指数関数的な数のノードを有するＢＤＤを作るおぞれがある。他方、これらのＸＯＲ演算子に対する良い順序は、イメージ計算及び到達可能性分析の間に遭遇する他のＢＤＤには良くないおそれがある。
【００９７】
詳細に観察すると、無関係の変数は、イメージ計算の間に早期に数量化できることが判る。そうすることによって、∃ＸＤ(Ｘ，ｊ／Ｐ)∧(Ｔ)(P≡j)は次のように単純化できる。
【００９８】
【数２５】
2009505227.tif 000026
【００９９】
ＸIjの早期の定量化は、これらの現在の状態の変数を対応する次の状態の変数に置き換えることと同じ効果を有する。しかし、早期の定量化の利点は、(Ｔ)(P≡j)を最初に作る必要がないことである。代わりに、より簡単なバージョンが使用される。定量化の間のＢＤＤ爆発の可能性も避けられる。したがって実装にあたっては、これらの無関係の変数に対する早期の定量化の代わりに、ここでは変数の置き換えを使用する。実験的な研究は、これが明らかにより良い選択であることを示している。
【０１００】
生きている変数(Live Variables)：
離接分解と、無関係の変数の早期の定量化とは、遷移関係ならびにイメージ計算における中間産出物の単純化が目的である。しかしながら、到達可能な状態のサブセットのＢＤＤは、依然として非常に大きい可能性がある。離接分割を使用してもなお、すべてのプログラム変数が到達可能な状態のサブセットに依然として現れる可能性があり、コンパクトなＢＤＤの発見をますます困難にすることに注目されたい（実際、これは、図４に示す指数関数的な増大の主な理由である）。
【０１０１】
しかし、多くのプログラム変数はプログラムのある部分（セグメント）でのみ使用され、これらの変数の値は、それらの範囲（スコープ）外では無意味である。これは、ハードウェアモデルで使用されその値がクロックサイクルごとに同時に更新される状態変数とは異なっている。この「変数の局所性」が図６に示す例によって示されている。図６において、ａとｂは局所変数として定義され、ｘ；ｙ，ｚは大域変数である。
【０１０２】
図６に示すこのブロックからプログラムが出た後、ａとｂが現在有するいかなる値も無意味であり、それらは制御フローとデータ経路のいずれもに影響を与えない。しかし、それらの値が継続されれば、それらはブール関数として表現されなければならない。これは、到達可能な状態のＢＤＤ表現を不必要に大きくする。
【０１０３】
幸いにも、その値が保持されるべきである基本ブロックの集合として定義されたある変数のライブスコープ(live scope)は、ソースコードから直接収集できる。例えば、任意の局所的に定義された変数は、それが定義された関数／ブロックの中でのみ有効である。しかし、しばしば大域変数ですら限定された数のブロックの中でのみ使用されるように、このようなスコープ(scope)は、多くの場合に十分に正確ではない。
【０１０４】
したがって、プログラムの実行がその（変数の）値から独立になるときは、大域変数ですら、それらのライブスコープの範囲外とみなされるべきである。例えば図６において、大域変数ｘが上の２つのブロックにのみ出現するならば、これら以外の他のすべてブロックでは、生きていない(dead)であるとみなされるべきである。結果として、このような場合において真に大域変数のみが、それらの値がすべてのブロックで必要であるので、ＰＣ変数である。
【０１０５】
変数がもはや必要とされなければ、到達可能な状態からそれらの値は直ちに除去されるべきであるから、ライブスコープは、到達可能な状態のサブセットを単純化するために使用できる。したがって、この集合に属さない変数は、到達可能なサブセットから存在量化されるべきである。生きていない変数(dead variable)の除外は、新しい到達可能な状態（図５）の再分配の間に実現できる。新しい到達可能な状態が特定のサブモジュールに分配される前に、そのサブモジュール内の生きていないすべての変数は、存在量化される。本発明の目的に関し、変数のライブスコープの正式な定義は以下のように与えられる。
【０１０６】
定義２：  ｘiの値が使用されるブロックｊからブロックｋへの経路が存在する場合にのみ、ブロックｊは変数ｘiのライブスコープの中にある。
【０１０７】
プログラム変数ｘiに対してそのライブスコープは、制御フローグラフを逆方向に詳しく調べることにより発見することができる。まず、ｘiの値が使用されるすべてのブロックを探索する（すなわち、代入文の右辺中、あるいは条件付きの式中のいずれかで）。次に、ｘiの値が変化したブロックに到達するまで、これらのブロックから再帰的に遡る。都合の良いことに、この技術は、大域的に定義された変数と局所的に定義された変数の両方に対して十分に一般的である。
【０１０８】
Ｋをブロックの数であるとし、Ｅをエッジの数であるとし、Ｎを状態変数の数であるとすれば、すべての変数に対してライブスコープを計算する複雑さは、Ｏ((Ｋ＋Ｅ)×Ｎ)により表すことができる。特別の利点は、シンボリックモデル検査と比較して、オーバーヘッドを無視できることである。さらに別の利点が、ライブスコープを計算するアルゴリズムが制御フロー分析で多くの場合に使用されるものであって、したがってよく理解されるものであるという事実で実感される。
【０１０９】
到達可能性の不動点(Reachability Fixpoint)の早い収束：
到達可能なサブセットから、変数のライブスコープ外にあるそれらの変数を除去することは、ＢＤＤサイズを小さくするのみではなく、到達可能性の不動点計算を速く収束させる可能性がある故に、重要である。
【０１１０】
図８に示すＣコードセグメントを例とする。ここで、各ステートメントは基本ブロックであり、すべての変数は大域変数と定義されていると仮定する。変数ｘとｙがプログラム中の他のどこにも使用されていなければ、上述の小節における分析アウトラインは、ｘがＬ３でのみライブ(live)であり、ｙはＬ５でのみライブであることを示す。この情報を考慮すれば、Ｌ１からＬ６までを１回だけ行った後で、到達可能性分析の終了を宣言することができる。
【０１１１】
都合の良いことに、これは、Ｌ６、（Ｐ≡２∧Ｓ≡８）の後に発見される状態が、既に（Ｐ≡２）により包含されるからである。しかし、ｘとｙが大域的にライブであると仮定すれば、到達可能性分析は、１回目の通過の後に収束することはできない。Ｌ６の後に、以前に状態は（Ｐ≡２∧ｘ≡０∧ｙ≡０）であったので、状態（Ｐ≡２∧ｘ≡７∧ｙ≡８∧ｓ≡８）は、既に到達している状態によって包含されない。結果として、到達可能性分析は、収束するまでにさらに２つのステップを必要とする。
【０１１２】
各々の離接サブモジュールに対して生きていない変数を識別し、それらを到達可能な状態のサブセットから除去することにより、実際にイメージ計算に関係するＢＤＤ変数を大幅に減少することが可能である。これは、よりコンパクトなＢＤＤ、より速いイメージ計算、及び、到達可能性分析の早期終了の可能性に変換される。
【０１１３】
離接分割の創出：
ここで、基本ブロックの全体の集合を離接サブセットにどのように分類するべきかを説明する。原則として、別々な遷移関係を、個別の基本ブロックの各々に対して作ることができる。実際にこの手法は、生きていない変数、及び無関係の変数の数を最大化する。しかしながら、実際に遭遇する基本ブロックが多数であるために、この最大化が妨げられる。その代わりに、基本ブロックがより大きいグループに混合（マージ）され、その各々に対して遷移関係が作られる。
【０１１４】
理想的には、できる限り少数のグループを作り、同時に変数の局所性の利点を維持することが望ましい。多方向ハイパーグラフ分割問題を定式化することにより、この目標は実現できる。すなわち、再帰的な二分割が実行される基本ブロックから始めて、すべての基本ブロックは最初にまとめて分類される。サブセットのコストが所定のしきい値未満に低下すると二分割が停止するように、コスト関数を定義しておく必要がある。各々個別の遷移関係をできる限り小さく維持したいから、遷移関係選言肢の実際のＢＤＤサイズは理想的なコスト関数である。しかし、すへての個別の基本ブロックに対して遷移関係を作り、次にそれらの混合を開始することは、コストがかかりすぎる。したがって代案でありながら、グループの遷移関係サイズの良い指標が必要とされる。本実施形態においては、関連する変数の総数が、そのような指標として選択される。ＢＤＤのサポート変数(support variable)の数がしばしばそのサイズの良い指標であることが、本発明者らの動機である。
【０１１５】
次に、最適化の判断基準、例えば、何を最適化することを望むか？を定める必要がある。以下のいくつかのものは、よい候補となり得る。
【０１１６】
ｌｉｖｅＶａｒ    共有された生きている変数(live variable)の数、
ａｓｇｎＶａｒ    共有された割り当てられた変数(assigned variable)の数、
ｃｆｇＥｄｇｅ    ＣＦＧ内のエッジの数。
【０１１７】
共有された生きている変数は、両方の分割の中でライブである変数であり、共有された割り当てられた変数は、その値が両方の分割の中で変えられた変数（それらは代入文の左側に出現する）である。なお、より多くの生きていない変数が到達可能な状態のサブセット外に定量化できるので、共有された生きている変数の数が少ないほど、変数の局所性の高い度合いを示すことになる。共有された割り当てられた変数が少ないほど、類似のサポートを有するビット関係が一緒に分類されることを示す。類似のサポート変数を有するＢＤＤの混合は、爆発を起こす原因とはなりにくい。共有されたＣＦＧエッジが少ないほど、異なるサブモジュール間のトラフィックが少ない。２つの分割がＣＦＧエッジにより接続される場合、新しい到達可能な状態が一方から他方へ伝達される必要があることがある。３つの最適化の判断基準のすべては、一般的な多方向ハイパーグラフ分割問題として一様に表現できる。それらは、ハイパーエッジ(hyperedge)が定義される方法のみが異なる。図９に示すように、
ハイパーノード(hypernode)は、個々の基本ブロックに対応し、各ブロックに対して１ノードである；
ハイパーエッジは、プログラム変数あるいはＣＦＧ内のエッジに対応する；
ｌｉｖｅＶａｒ  ｏｎｅ  ｅｄｇｅ（１つのエッジ）は、その変数がライブであるブロックを接続するために、各変数に対して加えられる；
ａｓｇｎＶａｒ  ｏｎｅ  ｅｄｇｅは、その変数が割り当てられたブロックを接続するために、各変数に対して加えられる；
ｃｆｇＥｄｇｅ  ｏｎｅ  ｅｄｇｅは、先頭及び末尾ブロックを接続するために、各ＣＦＧエッジに対して加えられる。
【０１１８】
異なるグループにまたがるハイパーエッジの数が最少となる一方で、各グループのコストが予め定めたしきい値未満であるように、このハイパーグラフの多方向分割を計算することが望まれる。ここでの生きている変数ベースの分割方法は、ＭＬＰ（最短生存期間順列；Minimum Lifetime Permutation）アルゴリズムに類似しているが、異なるアプリケーションのために設計されていることに、注目されたい。結合定量化演算に対してよいスケジュールを計算するように、ＭＬＰは、連接分割された遷移関係の集合に適用される。他方、ここでのアルゴリズムは、個々の離接遷移関係をより大きいクラスタ（サブモジュール）に分類するために、離接分割された遷移関係の集合に適用される。古典的なイメージ計算における定量化スケジュールの影響に類似して、良い離接分割は離接的なイメージ計算の性能に対しても重要であることは、言及する価値がある。
【０１１９】
離接的な方法の実験：
本発明に基づく新しいアルゴリズムを公けに利用可能なシンボリックモデルチェッカＶＩＳ２．０で実装した。シンボリックモデルチェッカＶＩＳ２．０は、ＢＤＤ演算にＣＵＤＤパッケージをデフォルトで使用する。分割ヒューリスティックスは、ｈＭｅＴｉｓハイパーグラフ分割パッケージで実装した。本発明に基づく新しいアルゴリズムと、ＶＩＳ２．０での最良の既知の従来の方法との実験的な比較を行った。制御された実験の目的で、ＶＩＳにおけるイメージ計算に関連するすべてのパラメータは、変化しないように維持された。これは、ＢＤＤ分割方法（境界(frontier)に設定された）、ＢＤＤ分割しきい値（２０００に設定された）、及びイメージクラスタサイズ（５０００に設定された）を含んでいる。基本的な連接スケジューリングアルゴリズムは、ＭＬＰ[16]であった。動的な変数の再順序付け（dynamic variable reordering）は、すべての実験を通じて、デフォルトの再順序付け方法.sift.を用いて実行可能とされた。すべての実験は、２．８ＧＨｚのＸｅｏｎプロセッサと４ＧＢのＲＡＭを備えてRed Hat Linux 7.2を走らせるワークステーション上で実行された。ベンチマークの集合は、ＰＰＰ(Point-to-Point Protocol)、Daisy（デイジー；公開で利用できるファイルシステム）、及びSerial（Linuxのシリアルデバイスドライバ）を含む、代表的な埋め込みソフトウェアである。調査対象の特性には、ロック(lock)／アンロック(unlock)特性、ファイルオープン(fileopen)／ファイルクローズ(fileclose)特性、及び利用者によって指定された(user-specifed)到達可能な特性を含んでいる。
【０１２０】
単純な整数(integer)／文字(char)変数を符号化するのに必要なビット数を減少させるために、範囲分析(range analysis)が適用された。ＢＤＤベースのアルゴリズムの完全な能力を試験するために、述語抽象化(predicate abstraction)なしで検証モデルが生成された。この意味で、本実施形態でのソフトウェアモデルは、（ブール変数のみが許される）ブール型プログラムよりも著しく複雑である。これらのソフトウェアモデルは、さらに、シンボリックモデルチェッカにより直接処理できるハードウェアモデルの大多数よりも著しく大きい。第１に、本発明に基づく新しいアルゴリズムとＰＰＰの例での従来の方法との実験的な比較を示す。
【０１２１】
図１０は、両方の方法に対して各到達可能性ステップにおけるピーク時メモリ使用量を示す。３つの曲線の中で、Oldは従来の方法を表し、Newは単一のＢＤＤ順序を有する本発明に基づく新しい方法を表し、New2は複数のＢＤＤ順序を有する本発明に基づく新しい方法を表す。ｘ軸は異なるＢＦＳステップを表し、ｙ軸は生きている(live)ＢＤＤノードのピーク数を表す。すべての実験は、４時間に設定されたタイムリミットで実行され、その間に、従来の方法は、２３８ステップを完了し、New及びNew2は、それぞれ３２８ステップと２４７ステップとを完了した。曲線中の水平域（プラトー）は、動的な変数の再順序付けが原因である。結果は、本発明に基づく新しい離接的なイメージ計算方法が、ピーク時のメモリ使用量を著しく減少させることを示しており、New及びNew2の両方と比較して、Oldのカーブはずっと深い。ＢＤＤサイズの縮減は、ＣＰＵ時間の縮減にもつながる。New及びNew2の両方は、Oldよりも多くのステップを完了することができる。
【０１２２】
表２は、テストケースでのより大きな集合について、２つの方法の比較を示している。ＰＰＰに加えて、表２は、SerialとDaisyからのモデルも含んでおり、タイムリミットは２時間に設定された。
【０１２３】
列１〜２は、各テストケースに対するモデルの名前と二進状態変数の数を示す。列３は、到達可能性分析が収束する場合の順序深度を示す。どの方法によっても完了することができないテストケースに対しては、最大共通ＢＦＳステップ（すなわち、すべての方法が到達することができるステップ）までの比較も示す。それは括弧内に示す。
【０１２４】
列４〜６は、ＣＰＵ時間を秒単位で比較する。列７〜９は、生きているＢＤＤノードのピーク数を比較する。表２に示される結果は、本発明に基づく新しい方法によって実現した性能改善が著しく、かつ整合性があることを示す。特に、New及びNew2は、ともに著しく速く、かつメモリ消費が少ない。
【０１２５】
本発明に基づく方法によってもたらされるＣＰＵ時間とメモリ使用量の両方の改善は、従来の方法よりも桁違いに良好となることがある。また多くの場合にNew2はNewより遅いが、それにもかかわらず、New2は、表内の最大のテストケースでも、より多くのＢＦＳステップを完了することが可能である。
【０１２６】
表３は、３つの異なる分割ヒューリスティックス、すなわちｌｉｖｅＶａｒ，ａｓｓｉｇｎｅｄＶａｒ及びｃｆｇＥｄｇｅの比較を示す。それらはすべて多方向ハイパーグラフ分割に基づいているが、最適化の判断基準が異なっている。
【０１２７】
到達可能性分析の性能を比較することにより、イメージ計算におけるそれらの効果を評価する。ＣＰＵ時間とピーク時のメモリ使用量とを、それぞれ表３の列２〜４と列５〜７で比較する。さらに列８〜１０は、異なるヒューリスティック手法によって作られた離接分割の数を比較している。すべてのＣＰＵ時間とメモリ使用量のデータは、到達可能性分析が収束した後に比較される。ただしＰＰＰとDaisyだけは２つの例外である（この２つについては、データはステップ２２８とステップ７０で比較された）。これらの実験のタイムリミットは、１時間に設定された。すべての実験は、方法Newを使用して（すなわち単一のＢＤＤ順序を使用して）、また１７５に設定された分割しきい値（すなわち、生きている変数の最大数）を使用して、１時間のタイムリミットで行われた。
【０１２８】
方法New2は、表３に類似した結果の表を生成する。表３に示される結果は、分割ヒューリスティックが、離接的なイメージ計算の性能に著しい影響を与えることを示している。さらに、ｌｉｖｅＶａｒベースのヒューリスティックは、より厳しい場合の大多数により良く適している。７。
【０１２９】
［ＢＤＤに代わる混合表現(mixed representation)の使用］
ＢＤＤベースの離接的なイメージ計算を単純化するために生きている変数を適用することを検討した。そして都合良く、著しい性能改善が得られた。本明細書においては、ＢＤＤ、プレスバーガー(Presburger)の式、及び実領域における線型制約条件を含む複数のシンボリック表現の組み合わせを使用して、モデル検査でのその応用を検討する。
【０１３０】
この実装では、ＢＤＤに関連する操作にはＣＵＤＤパッケージを、プレスバーガーの式に関連する操作にはオメガライブラリ(Omega library)を、また、実領域における線型制約条件にはパルマ多面体ライブラリ(Palma Polyhedral library)を使用する。離接遷移関係と到達可能な状態のサブセットの両方が、混合シンボリック表現で表現される。
【０１３１】
ここでは、制御フローグラフのブロックｉからブロックｊまでの各遷移に対して、１つの離接遷移関係構成要素Ｔijを作る。ブロックｉとｊの間の遷移が、式ｃｏｎｄijにより保護されるとすれば、
【０１３２】
【数２６】
2009505227.tif 000027
【０１３３】
となる。
【０１３４】
以下の最適化に対して、生きている変数分析(live variable analysis)を利用する。遷移関係Ｔijの構築の間に、ある変数ｘkがデスティネーション（あて先）ブロックｂjにおいて「生きて」いなければ、遷移関係構成要素ｘ'k≡ｅikを除外する。これは、デスティネーションブロックにおいて、ｘkの値が無関係だからである。なおこの場合に、次の状態の変数ｘ'kには任意の値を仮定することができ、したがって、状態空間の抽象化が与えられる。イメージ計算の間に、そのデスティネーションの位置にあるライブでない（生きていない）すべての変数は、自動的に定量化される。
【０１３５】
十分理解できるように、到達可能なサブセットから、生きていない変数を除去することは、シンボリック表現のサイズを減少させるのみではなく、到達可能性分析の潜在的なより速い収束をもたらす。図８のＣ言語コードの部分を例とする。ここで、各ステートメントは基本ブロックであり、すべての変数は大域変数と定義されていると仮定する。
【０１３６】
ここではモデル検査においていかなるコード最適化も行わないから、このプログラムは有効である。変数ｘとｙがプログラム内の他のどこにも使われていなければ、前述の小節における分析の概略は、ｘはＬ２でのみライブであり、ｙはＬ４でのみライブであることを示す。すなわちそれらの値は、Ｌ２とＬ４の実行の後に保存されるべきであり、他のどこでも保存されるべきではない。
【０１３７】
この情報を考慮して、表１に示すように、Ｌ１からＬ６までを１回だけ完了した後で、到達可能性分析の終了を宣言することができる。これは、Ｌ６、（Ｐ≡２∧ｓ≡８）の後に発見される状態が、既に（Ｐ≡２）により包含されるからである（この中で、ｓは任意の値をとることができる）。しかし、ｘとｙが大域的にライブであると仮定すれば、到達可能性分析は、１回目の通過の後に収束することはできない。
【０１３８】
Ｌ６の後に、以前に状態は（Ｐ≡２∧ｘ≡０∧ｙ≡０）であるので、状態（Ｐ≡２∧ｘ≡７∧ｙ≡８∧ｓ≡８）は、既に到達している状態によって包含されない。したがって、到達可能性分析は、収束するまでにさらに２つのステップを必要とする。
【０１３９】
［特別のシンボリック探索戦略］
シンボリック不動点計算を加速するヒューリスティックＩが知られている。例えば、Ｒi-1とＲiが２つの連続した反復からの既に到達している状態の集合であるとすれば、Ｒi+1の計算においてｐｏｓｔ(Ｔ，Ｒi)の代わりにｐｏｓｔ(Ｔ，Ｒi／Ｒi-1)を使用することができる。事後条件(post-condition)Ｉは、リソースを最も多く必要とする演算を緩和するから、（Ｒi／Ｒi-1）のシンボリック表現がＲiのシンボリック表現よりも重要にであれば、これは特性を改善するであろう。なお、収束を検出するためには、（Ｒi+1＝Ｒiであるとき、収束を宣言できるように、）既に到達している状態の全部の集合を蓄積する必要が依然としてある。
【０１４０】
境界(frontier)戦略：
混合表現を使用したときに、既に到達している状態Ｒiの全部の集合を維持することに非常に多大なコストを要することが、観察される。到達可能な状態の集合のサイズがしばしば不動点計算の中間段階で増加し、収束に近づくと低下することは、ＢＤＤベースのモデル検査ではよく知られた事実である。ここでの混合表現に多面体を使用すると、多くの場合に「こぶ状部(hump)」がさらに急峻になる意味で、状況はさらに厳しくなる。これは、主として、線型制約条件に対する多面体べき集合表現(polyhedral power set representation)が正準(canonical)ではない事実による。さまざまな分岐点と再収束点を介して伝搬された後に、多面体は、（それぞれ、より多数の一次不等式を有する）より小さい細片に容易に断片化される。
【０１４１】
以上の観察に基づいて、本発明者らは、リーチフロンティア(Reach Frontier)と呼ぶ特別なシンボリック探索戦略を開発した。このアイデアは、到達した状態の全部の集合を反復の各回において蓄積するのを避け、その代りに境界集合(frontier set)を使用して収束を検出するというものである。概念的には、到達可能な境界集合は、現在の反復における到達した新しい状態の集合である、すなわちＦ0＝Ｉ，Ｆi＝ｐｏｓｔ(Ｔ，Ｆi-1)＼Ｆiである。ラベルが付された遷移グラフが循環（サイクル）を有しないストリームライン(streamline)コードに対して、Ｆiが空になる時に（また、有限回数の反復の後に、集合が空になることが保証される時に）、収束を宣言できる。しかし循環が存在する状態では、境界集合が決して空にならないおそれがある（一例は、無限ループを有する任意のプログラムである）。
【０１４２】
循環が存在する状態で収束を検出するためには、ラベルが付された遷移グラフ内のバックエッジ(back edge)の集合を識別する必要があり、その除去はグラフを非循環にする（例を図１１に示す）。Ｓｐａが、それらのバックエッジの末尾ブロックの集合を示すとすると、Ｓｐａは、状態部分空間を効率的に定める。
【０１４３】
図Ｘにおいて、Ｓｐａ＝（Ｐ＝５∨Ｐ＝７∨Ｐ＝８）である。Ｒ∩ＳｐａであるＳｐａの内側に含まれるすべての到達した状態を記録すれば、集合（Ｆ＼Ｒ∩Ｓｐａ）の空は、収束を検出するために使用できる。ここでは、エントリブロックから始めて、深さ優先探索（ＤＦＳ；Depth-First Search）により、バックエッジを識別する。ＬＴＧが非循環であれば、ＤＦＳの後行順(post-order)は位相幾何学的な順序を与え、すべてのエッジは、より低ランクのブロックからより高ランクのブロックまでである。図１１におけるランク付けは、例えば偶然に、それらのブロックインデックスである。ＬＴＧが循環を有するならば、より高ランクのブロックからより低ランクのブロックまで、すべてのエッジを識別し、それらにバックエッジであるとのラベルを付ける。これらのエッジの除去は、ＬＴＧを有向非循環グラフ(directed acyclic graph)とする。
【０１４４】
図１２においてアルゴリズム１として示す新しい手順は、バックエッジの末尾ブロックＳｐａに加え、シンボリックモデル〈Ｔ，Ｉ〉及びエラーブロックＥｒｒをパラメータとする。なお、Ｓｐａ＝真(true)であるとき、これは通常の到達可能性分析手順に帰する。通常の手順が終了する限り、この手順は終了することが可能である。
【０１４５】
観察２：  Ｄは、バックエッジの除去後にＬＴＧ内のエントリブロックから始まる最長の経路であるとする。ならば、リーチフロンティアは、従来の到達可能性分析手順が終了した後に、さらに最大Ｄ回の反復で終了する。
【０１４６】
最後に、従来の到達可能性分析手順でも、多面体抽象領域(polyhedral abstract domain)では、常には収束しないおそれがあることに注目されたい。しかしそのようなケースは、本実施形態による特定の応用に対しては、実際にはまれにしか起きない。
【０１４７】
ロックステップ(lock-step)戦略：
上述の境界探索戦略は、不動点計算の中間段階において、ピーク時のメモリ使用量を大幅に減少させることができる。しかしながら依然として、Ｆiの混合表現でさえも大きくなりすぎる多くの場合が存在する。異なる長さの複数の循環をＬＴＧが有し、再収束点において循環が良く同期していない場合、（境界集合内の）新しい状態は、多数の基本ブロック内に容易に散乱するおそれがある。これは多くの場合に多数の多面体（及び多数の線型制約条件）を意味するので、蓄積すべき状態のサイズを減少させることによる上述の境界戦略による利得は、徐々に消滅する。
【０１４８】
この問題を検討するために、本発明者らは、Reach_Lockstepと呼ぶ、境界手順に基づく別の探索戦略を開発した。この考えは、バックエッジを介して新しい状態が伝搬する時間を制御することにより、複数の循環を同期させることである。このために、Ｔfはフォワードエッジ(forward edge)のみからなり、Ｔbはバックエッジのみからなるように、遷移関係ＴをＴfとＴbに２分割する。まずＴfを介して収束するまで境界集合を伝搬させ、次に、Ｔbを介して集合Ｒ∩Ｓｐａをフィードバックさせることにより、ロックステップにおいて到達可能性分析を行う。
【０１４９】
図１３においてアルゴリズム２として与えられる新しい手順は、シンボリックモデル〈Ｔf，Ｔb，Ｉ〉、エラーブロックＥｒｒ、及びバックエッジの末尾ブロックＳｐａをパラメータとする。アルゴリズム２は、ＴfとＴbの両方での事後条件計算が新しい状態に到達しないときにのみ、終了する。ロックステップ戦略を使用すれば、より長い反例を得る可能性があることに注目されたい。より短い反例は理解がより容易となりうるという事実を考慮すれば、これは欠点である。しかしここでは、境界戦略では長大な実行時間(runtime)を要するか、あるいは割当時間内には終了しないおそれさえある若干の例があることを示すであろう。これらの場合には、ロックステップが実行可能な唯一の選択肢となる。
【０１５０】
探索戦略実験：
本実施形態による探索戦略を評価するために、F-Soft検証プラットフォーム上に本発明に基づく探索戦略技術を実装した。本実施形態による混合シンボリックアルゴリズムは、公知のＣＵＤＤ、オメガライブラリ、及びパルマ多面体ライブラリで構築される。公知の複合(composite)モデル検査アルゴリズム、ならびにＢＤＤ及びＳＡＴに基づく純粋なブーリアン(Boolean)レベルアルゴリズムと比較することによって、性能評価を行うことが可能である。ここで用いたベンチマークは、Linuxのデバイスドライバ、ネットワークアプリケーションソフトウェア及び携帯機器の埋め込みプログラムを含む、パブリックドメインまたは産業用のＣプログラムである。すべてのテストケースに対して、到達可能性特性を調査する。実験は、２．８ＧＨｚのＸｅｏｎプロセッサと４ＧＢのＲＡＭを備えてRed Hat Linux 7.2を走らせるワークステーション上で実行された。すべての実行に対して、ＣＰＵのタイムリミットは１時間に設定された。
【０１５１】
異なる探索戦略の比較：
まず、プログラム特有の最適化と特別の探索戦略がある場合と、ない場合とについて、混合シンボリック手順の性能を比較する。これらの付加的な単純化がない場合には、本実施形態での混合アルゴリズムの実装は、従来技術の実装に相当する。結果を図１７の表４に示す。試験した各プログラムに対して、列１〜４は、名前、Ｃ言語コードの行、プログラム変数の数、及び基本ブロックの数を列挙している。
【０１５２】
列５〜８は、４つの異なる具体例について、性能を比較している。ここでoldは、ベースライン(baseline)アルゴリズムを表し、liveは、生きている変数に基づく単純化を使用するベースラインアルゴリズムを表し、frontは、境界探索戦略を使用してさらに増補されたベースラインアルゴリズムを表し、lstepは、ロックステップ戦略を使用するベースラインアルゴリズムを表す。列９〜１２は、オメガライブラリに使用する一次等式及び一次不等式のピーク数を比較する。
【０１５３】
これらの例に対しては、多くの場合、ＢＤＤサイズは非常に小さいから、ピークのＢＤＤサイズは報告しないこととする。１１のテストケースの中で、bakeryは、ベーカリー(bakery)プロトコルのＣモデリングであり、tcasは航空交通管制及び航空電子工学システムであり、pppはポイント・ツー・ポイント・プロトコルのＣモデリングである。mcfから始まる例は、携帯機器の埋め込みソフトウェアからもたらされたものであり、それに対して本発明者らは、検証モデルのみを所有し、（Ｃ言語コードの行のような）ソースコード情報を有しない。名前がftpdから始まる例は、LinuxのＦＴＰデーモンからもたらされたものである。
【０１５４】
１１の実験の中で、最適化のない到達可能性計算は２つだけを完了することができ、最適化とロック・ステップ戦略を有するものは、すべてを完了する。すべての方法が完全な走査(complete traversal)を行うことができる場合には、最適化により得られる性能は、著しい。順序性(sequential nature)と変数の局所性の利用が、ソフトウェアモデル検査をスケーラブルにするための基本であることを、この実験は明らかに示している。各反復における線型制約条件の数の比較は、本発明によって提案される技術が、混合シンボリック表現のサイズを減少するのに有効であることを示している。
【０１５５】
純粋なブーリアンレベルアルゴリズムとの比較：
ＢＤＤベースのモデル検査とＳＡＴベースの有界モデル検査とを含む混合ロックステップと純粋なブーリアンレベルエンジンの比較も示す。順序プログラムを処理するために、これらの２つのブーリアンレベルエンジンの両方を慎重に調整した。特に、本実施形態による純粋なＢＤＤベースのアルゴリズムは、さらに、離接分割と生きている変数に基づいた単純化を有する。結果を図１８の表５に示す。
【０１５６】
図１８を参照すると、列１〜３は、プログラムの名前、ブール(Boolean)モデルのビット変数の数、及びすべての所与の特性を決定可能な点の順序深度を示す。列４〜６は、３つの方法の各々に対して、検証が完了可能か、及び、不完了の場合の最大到達深度を示す。ＢＤＤベースの方法は、遷移関係が構築される前に時間切れとなるおそれがあることに注目されたい。その場合には最大到達深度は０である。最後に列７〜９は、各方法の実行時間を秒で記載している。ＢＤＤ／ＳＡＴは非線型演算をビットベクトル演算としてモデル化するが、本実施形態の混合表現はそれらを近似することが可能なので、同種類のものを比較していないおそれがあることに注目されたい。近似が起きる場合には、最後の列に星印を入れてある。
【０１５７】
混合シンボリック表現を使用する到達可能性計算が、すべての例で走査を完了できる唯一の方法であることを、実験データは示している。これは、混合ロックステップがシステムの異なる挙動を適切な抽象レベルでモデル化している事実によるものと確信される。
【０１５８】
正確な状態空間検証を行っているので、本明細書で説明した方法が多面体抽象領域に基づく静的解析とは大幅に異なることを指摘することは有用である。本実施形態によるいずれの結果も、凸閉包ベース(convex hull based)の近似または拡張には基づいてはいない。
【０１５９】
ソースコードレベルのＣ言語プログラムのような順序システム(sequential system)を検査するための、離接分割されたシンボリックモデル検査アルゴリズムを説明した。ここでは、ＢＤＤ及び複数のシンボリック表現の組み合わせを応用して、現代のプログラム言語による著しく豊富なデータ型とより複雑な式とをモデル化し、順序モデルに特有の最適化を開発してモデル検査アルゴリズムのスケーラビリティ(scalability)を改善する。実験結果は、本発明による方法がシンボリックモデル検査に必要な実行時間とピーク時のメモリ使用量とを大幅に減少することが可能なことを示している。複数のシンボリック表現に基づく実装は、ＢＤＤ及びＳＡＴを使用する従来の純粋なブーリアン・レベル検索エンジンに拮抗している。
【０１６０】
ここで、いくつかの具体的な例を使用して本発明を説明したが、本発明の教示がそれに限定されないことを、当業者は認識するであろう。特に、ソフトウェアならびに非同期のハードウェアシステムに由来するモデル、あるいは、並行（コンカレント）システムのインタリービングモデルに対する本発明の教示の応用性は、当業者には明白であろう。したがって、本発明に添付される特許請求の範囲によってのみ、本発明は制限されるべきものである。
【０１６１】
本出願は、2005年8月9日に出願された、米国特許法第119条(e)項による米国仮特許出願第60/706,656号による優先権を主張し、そのすべての内容と包袋は、本出願に対するすべての目的に対して、参考文献として本明細書に含まれる。
【図面の簡単な説明】
【０１６２】
【図１】本発明に基づく方法のフローチャートである。
【図２】状態遷移表の一例である。
【図３】二進状態変数の次の状態の論理を示す単純なブロック図である。
【図４】異なる到達可能性段階におけるＰＰＰ：ＢＤＤサイズを示すグラフである。
【図５】分割された到達可能なサブセットを有する到達可能性分析を示すプログラムの抜粋である。
【図６】局所的に定義された変数ａ，ｂを示すプログラムの抜粋である。
【図７】大域的に定義された変数ｘを示すプログラムの抜粋である。
【図８】到達可能性分析のこれまでの収束を示すプログラムの抜粋である。
【図９】ハイパーグラフ(hypergraph)の一例である。
【図１０】到達可能性分析におけるＰＰＰ：ピークライブ(peak live)ＢＤＤノードを示すグラフである。
【図１１】サイクルのあるラベル付き遷移グラフ（ＬＴＧ；Labeled Transition Graph）であり、（ａ）は元のグラフを示し、（ｂ）はバックエッジ(back edge)を除去したグラフを示す。
【図１２】本発明に基づくREACH_FRONTIER技術を示すアルゴリズム１を示す。
【図１３】本発明に基づくREACH_LOCKSTEP技術を示すアルゴリズム２を示す。
【図１４】各ＢＦＳ段階の後に発見される新しい到達可能な状態を示す表１を示す。
【図１５】到達可能性分析における性能比較を示す表２を示す。
【図１６】NEWを使用する３つの分割ヒューリスティックスの比較を示す表３を示す。
【図１７】到達可能性不動点計算における異なる探索戦略の比較を示す表４を示す。
【図１８】純粋なブール代数レベルのアルゴリズムを使用する混合ロックステップの比較を示す表５を示す。
【図１】
2009505227.tif 000028
【図２】
2009505227.tif 000029
【図３】
2009505227.tif 000030
【図４】
2009505227.tif 000031
【図５】
2009505227.tif 000032
【図６】
2009505227.tif 000033
【図７】
2009505227.tif 000034
【図８】
2009505227.tif 000035
【図９】
2009505227.tif 000036
【図１０】
2009505227.tif 000037
【図１１】
2009505227.tif 000038
【図１２】
2009505227.tif 000039
【図１３】
2009505227.tif 000040
【図１４】
2009505227.tif 000041
【図１５】
2009505227.tif 000042
【図１６】
2009505227.tif 000043
【図１７】
2009505227.tif 000044
【図１８】
2009505227.tif 000045