反例に基づいた抽象化の洗練

プログラムの正しさ、特に並行処理における時間の概念を含むプログラムの正しさを推論するために、状態遷移モデルが使用されます。特に、有限状態モデルは、自動検証において時相論理とともに使用できます。^{[ 6 ]}したがって、抽象化の概念は、2 つのクリプキ構造間のマッピングに基づいています。具体的には、プログラムは制御フローオートマトン(CFA)で記述できます。^{[ 7 ]}

クリプキ構造を定義する${\displaystyle M}$として${\displaystyle \langle S,s_{0},R,L\rangle }$、 どこ

• ${\displaystyle S}$は有限の状態の集合であり、
• $s0$は初期状態です${\displaystyle S}$、
• ${\displaystyle R}$これは完全な遷移関係であり、
• ${\displaystyle L}$これは、各状態に対して、その状態内で成立する命題名のセットをラベル付けする関数です。

抽象化${\displaystyle M}$定義される${\displaystyle \langle S_{\alpha },s_{0}^{\alpha },R_{\alpha },L_{\alpha }\rangle }$どこ${\displaystyle \alpha }$は、すべての状態をマッピングする抽象化マッピングです。${\displaystyle S}$州へ$\displaystyle S_{\alpha }}$[ ^{5 ]​}

モデルの重要な特性を維持するために、抽象化マッピングは元のモデルの初期状態をマッピングします。$s0$その対応するものに対して$\displaystyle s_{0}^{\alpha }}$抽象モデルにおいて。抽象化マッピングは、2つの状態間の遷移関係が保持されることも保証する。

各反復において、抽象モデルに対してモデル検査が実行されます。たとえば、限定モデル検査では、命題論理式が生成され、その後、SATソルバーによってブール充足可能性がチェックされます。^{[ 5 ]}

反例が見つかった場合、それらが偽例、つまりモデルの抽象化不足から生じる不正確な例であるかどうかを検証します。偽例でない反例はプログラムの誤りを反映しており、プログラム検証プロセスを終了させ、プログラムが誤りであると結論付けるのに十分な場合があります。洗練プロセスの主な目的は、偽例を処理することです。抽象化の粒度を上げることで、偽例を排除します。

洗練プロセスにより、行き止まりの状態と悪い状態が同じ抽象状態に属さないことが保証されます。行き止まりの状態とは、到達可能な状態でありながら出力遷移がない状態であり、悪い状態とは、反例を引き起こす遷移が存在する状態です。^{[ 2 ]}