モデル検査

コンピュータサイエンスにおいて、モデル検査またはプロパティ検査とは、システムの有限状態モデルが所定の仕様（正当性とも呼ばれる）を満たしているかどうかを確認する手法である。これは通常、ハードウェアシステムまたはソフトウェアシステムに関連付けられており、仕様には活性要件（ライブロックの回避など）と安全性要件（システムクラッシュを表す状態の回避など）が含まれる。

このような問題をアルゴリズム的に解決するためには、システムのモデルと仕様の両方を、何らかの厳密な数学的言語で定式化する必要があります。この目的のために、問題は論理学におけるタスクとして定式化され、すなわち、構造が与えられた論理式を満たすかどうかを検証することになります。この一般的な概念は、多くの種類の論理と多くの種類の構造に適用できます。単純なモデル検査問題は、命題論理における式が与えられた構造によって満たされるかどうかを検証することから成ります。

2 つの記述が等価でない場合に、プロパティチェックが検証に使用されます。詳細化の過程で、仕様は上位レベルの仕様では不要な詳細情報で補完されます。新しく導入されたプロパティを元の仕様と照合して検証することは不可能なので、その必要はありません。したがって、厳密な双方向等価性チェックは、一方向のプロパティチェックに緩和されます。実装または設計はシステムのモデルとみなされ、仕様はモデルが満たさなければならないプロパティです。^{[ 2 ]}

ハードウェアおよびソフトウェア設計のモデルを検査するための重要なクラスであるモデル検査手法が開発されており、その仕様は時相論理式で与えられています。時相論理仕様の先駆的な研究は、アミール・プヌエリによって行われ、彼は「時相論理を計算機科学に導入した画期的な研究」で1996年のチューリング賞を受賞しました。^{[ 3 ]} モデル検査は、EM クラーク、EA エマーソン、^{[ 4 ] [ 5 ] [ 6 ]} JP クエイユ、J. シファキスによる先駆的な研究から始まりました。^{[ 7 ]}クラーク、エマーソン、シファキスは、モデル検査の分野を創設および発展させた画期的な研究で2007年のチューリング賞を共同受賞しました。^{[ 8 ] [ 9 ]}

モデル検査は、ハードウェア設計に最もよく適用されます。ソフトウェアの場合、決定不能性（計算可能性理論を参照）のため、このアプローチは完全にアルゴリズム的ではなく、すべてのシステムに適用でき、常に答えを出すことはできません。一般的には、与えられた特性を証明または反証できない場合があります。組み込みシステムハードウェアでは、 UMLアクティビティ図^{[ 10 ]}や制御解釈ペトリネット^{[ 11 ]}などによって提供される仕様を検証することが可能です。

この構造は通常、産業用ハードウェア記述言語または特殊用途言語によるソースコード記述として与えられます。このようなプログラムは有限状態機械（FSM）、すなわちノード（または頂点）とエッジからなる有向グラフに対応します。各ノードには一連の原子命題が関連付けられており、通常はどのメモリ要素が1であるかを示します。ノードはシステムの状態を表し、エッジは状態を変更する可能性のある遷移を表し、原子命題は実行時点で成り立つ基本的な特性を表します。^{[ 12 ]}

形式的には、問題は次のように述べることができる。時間論理式として表現された望ましい特性が与えられたとき、${\displaystyle p}$構造${\displaystyle M}$初期状態${\displaystyle s}$決定する${\displaystyle M,s\models p}$。 もし${\displaystyle M}$ハードウェアの場合と同様に有限であるため、モデル検査はグラフ探索に帰着する。

到達可能な状態を一つずつ列挙する代わりに、一度に多数の状態を考慮することで、状態空間をより効率的に走査できる場合があります。このような状態空間の走査が、一連の状態と遷移関係を論理式、二分決定図（BDD）またはその他の関連データ構造として表現することに基づいている場合、モデル検査方法は記号的になります。

歴史的に、最初の記号的手法はBDDを使用しました。1996 年に人工知能のプランニング問題( satplan を参照)の解決に命題充足可能性が成功した後、同じアプローチが線形時相論理(LTL) のモデル検査に一般化されました。プランニング問題は、安全性のプロパティのモデル検査に対応します。この方法は、境界付きモデル検査として知られています。^{[ 13 ]}境界付きモデル検査におけるブール充足可能性ソルバーの成功により、記号モデル検査で充足可能性ソルバーが広く使用されるようになりました。^{[ 14 ]}

モデル検査ツールは、状態空間の組み合わせ爆発という問題に直面しており、これは現実世界のほとんどの問題を解決するために解決しなければならない問題です。この問題に対処するには、いくつかの方法があります。

1. 記号アルゴリズムは、FSM のグラフを明示的に構築することを回避し、代わりに、量化命題論理の式を使用してグラフを暗黙的に表現します。二分決定図 (BDD) の使用は、Ken McMillan ^{[ 16 ]} 、 Olivier Coudert と Jean-Christophe Madre ^{[ 17 ]}の研究、および CUDD ^{[ 18 ]や BuDDy [ 19 ]}などのオープンソースの BDD 操作ライブラリの開発によって普及しました。
2. 限定モデル検査アルゴリズムは、FSMを固定ステップ数だけ展開し、${\displaystyle k}$財産違反が発生する可能性があるかどうかを確認します${\displaystyle k}$またはより少ないステップ。これは通常、制限付きモデルをSATのインスタンスとしてエンコードすることを含みます。このプロセスは、より大きな値で繰り返すことができます。${\displaystyle k}$考えられるすべての違反が排除されるまで（反復深化深さ優先探索を参照）。
3. 抽象化は、まずシステムを単純化することによって、そのシステムの特性を証明しようとするものです。単純化されたシステムは通常、元のシステムと全く同じ特性を満たさないため、洗練のプロセスが必要になる場合があります。一般的に、抽象化は健全であること（抽象化で証明された特性が元のシステムでも真であること）が求められますが、抽象化が完全でない場合もあります（元のシステムのすべての真なる特性が抽象化でも真であるとは限りません）。抽象化の一例として、非ブール変数の値を無視し、ブール変数とプログラムの制御フローのみを考慮することが挙げられます。このような抽象化は粗雑に見えるかもしれませんが、実際には、例えば相互排他性などの特性を証明するのに十分である場合があります。
4. 反例誘導型抽象化改良 (CEGAR) は、粗い (つまり不正確な) 抽象化からチェックを開始し、それを反復的に改良します。違反 (つまり反例) が見つかると、ツールはそれが実現可能かどうかを分析します (つまり、違反は本物か、不完全な抽象化の結果か)。違反が実現可能であれば、ユーザーに報告されます。そうでない場合は、実現不可能性の証明を使用して抽象化を改良し、チェックを再度開始します。^{[ 20 ]}

モデル検査ツールは当初、離散状態システムの論理的正しさを推論するために開発されたが、その後、リアルタイムシステムや限定的なハイブリッドシステムにも対応できるように拡張された。

モデル検査は、計算複雑性理論の分野でも研究されている。具体的には、自由変数のない一階述語論理式が固定され、以下の決定問題が検討される。

例えば、関係データベースとして記述されるような有限の解釈が与えられた場合、その解釈が数式のモデルであるかどうかを判断します。

この問題は回路クラスAC ⁰に属します。入力構造にいくつかの制約を課すと扱いやすくなります。たとえば、ツリー幅が定数で制限されていることを要求すること (これはより一般的には、単項二階述語論理のモデル検査の扱いやすさを意味します)、すべてのドメイン要素の次数を制限すること、および有界展開、局所的に有界展開、どこにも稠密でない構造などのより一般的な条件などです。[ 21 ^{]これらの}結果は、自由変数を持つ一階述語論理式のすべての解を列挙するタスクに拡張されています。

以下に、重要なモデル検証ツールの一覧を示します。

• Afra：並行システムやリアクティブシステムをモデリングするためのアクターベース言語であるRebecaのモデルチェッカー
• 合金（合金分析装置）
• BLAST（Berkeley Lazy Abstraction Software Verification Tool）
• CADP（分散プロセスの構築と分析）は、通信プロトコルと分散システムの設計のためのツールボックスです。
• CPAchecker：CPAフレームワークに基づいた、C言語プログラム用のオープンソースソフトウェアモデルチェッカー
• ECLAIR：CおよびC++プログラムの自動分析、検証、テスト、変換のためのプラットフォーム
• FDR2 ： CSPプロセスとしてモデル化および指定されたリアルタイムシステムを検証するためのモデルチェッカー
• FizzBee：TLA+よりも使いやすい代替手段で、Pythonライクな仕様記述言語を使用し、TLA+のような振る舞いモデリングとPRISMのような確率モデリングの両方を備えています。
• MPIプログラム用のISPコードレベル検証ツール
• Java Pathfinder：Javaプログラム用のオープンソースモデルチェッカー
• Libdmc：分散型モデル検査のためのフレームワーク
• mCRL2ツールセット、Boostソフトウェアライセンス、 ACPベース
• NuSMV：新しい記号モデルチェッカー
• PAT：並行システムおよびリアルタイムシステム向けの強化されたシミュレータ、モデルチェッカー、および改良チェッカー
• Prism：確率的記号モデルチェッカー
• Roméo：パラメトリック、時間、ストップウォッチペトリネットとしてモデル化されたリアルタイムシステムのモデリング、シミュレーション、検証のための統合ツール環境
• SPIN：分散ソフトウェアモデルの正当性を厳密かつほぼ自動化された方法で検証するための汎用ツール
• Storm : ^{[ 22 ]}確率システムのモデルチェッカー。
• TAPAs：プロセス代数解析のためのツール
• TAPAAL ：時間付きアークペトリネットのモデリング、検証、妥当性確認のための統合ツール環境
• TLA+モデルチェッカー（Leslie Lamport著）
• UPPAAL：時間オートマトンネットワークとしてモデル化されたリアルタイムシステムのモデリング、検証、妥当性確認のための統合ツール環境
• Zing ^{[ 23 ]} – Microsoftの実験ツールで、ソフトウェアの状態モデルをさまざまなレベルで検証します。高レベルのプロトコル記述、ワークフロー仕様、Web サービス、デバイスドライバ、およびオペレーティングシステムの中核にあるプロトコルなどです。Zing は現在、Windows 用ドライバの開発に使用されています。