PR

状態爆発をいかに抑えるか

【図4 プログラムの状態数を減らす抽象化が必須】 通常のプログラムの状態数はそのままでは天文学的な規模であり,モデル化したとしても状態数が爆発してしまう。モデル検査では何らかの状態空間の絞り込みが必要で,これを「抽象化」や「効率化」と呼ぶ。状態空間を絞り込む手法にはさまざまなアルゴリズムが提案されている。
図4 プログラムの状態数を減らす抽象化が必須
通常のプログラムの状態数はそのままでは天文学的な規模であり,モデル化したとしても状態数が爆発してしまう。モデル検査では何らかの状態空間の絞り込みが必要で,これを「抽象化」や「効率化」と呼ぶ。状態空間を絞り込む手法にはさまざまなアルゴリズムが提案されている。
[画像のクリックで拡大表示]

 モデル検査の場合,状態遷移モデルであれば何でも調べられるわけではなく,幾つか制限がある。例えば,入力するモデルの状態数は有限で,一定の規模以下に抑える必要がある(図4)。32ビットの変数の値を,そのまま状態遷移モデルの各状態にマッピングしてしまうと,それだけで数十億の状態になってしまう。このため,変数は幾つかの定数に置き換えて使うのが原則だ。実際には「数千行のソフトウエア・モジュールごとにモデル化することが多い」(メルコ・パワー・システムズ 技術統括部 ビジネスチーム2の早水公二氏)という注4)

注4) LSI設計の形式検証の場合は「数万ゲート規模のモジュールを形式検証にかけることが多い」(東京大学 大規模集積システム設計教育研究センター 教授の藤田昌宏氏)という。

 こうした制約があるのは,状態数が多すぎると,「状態爆発」と呼ぶ現象が起き,現在のコンピュータで現実的な時間内にしらみつぶしの探索を終えられなくなってしまうからだ。一般にモデル検査ツールの内部では,与えられた状態遷移モデルを時間軸上に展開し,ツリー状の状態遷移パスの形に変換する(図1)。このツリー構造の枝分かれが多い場合や,与える状態数が多すぎると,ツリーを構成するノードの数が指数関数的に増大し,探索時間が天文学的な規模に膨らんでしまうのである。

 モデル検査の一部のアルゴリズムでは10120個の状態数を扱えることが理論的に分かっているものの,一般に現実のシステムの状態はこれよりもはるかに巨大である。このためモデル検査を用いる場合は,現実のシステムの状態数を何らかの方法で減らしたり,圧縮したりする必要がある(図4)。モデル検査技術の肝は,まさにこの状態圧縮の方法にある。

 状態爆発を避けるアプローチとしては,主に3つある。(1)入力する状態遷移モデルそのものを,ソフトウエア技術者自身が工夫して絞り込む,(2)探索が速くなるように,探索アルゴリズムやそのデータ構造を工夫する「効率化」と呼ぶ方法を導入する,(3)省略できそうな探索パスを一定の条件でツールが判断して切り捨て,探索空間そのものを半自動的に狭める「抽象化」と呼ぶ方法を用いる,といったことだ(図4)。モデル検査の歴史はこうした探索アルゴリズムの発展の歴史といっても過言ではない。

探索アルゴリズムは多種多様

 モデル検査の探索アルゴリズムには,さまざまな手法がある(表1)。まず効率化の手法として最も代表的なのが「シンボリック・モデル検査(symbolic model checking)」と呼ぶ手法である。モデル検査ツールとして有名な「SMV(symbolic model verifier)」や「NuSMV」に採用されている注5)

注5) 一般に「シンボリック」というと変数に置き換えることを意味するが,シンボリック・モデル検査では,変数ではなく論理式を1つのシンボルに置き換えることで探索を効率化している。

【表1 いかに状態爆発を抑えるか】 モデルの状態爆発を抑え,現実的な時間でモデル検査できるようにするには,探索アルゴリズムの工夫が必須である。これまでにさまざまなアルゴリズムが提案・実装されている。それぞれ工夫の重点は異なっており,目的に応じて使い分けるべきものである。このほかの抽象化方法としては,状態遷移の対称性を利用して状態を減らす方法や「Cone of influence」「データ抽象化(data abstraction)」などがある。
表1 いかに状態爆発を抑えるか
モデルの状態爆発を抑え,現実的な時間でモデル検査できるようにするには,探索アルゴリズムの工夫が必須である。これまでにさまざまなアルゴリズムが提案・実装されている。それぞれ工夫の重点は異なっており,目的に応じて使い分けるべきものである。このほかの抽象化方法としては,状態遷移の対称性を利用して状態を減らす方法や「Cone of influence」「データ抽象化(data abstraction)」などがある。
[画像のクリックで拡大表示]