モデルチェック

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

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

プロパティチェックは、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}$

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

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

このようなシステム要件の一例: エレベーターがある階で呼び出されてからその階でドアが開くまでの間に、エレベーターはその階に最大2回到着することができます。「有限状態検証のためのプロパティ仕様のパターン」の著者は、この要件を次のLTL式に変換しています: ^[15]

${\displaystyle {\begin{aligned}\Box {\Big (}({\texttt {call}}\land \Diamond {\texttt {open}})\to &{\big (}(\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor ((\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (\lnot {\texttt {atfloor}}~{\mathcal {U}}~{\texttt {open}})))))))){\big )}{\Big )}\end{aligned}}}$

ここで、は「常に」、 「最終的に」、 「まで」と読み取られ、その他の記号は「または」、「かつ」、「ない」を表す標準的な論理記号です。 ${\displaystyle \Box }$${\displaystyle \Diamond }$${\displaystyle {\mathcal {U}}}$${\displaystyle \lor }$${\displaystyle \land }$${\displaystyle \lnot }$

モデル検査ツールは、状態爆発問題として一般に知られる状態空間の組み合わせ爆発に直面しており、ほとんどの現実世界の問題を解決するには、この問題に対処する必要があります。この問題に対処するには、いくつかのアプローチがあります。

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

モデル検査ツールは当初、離散状態システムの論理的正しさを推論するために開発されましたが、その後、リアルタイムおよび制限された形式のハイブリッドシステムを処理するように拡張されました。

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

有限の解釈、たとえばリレーショナル データベースとして記述されたものが与えられた場合、その解釈が式のモデルであるかどうかを判断します。

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

重要なモデルチェックツールのリストは次のとおりです。

• Afra:並行およびリアクティブ システムをモデル化するアクター ベースの言語であるRebecaのモデル チェッカー
• 合金（合金分析装置）
• BLAST (Berkeley Lazy Abstraction ソフトウェア検証ツール)
• 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 : 確率的シンボリックモデルチェッカー
• ロメオ: パラメトリック、時間、ストップウォッチ ペトリ ネットとしてモデル化されたリアルタイム システムのモデリング、シミュレーション、検証のための統合ツール環境
• SPIN : 分散ソフトウェアモデルの正確性を厳密かつほぼ自動化された方法で検証するための汎用ツール
• ストーム：^[22]確率システムのためのモデルチェッカー。
• TAPAs : プロセス代数の分析ツール
• TAPAAL : Timed-Arc Petri ネットのモデリング、検証、検証のための統合ツール環境
• Leslie LamportによるTLA+モデル チェッカー
• UPPAAL : 時間オートマトンネットワークとしてモデル化されたリアルタイムシステムのモデリング、検証、検証のための統合ツール環境
• Zing ^[23] –マイクロソフトの実験的なツールで、高レベルのプロトコル記述、ワークフロー仕様、Webサービス、デバイスドライバ、オペレーティングシステムのコアにあるプロトコルなど、さまざまなレベルでソフトウェアの状態モデルを検証します。Zingは現在、Windows用のドライバの開発に使用されています。