背景
航空宇宙、自動運転、OS カーネルなどの安全性が極めて重要なシステムでは、従来のテストによる網羅は不可能です。形式的検証は、数学的証明を用いてシステムが仕様を満たすことを論理的に保証します。
核心理論
1. 時相論理 (LTL/CTL)
システムの振る舞いを時間軸上で記述します。$\mathbf{G},\varphi$（常に成立）や $\mathbf{F},\varphi$（いつか成立）などの演算子を用います。
2. モデル検査 (Model Checking)
Kripke 構造を用いて状態空間を探索し、仕様への違反がないかを確認します。
図示
図 1：Kripke 構造における初期状態、安全状態、違反状態の遷移グラフ。