(57)【特許請求の範囲】
【請求項１】
コンピュータ・プログラムの有界モデル検査（ＢＭＣ）のための方法であって、
少なくとも１つの到達可能なプロパティ・ノードを有するプログラムを提供することと、
有界モデル検査（ＢＭＣ）のための前記プログラムを下位問題に分解することであって、
前記プログラムによる分離した制御経路にもとづいて、少なくとも１つの、予め定められた長さの制御経路の集合であるトンネルを生成することと、
前記少なくとも１つのトンネルに課せられた経路制約条件を使用しつつ、ＢＭＣアンローリングを使用して、簡約されたＢＭＣ下位問題を得ることと、
前記到達可能なプロパティ・ノードに対して、１次論理の決定可能なサブセット内の限定記号のない数式（ＱＦＰ）を決定することと、
前記ＱＦＰが前記下位問題に対して充足し得るかどうかを判定するために、前記ＱＦＰの充足可能性を独立に、かつ個々に検査することと、
により、有界モデル検査（ＢＭＣ）のための前記プログラムを下位問題に分解することと、
前記分解することを、１つのＢＭＣ限界に到達するまで続けることと、
を有するコンピュータ・プログラムの有界モデル検査のための方法。
【請求項２】
前記生成することが、分割深度において、すべての制御経路から静的に到達可能な、分割された制御状態を通過する制御経路の互いに素な集合を得るために、アンロールされた制御流れ図（ＣＦＧ）の上で順方向及び逆方向のスライシングを行うことを含む、請求項１記載の方法。
【請求項３】
充足可能性を検査することが、充足可能性モジュロ理論（ＳＭＴ）ソルバーを使用して実行される、請求項１記載の方法。
【請求項４】
前記ＱＦＰ数式が充足し得るならば、反例（ＣＥＸ）を決定し、すべてのＢＭＣ下位問題が充足し得ないならば、アンロールされた深度を増し、分解段階を繰り返すことを、さらに有する、請求項１記載の方法。
【請求項５】
前記下位問題をさらに制約するために、前記少なくとも１つのトンネルに流れ制約条件を適用することを、さらに有する、請求項１記載の方法。
【請求項６】
前記少なくとも１つの到達可能なプロパティ・ノードが存在するか否かを判定するために有界モデル検査（ＢＭＣ）限界への有界な制御状態到達可能性を計算することを、さらに含む、請求項１記載の方法。
【請求項７】
各下位問題が、すべての他の下位問題から独立して、スケジュール設定可能であり、かつ解くことが可能であるように、各下位問題が独立である、請求項１記載の方法。
【請求項８】
前記少なくとも１つのトンネルを、分離した制御経路にもとづいて、１組のより小さいトンネルの集合に分割することと、前記集合のそれぞれを下位問題として解くことを、さらに有する、請求項１記載の方法。
【請求項９】
コンピュータ・プログラムの有界モデル検査（ＢＭＣ）のための方法であって、
少なくとも１つの到達可能なプロパティ・ノードを有するプログラムを提供することと、
有界モデル検査（ＢＭＣ）のためのプログラムを下位問題に分解することであって、
分割深度において、すべての制御経路から静的に到達可能な、分割された制御状態を通過する制御経路の互いに素な集合を得るために、アンロールされた制御流れ図（ＣＦＧ）の上で順方向及び逆方向のスライシングを実行することによって、前記プログラムによる分離した制御経路にもとづいて、少なくとも１つの、予め定められた長さの制御経路の集合であるトンネルを生成することと、
前記少なくとも１つのトンネルに課せられた経路制約条件を使用しつつ、ＢＭＣアンローリングを使用して簡約されたＢＭＣ下位問題を得ることと、
前記到達可能なプロパティ・ノードに対して、１次論理の決定可能なサブセット内の限定記号のない数式（ＱＦＰ）を決定することと、
前記ＱＦＰが前記下位問題に対して充足し得るかどうかを判定するために、充足可能性モジュロ理論（ＳＭＴ）ソルバーを使用して、前記ＱＦＰの充足化可能性を独立して、かつ個々に検査することと、
により、有界モデル検査（ＢＭＣ）のためのプログラムを下位問題に分解することと、
前記分解することを、１つのＢＭＣ限界に到達するまで続けることと、
有するコンピュータ・プログラムの有界モデル検査のための方法。
【請求項１０】
前記ＱＦＰ数式が充足し得るならば、反例（ＣＥＸ）を決定し、すべてのＢＭＣ下位問題が充足し得ないならば、アンロールされた深度を増し、分解段階を繰り返すことを、さらに有する、請求項９記載の方法。
【請求項１１】
前記下位問題をさらに制約するために、前記少なくとも１つのトンネルに流れ制約条件を適用することを、さらに有する、請求項９記載の方法。
【請求項１２】
前記少なくとも１つの到達可能なプロパティ・ノードが存在するか否かを判定するために、有界モデル検査（ＢＭＣ）限界への有界な制御状態到達可能性を計算することを、さらに有する、請求項９記載の方法。
【請求項１３】
各下位問題が、すべての他の下位問題から独立して、スケジュール設定可能であり、かつ解くことが可能であるように、各下位問題が独立である、請求項９記載の方法。
【請求項１４】
前記少なくとも１つのトンネルを、分離した制御経路にもとづいて、１組のより小さい集合のトンネルに分割することと、前記集合のそれぞれを下位問題として解くことを、さらに有する、請求項９記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はコンピュータ検証に関し、特に、コンピュータ・プログラム検証の効率を改善し複雑さを減少するための、有界モデル検査の分解に関する。
【背景技術】
【０００２】
有界モデル検査（ＢＭＣ, Bounded Model Checking）は、コンピュータ・プログラム検証に使用される技術である。ＢＭＣは、有界深度（bounded depth）に対する正確さに対して、完全な設計保償範囲を提供する。圧縮表現（compact representation）を得るために、より豊かな表現理論を使用し、また、その場その場での回路簡略化を使用しているにもかかわらず、深度ｋにおける各ＢＭＣインスタンスは、サイズが大きくなり、設計の連続したアンローリングを使用して解くことが困難になる。
【０００３】
拡張容易なフレームワークを作るためには、ピーク・リソース必要条件を減少させるために、深度ｋにおける各ＢＭＣ問題を、別々に解くことができるより小さい下位問題に、分解することが非常に重要である。
【０００４】
さらに、多コアＣＰＵを有する近代的なサーバを効率的に利用するためには、情報の共有を最少にして、これらの下位問題を独立して解くことが重要である。さらに、単一サーバのメモリ限界によって、これらの下位問題は、メモリ・フットプリントが小さいことも重要である。
【０００５】
これらの問題に対処するために、分解記号走査技術（decomposition symbolic traversal technique）のためのいくつかの技術が、使用されている。しかし、これらの記号走査技術は、拡大縮小可能性の必要条件には対応していない。当該技術分野におけるＢＤＤベースの方法では、遷移関係及び到達可能な状態空間は分割され、分離的な画像計算は各分割に対して別々に実行される。このような状態ベースの分割方法は、各下位問題により検討される到達可能な状態の「記憶」を必要とする。
【０００６】
しかし、これらの方法は、画像計算の中間のブロー・アップを回避し、次の走査段階に対する到達可能な状態の再分割は、非常にリソース集中的であり得る。分散環境で、あるいは多コアＣＰＵサーバ上で実現する場合、このような方法は、分離的な画像演算の結果の再分配において、通信コストの増大を招くであろう。
【０００７】
分散ＢＭＣ法においては、各プロセッサが連続したＢＭＣタイム・フレームのいくつかを占有するように、各ＢＭＣインスタンスは構造上分割される。次に、分散問題は、セントラル・サーバにより管理される分散ＳＡＴ(satisfiability,充足可能性)によって解かれる。この方法は単一プロセッサのメモリ限界を克服し、ブーリアンあるいは命題充足可能性（ＳＡＴ）の個々の処理機能が細かい並列化を使用するが、補助定理の交換と分割インタフェイスに跨る値の伝搬の間に、特にＢＭＣインスタンスを解くことが困難な場合に、著しい通信オーバーヘッドを招く。
【０００８】
他のＢＭＣ方法においては、ＢＭＣインスタンスの分割は、増分学習を利用するように、プロパティ従属式（property sub-formula）の連結と分離に関して実行される。しかし、微細な従属式に対しては、ＢＭＣインスタンスが、さらに分割されることはない。
【０００９】
連続的なＡＴＰＧベースの方法においては、明示的な状態走査とアンローリングは回避される。より正確に言えば、各タイム・フレームにおける解状態キューブ（solution state cubes）は、深度第一あるいは幅第一の方法のいずれかの、また正当である必要がある方法で、列挙される。現実の設計に対して状態空間は通常指数関数的であるので、解状態キューブの蓄積のために提案されるさまざまな状態キャッシング及びプルーニング技術にもかかわらず、この方法は、場合によっては一定の間隔を置くことができる。さらに、この方法は、もし存在するとしても、最も短い反例を保証しない。この方法は、状態ベースの分割方法（state-based partitioning approach）と同じ問題に苦慮する。
【００１０】
テストに使用された記号実行においては、幅優先記号走査の代わりに、深度優先記号走査が、有界深度に対して行われる。経路条件は、記号経路を制約するために、選ばれたプログラム経路に対して生成される。このような方法は、分割の極端な場合であると考えることができ、各プログラム経路は別々に調査される。有界深度に対する完全性は、すべてのプログラム経路を別々に調査することにより、保証される。複数のプログラム経路（各分岐条件のクロス乗積）が存在しうるので、このような方法はオーバーヘッドが大である。
【００１１】
抽象化細分ベースの方法においては、選択された各抽象経路は、不完全な経路条件を有するプログラム経路である。（制約条件ソルバーを使用する）各改良段階においては、具体的なウイットネスを示す必要があるか、あるいは、ウイットネスを示さなくても十分であるか、いずれかの経路条件が導出される。
【発明の開示】
【００１２】
ＳＡＴベースの有界モデル検査（ＢＭＣ）は、現実の設計を検証するために成功裡に適用された。ＢＭＣは、所与の線形時相論理（ＬＴＬ, Linear Temporal Logic）プロパティφの反証（falsification）が所与の順次深度において検査されるモデル検査技術である。これは、ｋタイム・フレームに対する設計のアンローリングと、φが深度ｋ（未満、あるいは）に等しい反例を有するならばΨが充足し得るように、ＢＭＣインスタンスを決定問題Ψに変換することと、Ψが充足し得るか否かを調べるための決定手順の使用と、を含んでいる。
【００１３】
ＢＭＣの強さは、次のことを含んでいる。第一に、記号モデル検査に使用される広範囲な定量化が避けられる。第二に、到達可能な状態は蓄積されず、中間状態表現のブロー・アップを回避する。第三に、近代的なＳＡＴ／ＳＭＴ（Satisfiability Modulo Theory、充足可能性モジュロ理論）ソルバーは、それぞれのＢＭＣアンローリングに対して経路が長くなる場合でさえも、問題に関連する経路を介して検索をすることが可能である。ＳＡＴベースのＢＭＣにおいて、Ψは命題式であり、決定手順はブーリアンＳＡＴソルバーである。ＳＡＴベースのＢＭＣにおいて、いくつかの最新の技術的進歩が提案されているが、ブーリアン表現を使用する問題の公式化には固有の欠点がある。より豊かなデータ型、たとえば、整数、の命題変換、及び、線形演算における高レベル表現式は、高レベル・セマンティクスの「損失」を伴う恐れのある大きなビット・ブラステッドな（bit-blasted）数式を招く。今日の複雑な設計特徴を捕らえるために高レベルの設計抽象化の使用が増加するに伴い、検証技術の焦点は、ブーリアン論理を超えるより豊かな表現理論を使用して、充足可能性モジュロ理論（ＳＭＴ）ソルバーの使用に移りつつある。ＳＭＴベースのＢＭＣのようなＳＭＴベースの検証方法は、ＳＡＴベースあるいはＢＤＤベースの方法よりも、より拡張容易な代案を提供できる可能性がある。
【００１４】
ＳＭＴベースのＢＭＣにおいて、Ψは１次論理の決定可能なサブセット内の限定記号のない数式（ＱＦＰ, Quantifier Free formula）であり、次にＳＭＴソルバーによって充足可能性を検査される。ＳＭＴベースの検証方法は、ＳＡＴベースあるいはＢＤＤベースの方法よりも、より多くの拡張容易な代案の提供において、非常に有望に見える。圧縮表現を得るために、より豊かな表現理論を使用しているにもかかわらず、アンローリングを使用して解くには、各ＢＭＣインスタンスは、サイズが大きくなり、より困難になる。
【００１５】
拡張容易なフレーム・ワークを作るためには、ピーク・リソース必要条件を減少させるために、深度ｋにおける各ＢＭＣ問題を、個々に解くことが可能な小さな下位問題に分解することが有用である。多コアＣＰＵを有するサーバを効率的に利用するためには、部分的な結果の最少の共有で、これらの下位問題を独立して解くことが可能であることも、重要である。さらに、単一サーバのメモリ限界のために、これらの下位問題は、メモリ・フットプリントが小さいことを必要とする。深度ＡにおいてＢＭＣインスタンス（決定問題φ）を、アンロールされたタイム・フレームの代わりに、トンネル、すなわち、長さｋの制御経路の集合にもとづいて、小さな独立の下位問題に、分離的に分解するための新規な拡張容易な方法を実例として説明する。本発明では、軽量な静的変換、ならびに、スライシング、データ経路簡略化、及び制御流れ制約条件のような学習を使用して、各下位問題を単純化する。本発明では、それぞれ減少したＢＭＣ下位問題を、充足し得るφiが存在する時、かつ、その時に限り、φが充足し得るように、独立した決定問題φとして解く。同じ状態に対して繰り返される検索のオーバーヘッドを減少し、増分解決を利用するために、グラフベースの分割、手順呼出しグラフ、及び下位問題順序付けのような、さまざまな分割ヒューリスティックスも、容易に組み込むことが可能である。このようなトンネリング及びスライシング・ベースの簡約（ＴＳＲ）方法は、リソースのピーク必要条件を減少させることにより、総合的なＢＭＣ性能を改善する。
【００１６】
ＢＭＣは、主としてハードウェア設計の検証に使用されて来たが、Ｃ言語の低レベル・ソフトウェア・プログラムの検証にも使用されて来た。本発明では、有限の反復と有限のデータを仮定して、このような低レベル埋め込みプログラムの検証に焦点を合わせている。高度の信頼性を必要とする埋め込みプログラムに対しては、動的メモリ割り当て及び反復は失望である。本発明では、配列上下限の違反、空ポインタ参照解除、イニシャライズされていない変数の使用、及び、到達可能性プロパティとしての利用者提供のアサーションのような、一般的な設計不良を定式化し、ＢＭＣを使用してそれらを解決している。
【００１７】
モデルの大きさを縮少し、冗長なチェックを除外するために、多くの場合に、前処理段階として、静的アナライザー・ツールが、これらのプログラムに適用されるこのようなプロパティのいくつかは、静的解析段階の間に解決されるが、それらの多くは未解決のままであり、いくつかは設計者により解決されるべき予想される設計不良としてマークされる。設計者の負担を減少させるために、ＢＭＣは最後の手段として適用される。したがって、頑丈で拡張容易なＢＭＣが非常に重要である。
【００１８】
コンピュータ・プログラムの有界モデル検査のためのシステム及び方法は、少なくとも１つの到達可能なプロパティ・ノードを有するプログラムの提供を含んでいる。このプログラムは、このプログラムを介して分離的な制御経路にもとづいてトンネルを創出することによる、有界モデル検査（ＢＭＣ）のために、下位問題に分解されている。少なくとも１つのトンネルにより課せられる経路制約条件を使用する一方で、ＢＭＣアンローリングを使用して、簡約したＢＭＣ下位問題が、得られる。到達可能なプロパティ・ノードに対して、１次論理の決定可能なサブセット内に限定記号のない数式（ＱＦＰ）が決定される。ＱＦＰが下位問題に対して充足し得るか否かを決定するために、ＱＦＰの充足可能性が、独立して個々に、検査される。分解は、ＢＭＣ限界に到達するまで、継続する。
【００１９】
これらの及び他の特徴と利点は、添付図面に関連して読まれるべき例証的実施形態の下記の詳細説明から明白であろう。
【発明を実施するための最良の形態】
【００２０】
有界モデル検査（ＢＭＣ）インスタンス（たとえば、決定問題、Ψ）を、より小さい独立の下位問題に、深度ｋにおいて分離的に分解する拡張容易な方法が提供される。本発明による方法は、到達可能な状態での分割の代わりに、トンネル、すなわち、長さｋの１組の制御経路、にもとづいている。各下位問題は、スライシング、データ経路簡略化、及び分割特有の制御流れ制約条件のような低オーバーヘッド静的変換及び学習を使用して単純化される。
【００２１】
各簡約したＢＭＣ下位問題は、充足し得るΨｉが存在する場合にのみΨが充足し得るように、独立した決定問題Ψｉとして解かれる。このようなトンネリング及びスライシング・ベースの簡約（ＴＳＲ, Tunneling and Slicing-based Reduction）方法は、リソースのピーク必要条件を減少することにより、総合的なＢＭＣ性能を改善する。
【００２２】
本発明の重点は、ＢＭＣを使用して、低レベル埋め込みプログラムを検査することである。モデルのサイズを縮小し、冗長なチェックを省くために、多くの場合に前処理段階として静的アナライザー・ツールがこれらのプログラムに適用される。このようなプロパティの幾つかは静的解析段階の間に解決されるが、プロパティの多くは未解決のままであり、幾つかのプロパティは設計者により解決されるべき予想される設計不良としてフラグをたてられる。設計者の負担を減少するために、ＢＭＣが最後の手段として適用される。したがって、頑丈で拡張容易なＢＭＣを持つことが非常に重要である
ＢＭＣ分解のための本発明の原理によるトンネリング及びスライシング・ベースの簡約は、いくつかの利点を有し、従来技術の多くの欠点を克服し、それにより、低レベル埋め込みプログラムの高速でメモリ効率的の良い検証を可能にする。本発明による分解は独立の下位問題を作るので、通信オーバーヘッドを招くことなく、１つの方法を多コアＣＰＵ上で容易に並列化可能である。
【００２３】
本明細書において説明する実施形態は、完全にハードウェア、完全にソフトウェア、あるいはハードウェア要素とソフトウェア要素の両方を含むものとすることが可能である。推奨実施形態において、本発明はソフトウェアで実現される。そのソフトウェアはファームウェア、常駐ソフトウェア、マイクロコード、等を含むが、それだけに制限されるものではない。
【００２４】
実施形態は、コンピュータあるいは任意の命令実行システムにより使用あるいは関連するプログラム・コードを提供するコンピュータで使用可能あるいはコンピュータで読み取り可能な媒体からアクセス可能なコンピュータ・プログラム・プロダクトを含んでもよい。コンピュータで使用可能あるいはコンピュータで読み取り可能な媒体は、命令実行システム、装置、あるいはデバイスにより使用あるいは関連するプログラムを、蓄積し、通信し、伝搬し、あるいは移送する任意の装置を含んでもよい。媒体は、磁気的、光学的、電子的、電磁気的、赤外線、あるいは半導体システム（あるいは装置あるいはデバイス）あるいは伝搬媒体とすることが可能である。媒体は、半導体、あるいはソリッド・ステート・メモリ、磁気テープ、取外し可能なコンピュータ・ディスケット、ランダム・アクセス・メモリ（ＲＡＭ）、リード・オンリー・メモリ（ＲＯＭ）、磁気ハード・ディスク、及び光ディスク、等のようなコンピュータ読み取り可能な媒体を含むことが可能である。
【００２５】
都合の良いことに、本発明の原理によれば、分解は、従来技術の状態ベースの分解に対して経路ベースである。分割に無関係な経路を切り取ることによって、各ＢＭＣ下位問題は、オリジナルのＢＭＣインスタンスより、はるかに縮小され、解くことがより容易な可能性がある。さらに、下位問題が充足し得ると発見されると、ＢＭＣは、ただちに停止可能である。充足し得るトレースの各々は、最短のウイットネスを提供することに注目されたい。
【００２６】
テストで使用された連続的な実行方法とは異なり、本発明による方法は、記号走査に対して２つ以上の制御経路を可能にする。その結果、分割の数と分割のサイズの間のバランスが得られる。単一のスレッドされた環境（threaded environment）において、任意の所与の時間においては、ただ１つのみの下位問題が解かれ、スペース効率を改善する。各ＢＭＣ下位問題は、その場その場で生成され、解かれた後は、メモリーから除去されることが望ましい。下位問題の各計算は実際には「無状態（stateless）」なので、リソース必要条件は現在の下位問題の「難点（difficulty）」によってのみ決定される。したがって、分割のサイズを十分に小さく保つことにより、本実施形態はピークリソース必要条件を制御することが可能である。
【００２７】
分解された下位問題は、各下位問題が独立であるから、相互の間の通信を必要としない。分散環境、あるいは、多くのコアを有するサーバに対しては、各下位問題は、それらの間に通信コストを生ずることなく、別々な処理にスケジュールを設定できる。
【００２８】
ここで図面を参照すると、図面において類似の番号は同一あるいは類似の要素を表す。最初に図１を参照すると、トンネリング及びスライシング・ベースの簡約方法を使用して、ＢＭＣをより簡単で独立の問題に分解するために、有界モデル検査（ＢＭＣ）問題を分解するシステム／方法１００が、実例として示されている。ブロック１１０において、拡張有限状態マシン（ＥＦＳＭ）Ｍ、エラー・ブロックＰ、ソース・ブロックＳ、及び、ＢＭＣ限界Ｎが示されている。拡張有限状態マシン（ＥＦＳＭ）は、もし充足されれば、遷移が起動され、拡張有限状態マシンを現状態から次の状態へ移し、指定された動作を行う「ｉｆステートメント」で表現できる遷移を含んでいる。
【００２９】
ブロック１１１において、有界な制御状態到達可能性情報Ｒが、深度Ｎまで計算される。ブロック１１２内のすべてのｋ≦Ｎに対して、ブロック１１３においてＰ∈Ｒ（ｋ）か否かを調べる。Ｐが深度ｋにおいて静的に到達可能でなければ、ブロック１１４のＢＭＣ段階はｋでスキップされ、ブロック１２２においてｋはインクレメントされ、ブロック１１２で再び調べられる。ｋがｎに等しければ、プログラムは中止される。Ｐが深度ｋにおいて静的に到達可能であれば、ＢＭＣ分解が実行される。
【００３０】
ブロック１１４において、トンネルが創出される、たとえば、１組の制御経路が創出される。次に、トンネルは（制御経路にもとづいて）分離的に１組のＭ個のより小さいトンネル｛γ0,k1，．．．，γ0,kM｝に分割可能である。ブロック１１５における非選択のトンネルｔ＝γ0、kiを選び、トンネルγ0、kiによって課せられる経路制約条件を使用する間に、ＢＭＣアンローリングのその場での簡略化を使用して、ブロック１１６において、簡約したＢＭＣ下位問題ＢＭＣk｜tを得る。オプションとして、ブロック１１７において、流れ制約条件、ＦＣktも適用する。
【００３１】
到達可能なプロパティ・ノードＰに対して、ブロック１１８内の１次論理の決定可能なサブセットに、限定記号のない数式（ＱＦＰ, Quantifier Free formula）（たとえば、ＢＭＣk｜t∧ＦＣkt∧Ｂkp）を得る。ブロック１１９において、望ましくは充足可能性モジュロ理論（ＳＭＴ, Satisfiability Modulo Theory）ソルバーを使用して、減少し条件付きの分離的なＢＭＣ数式の充足可能性を、独立して個々に、チェックする。数式がブロック１２０において充足し得るなら、反例（ＣＥＸ, Counter Example）を得たので、ＢＭＣを停止する。他の場合には、ｉ［Ｍであれば、ブロック１１５に戻り、ｉをインクリメントし、他のトンネルを選ぶことによって、ブロック１２１において選択されていないトンネルを選び続ける。
【００３２】
すべてのＢＭＣ下位問題が充足し得なければ、ブロック１２２においてｋを増加する。限界Ｎに到達するまで、上の処理を続行する。本発明による方法は、経路にもとづくＢＭＣ分解に基本的なフレームワークを提供する。同じ状態に対して繰り返す検索のオーバーヘッドを減少し、増分解決（incremental solving）を利用するために、グラフ・ベース及びプログラム・セマンティクス・ベース、ならびに、分割順序付けのような、分割のためのさまざまな発見的学習を、容易に取り入れることが可能である。
【００３３】
図１に関連して以上に説明した概念を、次に詳細に説明する。拡張有限状態マシン（ＥＦＳＭ）モデルＭは、５つ一組（ｓ0，Ｃ，Ｉ，Ｄ，Ｔ）であり、ここで、ｓ0は初期状態であり、Ｃは１組の制御状態（あるいはブロック）であり、Ｉは１組の入力であり、Ｄはｎ個のデータ経路変数の次元空間Ｄ1×Λ×Ｄn付値であり、Ｔは１組の４つ一組（ｃ，ｘ，ｃ’，ｘ’）の遷移であって、この場合ｃ，ｃ’∈Ｃ及びｘ，ｘ’∈Χである。順序付けた対＜Ｃ，ｘ＞∈Ｃ×Ｄは、Ｍの構成あるいは状態と呼ばれる。ｇ：Ｄ×Ｉα  Ｂ＝｛０，１｝がブール値の可能化条件（あるいはガード）を示し、ｕ：Ｄ×Ｉα  Ｄがアップデート関数を示すとする。可能化述語ｇ（ｘ，ｉ）の下での状態＜ｃ，ｘ＞から＜ｃ’，ｘ’＞への遷移と、アップデート関係ｕ（ｘ，ｉ，ｘ’）は、
【００３４】
【数１】
0005403999.tif 000002
【００３５】
として表される。
【００３６】
自己ループ、すなわち、ｃ≠ｃ’は存在しないと仮定する。ｃ，ｃ’∈ＣＴ（ｃ，ｃ’）＝１に対して、ｃからｃ’への制御遷移に関連する可能化条件が存在する場合にのみ、Γ：Ｃ×Ｃα｛０，ｉ｝はブーリアン述語を示すとする。ＮＯＰ状態は、アップデート遷移が無く、単一入力（出力）遷移の制御状態である。ＳＩＮＫ状態は出力遷移がない唯一の制御状態であり、ＳＯＵＲＣＥ状態は入力遷移がない唯一の制御状態である。
【００３７】
ｓi≡ｃi，ｘi＞は状態を示し、Ｔ（ｓi，ｓi+1）は状態遷移関係を示すとする。経路は、π0,k＝（ｓ0，．．．，ｓk）と示され、述語
【００３８】
【数２】
0005403999.tif 000003
【００３９】
を充足させる、一連の連続した状態である。数式（１）でπ0,0＝１である。経路は、ｋ回の遷移をすれば、長さはｋである。ＬＴＬ（線形時相論理, Linear Temporal Logic）プロパティφが、次の数式の初期状態ｓ0から正確にｋ回の段階で歪曲される恐れがあれば、ＢＭＣインスタンスは、検査を行う。
【００４０】
【数３】
0005403999.tif 000004
【００４１】
ここで、φ（Ｓk）は、φが状態Ｓkで保持する述語を示す。ＢＭＣは、ＳＭＴあるいはＳＡＴソルバーを使用して、数式（２）、０≦ｋ≦ｎの充足可能性を反復して検査する。
【００４２】
制御流れ図（ＣＦＧ, Control Flow Graph）Ｇ＝（Ｖ，Ｅ，ｒ）は、制御状態、１組の指示された制御流れエッジＥ、及び、エントリ・ノードｒに対応する１組のノードＶを有する。ＣＦＧは、可能化し更新された遷移を無視することにより、ＥＦＳＭ  Ｍから得られる。すなわち、
【００４３】
【数４】
0005403999.tif 000005
【００４４】
及びｒ＝ＳＯＵＲＣＥを使用して、ＭからＣＦＧを得る。
【００４５】
例：      図３に示す対応するＥＦＳＭと共に、図２に示す低レベルＣプログラムｆ00を考える。図３にボックスとして示す制御状態は、図２のプログラムの制御点に対応し、ボックス内に示す行番号により示されている。各制御状態は、添えられた小さい矩形のボックス内の番号（１−１０）で識別されることに注目されたい。たとえば、ＳＯＵＲＣＥはブロック１（ソース・ブロック）であり、ＥＲＲＯＲはブロック１０（エラー・ブロック）である。データ経路表現式のアップデート遷移は、各制御状態に示される。ＥＦＳＭの複数の制御状態の間の遷移エッジは、プログラム内のそれらの関連する制御点の間の制御流れに対応する。このようなエッジのそれぞれは、可能化述語と関連している。
【００４６】
制御経路は、述語
【００４７】
【数５】
0005403999.tif 000006
【００４８】
を充足させるγ0,k＝Ｃo，．．．，ｃkとして示される一連の連続した制御状態である。ただし、Γ0,0＝１とする。
【００４９】
本明細書では、制御状態と制御ノードを、それぞれＥＦＳＭ及びＣＦＧの前後関係で同じものを意味するものとして、交換可能に使用している。本明細書では、ブーリアン述語をＢr≡（ＰＣ＝ｒ）と定義する。ここで、ＰＣは、現在の制御状態を追跡するプログラム・カウンタである。この後、ＢＭＣアンローリングの間に深度ｄにおいてアンロールされた変数υを示すために、υdを使用する。
【００５０】
制御状態到達可能性（ＣＳＲ, Control State Reachability）分析は、ＣＦＣの幅優先走査（breadth-first traversal）であり、ここで、制御状態ｂは、Γ（ａ，ｂ）の時、かつ、その時に限り、ａから１段階で到達可能である。すなわち、なんらかの可能化遷移（enabling transition）ａ→ｂが存在する。所与の順次深度ｄにおいて、Ｒ（ｄ）は、静的に到達可能な、すなわち、ガードを無視し、Ｒ（０）＝ｃoを条件として、Ｒ（ｄ−１）内の状態から１段階で到達可能な、制御状態の集合を表すと仮定する。制御状態は、ａ∈Ｒ（ｋ）であれば、深度ｋにおいて、ＣＳＲ到達可能であると言える。ＭのＣＦＧ（図３）に対してＣＳＲを計算すると、０≦ｄ≦７に対して、次式のように、また、図４のアンロールされたＣＦＧ２３０で表すように、集合Ｒ（ｄ）を得る。
Ｒ（０）＝｛１｝、Ｒ（１）＝｛２，６｝、Ｒ（２）＝｛３，４，７，８｝、Ｒ（３）＝｛５，９｝、Ｒ（４）＝｛２，１０，６｝、Ｒ（５）＝｛３，４，７，８｝、Ｒ（６）＝｛５，９｝、Ｒ（７）＝｛２，１０，６｝
一部のｄ（アンロール深度）に対しては、Ｒ（ｄ−１）≠Ｒ（ｄ）＝Ｒ（ｄ＋ｌ）であれば、ＣＳＲは深度ｄにおいて飽和すると言える。
【００５１】
２つの述語ｆとｇを仮定して、ｆ｜gと示される制約条件演算子を定める（あるいは単純化する）、したがって、ｇ＝１であれば、ｆ｜g＝ｆであり、他の場合には、ｆ｜g＝ｄｏｎ’ｔ＿ｃａｒｅである。したがって、ｆ｜g∧ｇ＝ｆ∧ｇである。２つの数式ＡとＢは等価充足可能であると言い、一方の充足可能性が他方の充足可能性を意味するなら、Λ⇔satＢと示され、逆もまた同様である。所与の集合Ａに対して、Ａのサイズを示すため、｜Ａ｜を使用する。
【００５２】
ＥＦＳＭへのモデリングＣ：      有界なヒープ及び有界なスタックの仮定の下での所与のＣプログラムからの数学的模型構成を、次に説明する。構造と配列を、単純な型（ブーリアン、整数、フロート）のスカラー変数に平坦にすることにより、まず簡略化ＣＦＧを得る。有限ヒープ・モデル上の直接メモリ・アクセスを使用して、ポインタ・アクセスを処理し、標準のスライシング及び一定の伝搬を適用する。ブロー・アップを避けるために非再帰的な手順をインラインしないが、再帰的な手順をバウンドし、インラインする。簡略化ＣＦＧからＥＦＳＭを作り、ＥＦＳＭにおいて、各ブロックは固有のｉｄ値を使用して識別され、制御状態変数ＰＣは現在のブロックｉｄを示す。ＰＣに対して、基本ブロックの間の保護された遷移を表す記号遷移関係を作る。各データ変数に対して、ＣＦＧ内のさまざまな基本ブロック内の変数に割当られた式にもとづいて、アップデート遷移関係を加える。アップデートされ保護された遷移機能を表すために、ブーリアン式及び演算式を使用する。一般的な設計不良は、エラーブロックとしてモデル化される。
【００５３】
トンネリング及びスライシング・ベースの簡約（ＴＳＲ）：      深度ｋにおけるＢＭＣインスタンスのより簡単な下位問題への分解を次に説明する。ここで、各下位問題は、長さｋの具体的な経路の排他的なサブセットを有する。低レベルＣプログラムｆ00及び、図２及び図３に示すそのＥＦＳＭ及びＣＦＧを考える。ＣＦＧ２３０に対してｋ＝７まで図４に示すように、ＣＦＧを深度ｋに到るまで単純に展開することにより、アンロールされたＣＦＧを得る。アンロールされたＣＦＧ２３０内の各制御経路は、初期状態ＳＯＵＲＣＥからの抽象プログラム経路であることに、注目されたい。ＢＭＣインスタンスは、ＥＦＳＭモデルを深度ｋに到るまでアンローリングすることにより得ることができ、長さｋのすべてのプログラム経路を収集する。さらに、深度ｋまでのＢＭＣインスタンス内の各プログラム（具体的な）経路は、アンロールされたＣＦＧ２３０内の（抽象）制御経路のインスタンスである。アンロールされた深度が増加するにつれて、経路の数（及び、制御経路）、ならびに、それらの長さも増加する。その結果、各連続したＢＭＣインスタンスを解くことは、ますます困難になる。
【００５４】
図２及び図３を引き続き参照しながら図４を参照すれば、ｋ（アンロール深度）が４から７にそれぞれ増加するにつれて、エラー・ブロック１０に到達する迄の制御経路の数は４から８に増加する。
【００５５】
本発明の原理によれば、より小さい分離的な下位問題へのｋ＝７におけるＢＭＣインスタンスの分解は、制御経路の分割により実行される。分割深度ｐ＝３を選択すると仮定する。この分割深度においては、制御状態５及び９は、静的に到達可能であることに注目されたい。深度７においてブロック１（ＳＯＵＲＣＥ）からブロック１０（ＥＲＲＯＲ）迄のすべての制御経路は、（深度３において）５あるいは９のいずれかを通過する。これらの制御状態を「トンネル・ポスト」（図５）と呼ぶ。トンネル・ポストの互いに素な分割、すなわち、図５の｛５｝及び｛９｝を得る。分割された各トンネル・ポスト、すなわち、｛５｝（あるいは｛９｝）、７におけるＥＲＲＯＲブロック、及び、ＳＯＵＲＣＥブロック、内の（単数または複数の）制御状態から、制御経路の互いに素な集合、すなわち、図５に示すＴ1及びＴ2を得るために、アンロールされたＣＦＧに順方向及び逆方向のスライシングを行う。制御経路の互いに素な集合は、「トンネル」と呼ばれる。図５のトンネルＴ1及びＴ2内のすべての制御経路は、分割深度３において、分割されたトンネル・ポスト５及び９を、それぞれ通過していることに注目されたい。明らかに、深度ｋ＝７において得られ、トンネルＴ１（あるいはＴ２）により制約されたＢＭＣ下位問題は、より少ない経路を有し、オリジナルのＢＭＣインスタンスよりも解くことが容易である可能性を有する。本発明では、各ＢＭＣ下位問題を別々に解き、問題は、下記により大幅に単純化されている。１）無関係な経路、すなわち、トンネル内以外の経路はスライスしない。２）関連経路に対するデータ経路表現を縮小する。３）関連経路に対して制御流れ学習能力制約条件を追加する。
【００５６】
任意のＢＭＣ下位問題の充足可能性は、ＢＭＣインスタンスの充足可能性を意味することに注目されたい。さらに、共有性に極めて乏しい下位問題の独立性により、並列化のための効率的な方法が効率的に得られる。この基本的な分解のアイデアを使用して、方法及び分割の発見的学習法、ならびに、それらを実現するためのシステムを、公式に発表する。これらは、固有の分割オーバーヘッドを軽減する。
【００５７】
ＢＭＣ分解のためのトンネリング及びスライシング・ベースの簡約（ＴＳＲ）方法は、いくつかの利点を有する。１）分解は、状態ベースの分解ではなく、経路ベースである。あるいは、アンロールされたタイム・フレーム・ベースの分解である。分割に無関係な経路を切り取ることによって、各ＢＭＣ下位問題は、オリジナルのＢＭＣインスタンスより、はるかに縮小され、解くことがより容易な可能性がある。さらに、下位問題が充足し得ると発見されると、ＢＭＣを、ただちに停止することが可能である。充足し得るトレースの各々は、最短のウイットネスを提供することに注目されたい。２）従来のテストで使用された連続的な実行方法とは異なり、本発明による方法は、記号走査に対して２つ以上の制御経路を可能にする。その結果、本発明では分割の数と分割のサイズの間のバランスが得られる。３）単一のスレッドされた環境においては、任意の所与の時間において、ただ１つの下位問題が解かれ、スペース効率を改善する。本発明では、各ＢＭＣ下位問題をその場で生成する。（各ＢＭＣ下位問題は、解かれた後は、メモリから除去できる）。各下位問題の計算は実際には「無状態」であるから、リソース必要条件は、現在の下位問題の「困難さ」によってのみ決まる。したがって、分割のサイズを十分に小さく維持することにより、ピーク・リソース必要条件を制御することが可能である。４）従来の方法とは異なり、本発明による分解した下位問題は、各下位問題が独立であるから、相互間の通信を必要としない。分散環境あるいは多コアＣＰＵを有するサーバに対しては、各下位問題は、それらの間に通信コストを生ずることなく、別々な処理にスケジュールを設定できる。５）基本的な分割及び下位問題順序付け方式は、分割オーバーヘッドを減少し、増分解決を利用することを目標とする。この方式は、グラフ分割、及び、手順呼出しグラフのようないくつかの分割ヒューリスティックスを使用して容易に強化できる。要約すれば、本発明は、経路にもとづくＢＭＣ分解に対して基本的なフレームワークを提供し、いくつかの他の発見的学習法を推進する。６）本発明は、充足可能性モジュロ理論（ＳＭＴ）ベースのＢＭＣフレームワークを実現し、産業用の設計に実験結果を提供する。本発明による制御された実験は、本発明による方法の有効性を示している。
【００５８】
トンネル：
【００５９】
【数６】
0005403999.tif 000007
【００６０】
は、初期の制御状態から深度ｉにおける到達可能な１組の制御状態を、示すものとする。ブーリアン述語
【００６１】
【数７】
0005403999.tif 000008
【００６２】
を、下記の時、かつ、その時に限り定義する。
【００６３】
【数８】
0005403999.tif 000009
【００６４】
本明細書では
【００６５】
【数９】
0005403999.tif 000010
【００６６】
をトンネル・ポストと呼ぶ。
本明細書では、述語
【００６７】
【数１０】
0005403999.tif 000011
【００６８】
を充足させる
【００６９】
【数１１】
0005403999.tif 000012
【００７０】
として示すトンネル・ポストの数列として、トンネルを定義する。トンネルは、本質的に１組の制御経路、すなわち、
【００７１】
【数１２】
0005403999.tif 000013
【００７２】
を表すことに注目されたい。
【００７３】
例（図４参照）：
【００７４】
【数１３】
0005403999.tif 000014
【００７５】
に対して、本発明では、
【００７６】
【数１４】
0005403999.tif 000015
【００７７】
を具備している。すべてのトンネル・ポストが指定されていれば、このようなトンネルを完全に指定されたと呼び、他の場合には、部分的に指定されたと呼ぶ。トンネル
【００７８】
【数１５】
0005403999.tif 000016
【００７９】
は、次の時、かつ、その時に限り完全に形式化されていると言う。
【００８０】
・エンド・トンネル・ポスト、すなわち、
【００８１】
【数１６】
0005403999.tif 000017
【００８２】
は、指定されている。
【００８３】
・任意の２つの指定されたトンネル・ポスト
【００８４】
【数１７】
0005403999.tif 000018
【００８５】
を仮定すると、
【００８６】
【数１８】
0005403999.tif 000019
【００８７】
である。
【００８８】
例（図５参照）：      完全に指定され、完全に形式化されたトンネル
Ｔ1（γ0,k）は、
【００８９】
【数１９】
0005403999.tif 000020
【００９０】
である。部分的に指定され完全に形式化されたトンネルを仮定して、次のように完全に指定されたトンネルを作ることができる。
【００９１】
・任意の２つの隣接する指定された
【００９２】
【数２０】
0005403999.tif 000021
【００９３】
すなわち、ｉ＜ｈ＜ｊが未指定であるすべてのトンネル・ポスト
【００９４】
【数２１】
0005403999.tif 000022
【００９５】
の間で、
【００９６】
【数２２】
0005403999.tif 000023
【００９７】
からｊ−ｉ段階順方向のＣＳＲと、
【００９８】
【数２３】
0005403999.tif 000024
【００９９】
からｊ−ｉ段階逆方向のＣＳＲを計算する。
【０１００】
・順方向及び逆方向のＣＳＲの両方から到達可能な制御状態を有する集合
【０１０１】
【数２４】
0005403999.tif 000025
【０１０２】
を形成する。到達不能な制御経路も同様に効率的に「切り取る」ことに注目されたい。
【０１０３】
例（図５参照）：      部分的に指定されたトンネル
【０１０４】
【数２５】
0005403999.tif 000026
【０１０５】
は、順方向及び逆方向のＣＳＲを指定されたトンネル・ポストから計算し、到達可能な制御状態の交点をとることによって、完全に指定されたトンネルに変換可能である。したがって、トンネル・ポスト
【０１０６】
【数２６】
0005403999.tif 000027
【０１０７】
を有する完全に指定されたトンネルｔを得る。
【０１０８】
補助定理１．      上記により構築された完全に指定されたトンネルも完全に形式化されており、所与の制御流れ図及び指定されたトンネル・ポストの所与のシーケンスに対して固有である。
【０１０９】
この後は、完全に形式化されたトンネルのみを考慮する。本明細書では、多くの場合に指定されたトンネル・ポストの（部分的な）シーケンスでトンネルを識別し、（補助定理１を使用して）それを等価な完全に指定されたトンネルと暗黙的に関連付ける。本明細書においては、ＥＲＲＯＲブロックＥｒｒの学習能力、すなわち、
【０１１０】
【数２７】
0005403999.tif 000028
【０１１１】
を考慮する。ここで、（ＰＣ＝Ｅｒｒ）のの時、かつ、その時に限り、ＢErr＝１であり、ＦはＬＴＬ演算子である。
【０１１２】
ＴＳＲベースのＢＭＣ簡略化：      深度ｋ  ＢＭＣkにおけるＢＭＣインスタンスを仮定すると、下記のように、静的に到達不能な制御経路を効率的に切り取ることによって、
【０１１３】
【数２８】
0005403999.tif 000029
【０１１４】
として示されるそれを制約するトンネル
【０１１５】
【数２９】
0005403999.tif 000030
【０１１６】
を使用することが可能である。
【０１１７】
【数３０】
0005403999.tif 000031
【０１１８】
ここで、ＵＢＣ、（到達不能なブロック制約条件）は、当該技術分野において公知である機能的あるいは構造的ハッシング（hushing）、ならびに、定数の畳込み（constant folding）のような、その場でのサイズ縮減技術を使用して、Ｔ0、kを単純化するために、静的に到達不能な制御状態を使用する。
【０１１９】
補助定理２．
【０１２０】
【数３１】
0005403999.tif 000032
【０１２１】
【数３２】
0005403999.tif 000033
【０１２２】
は、指定されたトンネル・ポスト
【０１２３】
【数３３】
0005403999.tif 000034
【０１２４】
を有するトンネルを示すとする。ここで、Ｅrr∈Ｒ（ｋ）である。トンネルｔは、深度ｋにおいてＥｒｒブロックに到達する可能性がある長さｋのすべての経路の集合を表すことに注目されたい。
【０１２５】
定理１．      ＢＭＣk｜t⇔SATＢＭＣk      ＢＭＣkの充足可能性も、ＢＭＣk｜tの充足可能性を暗示することを、明らかにできる。
【０１２６】
ＴＳＲベースのＢＭＣ分解：      トンネルｔのサイズを、
【０１２７】
【数３４】
0005403999.tif 000035
【０１２８】
と定義する。一般に、トンネル・サイズが大きければ、ＢＭＣk｜tの縮小は少ないことが暗示される。大きいモノリシックなＢＭＣ数式を解くのを避けるために、本発明では、より小さい分離的なトンネルを使用して、それを分解する。トンネル
【０１２９】
【数３５】
0005403999.tif 000036
【０１３０】
を仮定すれば、本発明では、各分割トンネルｔiが、それぞれ互いに素なトンネル・ポスト
【０１３１】
【数３６】
0005403999.tif 000037
【０１３２】
をｔ回通過する間に、制御経路のサブセットを有するように、トンネル・ポストｃhを一定の深度ｈにおいて分離的に分割することによって、トンネルを１組のトンネルｔiに、さらに分割することが可能である。表記法では、トンネル・ポスト
【０１３３】
【数３７】
0005403999.tif 000038
【０１３４】
を有するトンネル分割ｔiとなる。ここで、
【０１３５】
【数３８】
0005403999.tif 000039
【０１３６】
である。
【０１３７】
補助定理３．      各分割されたトンネルは、排他制御経路、すなわち、
【０１３８】
【数３９】
0005403999.tif 000040
【０１３９】
を有する。さらに、分割は完了する。すなわち、
【０１４０】
【数４０】
0005403999.tif 000041
【０１４１】
である。
【０１４２】
トンネル分割集合partt＝｛ｔ1，．．．，ｔm｝を仮定すると、ＢＭＣkは、トンネル分割
【０１４３】
【数４１】
0005403999.tif 000042
【０１４４】
すなわち、
【０１４５】
【数４２】
0005403999.tif 000043
【０１４６】
によって別に制約されるより簡単な下位問題に分離的に分割可能である。
【０１４７】
定理２．      ＢＭＣk｜t⇔SATＢＭＣk｜partt      ｋが増加するにつれて、ＢＭＣk問題は大きくなり、ますます解くことが困難になる。一般に、ＢＭＣkを解くことに較べれば、分割と制約条件簡略化オーバーヘッドは無視できる。したがって、ＢＭＣｋ数式を、独立な分離的に分割された簡単なＢＭＣk｜t下位問題に分解することにより、ピーク・リソース必要条件を減少させ、利用可能な場合には、分散されたリソースを使用できる可能性がある。任意の分割方法を使用する固有なオーバーヘッドによって、分割のサイズを分割の数と均衡させる必要があることに注目されたい。
【０１４８】
図６において、方法１は、スライシング及びトンネリング・ベースの簡約方法を使用して、簡単で独立した下位問題にＢＭＣを分解するための擬似コードの実例を示す。行６において、手順Ｃｏｍｐｕｔｅ＿ＣＳＲは、ＣＦＧ  Ｇを取り上げて、深度ｎに対する有界なＣＳＲを計算する。行８−９において、深度ｋにおいてＥｒｒが静的に到達可能でなければ、ＢＭＣ段階は省略される。行１１において、手順Ｃｒｅａｔｅ＿Ｔｕｎｎｅｌは、２つのエンド・トンネル・ポストを取り上げて、順方向及び逆方向の制御流れ到達可能性情報を使用して、トンネルｔを構築する。さらにトンネルを減少させる可能性のためには、制御とデータに依存するスライシングを使用することが可能である。行１２において、（方法２で説明する）アルゴリズムＰａｒｔｉｔｉｏｎ＿Ｔｕｎｎｅｌを使用して、トンネルを分割する。トンネル閾値サイズＴＳＩＺＥを使用して、トンネルｔを、１組の分離的なトンネルparttに再帰的に分割する。
【０１４９】
分割集合parttを仮定すれば、（行１３において）手順Ｏｒｄｅｒ（partt）を使用して、分割の順序付けた集合ord_parttを得る。順序付けヒューリスティックの目標は、下記を含む。
【０１５０】
・増分解決を容易にする。
【０１５１】
・「より容易な」分割に優先順位を付ける。
【０１５２】
ここで、優先順位付けの基準として、トンネルとトンネル・サイズの間のトンネル・ポストの共有を使用する。具体的にいうと、２つのトンネルｔi及びｔjが、一定のｈ＜ｋまでトンネル・ポストの同じプレフィックスを有していれば、オーバーラップしている問題ＢＭＣk｜tとＢＭＣk｜tjの間で、深度０からｈまで、遷移及び学習制約条件を共有することが可能である。同様に、連続したＢＭＣ深度に跨ってオーバーラップしているトンネル分割の間で、情報共有の考えを、容易に拡張可能であることに注目されたい。
【０１５３】
各分割ｔiに対して、分割特有のＢＭＣを得るために、次にＢＭＣk｜tを単純化する（行１５）。任意選択で行１６において、流れ制約条件ＦＣtiを追加する。行１７において、縮小し条件付きのＢＭＣ下位問題の充足可能性を、独立して個々にチェックする。本明細書では、この方法をｔｓｒ＿ｃｋｔと呼ぶ。
【０１５４】
あるいは、所与の深度ｋに対してＢＭＣkを１回生成し、各ｔiに対して独立にＢＭＣk∧ＦＣtiを解くことによって、分割特有の簡略化なしで、分解したＢＭＣ問題も得ることが可能である。しかしながら、ＢＭＣkのサイズは、各分割に対してＢＭＣk｜tを計算するオーバーヘッドを避けるよりも大きい可能性がある。本明細書では、この方法をｔｓｒ＿ｎｏｃｋｔと呼ぶ。ＢＭＣkに対して、集合Ｒ上のＣＳＲを使用して、回路簡略化を適用することに注目されたい。
【０１５５】
深度ｋにおいて、違反が見出されなければ、Ｅｒｒを到達可能な集合Ｒ（ｋ）から除去する。ｋ＞ｎであり、反例（ＣＥＸ, Counter Example）が見出されなければ、ＰＡＳＳを返す。（ブロック／フロー・ダイヤグラムに対しては、図１も参照）。
【０１５６】
図７において、ＴＳＲ分割に対して、トンネル・サイズにもとづいて、再帰的なトンネル分割方法２を示す。トンネルｔとトンネル閾値サイズＴＩＺＥを仮定して、トンネルを、１組の互いに素なトンネル、すなわち、部分的に重なり合わない制御経路に、再帰的に分割する。基本的な流れを次のように説明する。行５において、現在のサイズが閾値ＴＳＩＺＥ未満であれば、分割を省略する。行９において、最高の（ＭＡＸ）到達可能な制御状態を含む連続した指定されたトンネル・ポストを有する一対の深度（ｈ、ｋ）を選択する。行１０において、
【０１５７】
【数４３】
0005403999.tif 000044
【０１５８】
のサイズ、すなわち、
【０１５９】
【数４４】
0005403999.tif 000045
【０１６０】
が最小（ＭＩＮ）であるように、ｈとｋの間のｉを選択する。行１３−１４において、
【０１６１】
【数４５】
0005403999.tif 000046
【０１６２】
を指定されたトンネル・ポスト
【０１６３】
【数４６】
0005403999.tif 000047
【０１６４】
に置換することにより、ｔから分割ｔ’を創出する。このｔ’に対して、行１４において、Ｐａｒｔｉｔｉｏｎ＿Ｔｕｎｎｅｌアルゴリズムを再帰的に呼び出し、集合parttを蓄積する。
【０１６５】
行９及び１０における選択は、具体的には、分割の数を最小化し、分割サイズとの間で良いバランスを得る方向に向けられることに注目されたい。この選択ヒューリスティックは、（後に実験結果を示すように）オーバーヘッドが非常に低く、計算コストはかなり安価である。分割を計算するための相対的な時間が、ソルバーのランタイムに対して相対的に無視できる可能性があるような、特に大きい問題に対しては、もっと費用がかかる分割方法を使用することも可能である。
【０１６６】
一般に、良い分割を見出すことは難しい問題である。一方では、大きいサイズの分割ほど、各下位問題を解くことが困難であるが、繰り返し作業のために分割オーバーヘッドは減少する。他方、小さなサイズの分割は、下位問題は容易であるが、分割オーバーヘッドが大幅に増加する恐れがある。本発明の目標は、本発明によるＥＦＳＭ及びＣＦＧモデルにおける構造的な情報にもとづいて、分割ヒューリスティックスを使用することである。前述のように、方法２は制御状態到達可能性情報を利用する。
【０１６７】
本発明による分解は経路ベースであるから、互いに素な下位問題で同じ経路を調べることはない。しかし、基本的なＢＭＣ方法は「無状態」であるから、同じ状態を再調査することは可能である。下位問題においては、これらの状態から繰り返し検索が結果として生ずる。オーバーヘッドを減少させるためには、小さいエッジ・カットセットを見出すために、ＣＦＧ（あるいはアンロールされたＣＦＣ）上で、グラフ分割技術を使用することも可能である。この集合は、ＳＯＵＲＣＥからＥＲＲまでのトンネル内のすべての経路が集合内の少なくとも１つを通過するように、１組の制御集合に対応する。また、これらの状態は、異なるアンロール深度において到達可能であってもよい。結果として生ずる分割は、より少数の制御状態を共有し、その結果、複数の分割において繰り返し作業を回避する。
【０１６８】
分割特有のＢＭＣ：サイズ縮減      ＣＳＲはＢＭＣインスタンスのサイズを減少させるために使用できる。制御状態がｒ∈Ｒ（ｄ）ならば、ｒに依存する変数のアンロールされた遷移関係は、以下に説明するように、単純化される。本明細書ではブーリアン述語Ｂr≡（ＰＣ＝ｒ）を使用することを想起されたい。ここで、ＰＣは、現在の制御状態を追跡するプログラム・カウンタである。さらに、Ｖdは、ＢＭＣアンローリングの間の、深度ｉにおけるアンロールされた変数ｖを示す。図２のモデルＭを再び考える。ここで、変数ａの次の状態は、ｎｅｘｔ（ａ）＝（Ｂ4‖Ｂ7）？ａ−ｂ：ａとして定義される。（カスケードされたＩＦ−ＴＨＥＮ−ＥＬＳＥに対してＣ言語表記を使用している）。深度ｉ＝３，４に対して、ブロック４，７∈／Ｒ（ｋ）、したがって、Ｂk4＝Ｂk7＝０。この不到達可能性制御状態情報を使用して、ａk+Iに対する式表現を既存の式ａkにハッシュすることが可能である。すなわち、ａk+I＝ａk。このハッシング、すなわち、式の再利用は、論理式、すなわち、ＢＭＣインスタンスのサイズを著しく減少させる。
【０１６９】
所与のトンネルに対して、類似の回路簡略化を適用することができる。トンネル
【０１７０】
【数４７】
0005403999.tif 000048
【０１７１】
に対する所与の深度≦ｋにおける到達不能なブロックの集合は、Ｒに対するそれよりも大きい、すなわち、
【０１７２】
【数４８】
0005403999.tif 000049
【０１７３】
はＣ／Ｒ（ｉ）より大きいことに注目されたい。ここで、Ｃは制御ブロックの全集合である。これは、オリジナルのＢＭＣインスタンスと比較して、分割特有のＢＭＣインスタンスで、より多くのサイズ縮減をもたらす。
【０１７４】
集合Ｒ（ｄ）の大きい基数、すなわち、｜Ｒ（ｄ）｜は、上記の簡略化の範囲、したがって、ＢＭＣの性能を縮小することに注目されたい。異なる長さと異なるループ周期の経路の再収束は、ＣＳＲの飽和に主として関係する。ＣＳＲの飽和は大きい｜Ｒ（ｄ）｜を招き、アンロールされたＢＭＣインスタンスのサイズに不利な影響を与える。
【０１７５】
飽和を避けるために、経路／ループ平衡（ＰＢ）と呼ばれる方法が提案された。この方法は、再収束経路の長さとループの周期が同じであるように、ＮＯＰ状態を挿入することにより、ＥＦＳＭを変換し、その結果、非ＮＯＰ制御状態の静的に到達可能な集合を減少させる。ＮＯＰ状態は、任意の変数の遷移関係を変化させないことに注目されたい。
【０１７６】
流れ制約条件：      所与のトンネル
【０１７７】
【数４９】
0005403999.tif 000050
【０１７８】
に対して、順方向の流れ制約条件（ＦＦＣ）、逆方向の流れ制約条件（ＢＦＣ）、及び到達可能な流れ制約条件（ＲＦＣ）を有する流れ制約条件（ＦＣ）を、次式により、得ることができる。
【０１７９】
【数５０】
0005403999.tif 000051
【０１８０】
ここで、「〜ｓへの集合」及び「〜ｓからの集合」は、それぞれ、ｓからの出力遷移と、ｓへの入力遷移における制御状態の集合を示す。流れ制約条件は、数式（４）で定義したように、トンネル内に固有な制御流れ情報を明示的に収集することに注目されたい。たとえば、ＦＦＣは次のように説明される。深度ｉ、すなわち、ａk+1＝１において到達可能な制御状態ｒを仮定すると、深度ｉ＋１において到達可能な制御状態は、トンネル・ポスト
【０１８１】
【数５１】
0005403999.tif 000052
【０１８２】
と「〜ｒへの集合」の交点になければならない。
【０１８３】
所与の
【０１８４】
【数５２】
0005403999.tif 000053
【０１８５】
に対して、
【０１８６】
【数５３】
0005403999.tif 000054
【０１８７】
の充足可能性に影響を与えずに、流れ制約条件
【０１８８】
【数５４】
0005403999.tif 000055
【０１８９】
を加算することも可能である。
【０１９０】
トンネリング及びスライシング・ベースのＢＭＣ分解のためのシステム及び方法（これは、内容の制限を意図するのではなく、実例の説明を意図している）の推奨実施形態を説明したが、上記の教示を考慮して当業者は修正及び変形を行うことが可能であることが注目される。したがって、添付した特許請求の範囲に大要を示すように、本発明の範囲と技術思想内にある開示した特定の実施形態において、変更が可能であることが、理解されるべきである。このように本発明の態様を、特許法により要求される詳細と独自性と共に説明したが、特許請求の範囲、ならびに、特許証による保護を望むものを、添付した特許請求の範囲に宣言する。
「関連出願情報」
この出願は、２００７年１１月１２日に出願された米国仮特許出願番号第６０／９８７，２０３号を基礎とする優先権を主張し、その開示の全てをここに取り込む。
【図面の簡単な説明】
【０１９１】
【図１】本発明の原理による有界モデル検査分解のためのシステム／方法を示すブロック／フロー・ダイヤグラムである。
【図２】本発明の原理を示すための実例のＣプログラムである。
【図３】本発明の原理を示すための、図２のプログラムに対する拡張有限状態モデル（ＥＦＳＭ）の実例である。
【図４】本発明の原理を示すための、トンネル・ポストを示す深度７のアンロールされた制御流れ略図である。
【図５】本発明の原理によるトンネル分割を示す、分割された深度７のアンロールされた制御流れ略図である。
【図６】本発明の原理による有界モデル検査のためのトンネリング及びスライシング・ベースの簡約を行うための実例プログラムである。
【図７】本発明の原理によるトンネリング分割を行う実例プログラムである。
【図１】
0005403999.tif 000056
【図２】
0005403999.tif 000057
【図３】
0005403999.tif 000058
【図４】
0005403999.tif 000059
【図５】
0005403999.tif 000060
【図６】
0005403999.tif 000061
【図７】
0005403999.tif 000062