モデル検査器を使うのにLTLは必要ない
モデル検査器を使うために線形時相論理を学ぶ必要はない。Kani、CBMC、Alloyのようなツールは、通常のアサーションと関係制約で性質を検証できる。活性を証明する能力と引き換えに、学習曲線は週ではなく時間単位で測られ、ほとんどのソフトウェアのバグに対してそれは見合う交換だ。
時相論理は、ほとんどのモデル検査器が要求する門番だ
古典的なモデル検査器であるSPINやNuSMVは、性質をLTLやCTLで表現することを求める。G(request -> F(response))のように書いて、「グローバルに、すべてのリクエストは最終的にレスポンスに続く」という意味を表す。これは強力だ。プロトコルがデッドロックしないこと、すべてのメッセージが最終的に確認応答されること、システムが公平であることを証明できる。
同時に、これはほとんどの現役開発者が持っていない専門的なスキルでもある。LTL式を読むことはコードを読むこととは異なる。演算子はモーダルであり、意味論は無限トレース上で定義され、単体テストを書いて培った直感は移行しない。だから質問は正当だ：モデル検査のバグ発見能力が欲しいなら、本当に最初にその山を登らなければならないのか？
いや。別のクラスのツールは何十年も存在しており、すでに書いている同じアサーションでコードを検証する。
境界付きモデル検査器はアサーションをSAT問題に変換する
境界付きモデル検査器は、新しい論理を学ぶことを求めない。テストハーネスを書くことを求める。非決定的な入力を宣言し、アサンプションで制約し、ホスト言語で性質を主張する。ツールはループを境界まで展開し、プログラムをSAT式やSMT式に符号化し、ソルバーに反例を見つけるよう依頼する。
ソルバーがUNSATを返せば、その境界内のすべての経路で性質が成り立つ。反例を見つければ、どの入力がバグを引き起こすかを正確に示す具体的なトレースが得られる。時相演算子なし。無限トレースなし。再現可能な入力ベクトルを伴う失敗したアサーションだけだ。
KaniはRust向けの最も手軽な境界付きモデル検査器だ。cargo install kani-verifierでインストールでき、通常のRustコードで動作する。
実例：Rustでのステートマシンの検査
ここにバグのあるステートマシンがある。単純なカウンタを追跡し、各ティックでデクリメントしてゼロになると、アイドルに遷移する。
#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
Idle,
Running,
Stopped,
}
struct Machine {
state: State,
count: u32,
}
impl Machine {
fn start(&mut self, initial: u32) {
if self.state == State::Idle && initial > 0 {
self.state = State::Running;
self.count = initial;
}
}
fn tick(&mut self) {
if self.state == State::Running {
self.count -= 1;
if self.count == 0 {
self.state = State::Idle;
}
}
}
fn stop(&mut self) {
if self.state == State::Running {
self.state = State::Stopped;
}
}
}バグは微妙だ。stopを見てほしい。状態をStoppedに設定するが、countは変更しない。後に何かがstate == State::Stoppedのときcount == 0だと仮定すれば、その仮定は誤りだ。
これを捕捉するKani証明ハーネスを以下に示す：
#[kani::proof]
fn check_stopped_implies_count_zero() {
let mut machine = Machine {
state: State::Idle,
count: 0,
};
let initial: u32 = kani::any();
kani::assume(initial > 0 && initial <= 10);
machine.start(initial);
machine.tick();
machine.stop();
assert!(
machine.state != State::Stopped || machine.count == 0,
"Stopped state should have count == 0"
);
}Kaniはすべての経路を探索する。initial == 2の場合、start後に機械はcount == 2でRunning状態だ。1回のtickでcountは1に減るが状態はRunningのまま。そしてstopで状態はStoppedに、countは1のままになる。アサーションが失敗する。Kaniはこの正確なトレースを報告する。
これが時相論理なしのモデル検査の体験だ。Rustを書く。Rustでアサーションを書く。ツールがどの入力がそれを破るか教えてくれる。
Alloyは関係論理で設計レベルのバグを見つける
境界付きモデル検査器はコードを検証する。Alloyは設計を検証する。
Alloyは従来のモデル検査器ではなくモデルファインダーだが、その違いはワークフローほど重要ではない。システムを一連の関係として記述し、状態不変条件を一階論理の制約として表現し、Alloyに反例を見つけるよう依頼する。ユーザー定義の範囲内ですべての可能なインスタンスを探索し、失敗の図を示す。
以下は、単純な有向グラフの性質に関するAlloyモデルだ：
sig Node {
next: set Node
}
pred reachable[n1, n2: Node] {
n2 in n1.^next
}
assert symmetric_reachability {
all n1, n2: Node |
reachable[n1, n2] implies reachable[n2, n1]
}
check symmetric_reachability for 3このアサーションは、到達可能性が対称であると主張する。Alloyは3ノード以下のすべてのグラフでこれを検査し、即座に反例を描画する：n1がn2を指すが、n2には出辺がないグラフ。G、F、U演算子はどこにも現れない。
諦めるもの：活性と無限の振る舞い
この利便性には代償がある。境界付きモデル検査器は、ループ境界やトレース長までの振る舞いしか検証できない。リクエストが最終的に応答されることを証明できず、最初のNステップ内に悪いことが起こらないことだけを証明できる。Alloyも自身の範囲内のインスタンスしか検査できない。任意に大きなシステムの性質を証明できず、境界以下に反例が存在しないことだけを示せる。
合意プロトコルがコミットされた書き込みを失わないこと、すべてのメッセージが最終的に配信されることを証明する必要があるなら、依然として時相論理と非境界モデル検査が必要だ。TLA+のようなツールは時相論理を、様相論理よりも数学のような構文で包むが、根本の意味論は依然として時相的だ。
データ構造不変条件、API契約の強制、47番目の実行経路でのみ発動する競合状態の発見には、境界付きツールで通常十分だ。単体テストが見逃すバグを捕捉し、教科書なしで読めるアサーションでそれを行う。
5分でKaniを始める
Rustがインストールされていれば、境界付きモデル検査はコマンド一つで届く距離だ。
cargo install kani-verifier
cargo kani setup新しいクレートを作成し、微妙なバグを持つ関数を書き、#[kani::proof]ハーネスを追加する。cargo kaniを実行する。Kaniが反例を見つければ、失敗を引き起こす具体的な入力を出力する。VERIFICATION SUCCESSFULと報告されれば、デフォルトの境界内のすべての経路で性質が成り立つ。
状態空間が小さく不変条件が明確な関数から始めよう。ステートマシン、パーサー検証、プロトコル状態遷移は理想的な最初の対象だ。最初からHTTPサーバー全体を検証しようとしないこと。SATソルバーにも限界があり、あなたの忍耐にも限界がある。
FAQ：境界付き対非境界、活性、どこから始めるか
境界付きモデル検査は本当にモデル検査か？
技術的には、状態グラフを明示的に探索するのではなく、問題を充足性クエリとして符号化する変種だ。バグを発見しようとする開発者にとって、その違いは学問的なものだ。すべての経路を体系的に探索するという点で、実際にモデル検査の意味するところだ。
KaniやCBMCで活性を証明できるか？
直接的にはできない。活性は無限の振る舞いについての推論を必要とし、境界付きツールは探索を明示的に制限する。十分なステップを展開して不動点に到達するよう境界付き活性検査を符号化することもあるが、それは高度な技法だ。
TLA+はどうか？時相論理を必要とするか？
TLA+はTemporal Logic of Actionsを使うので、技術的にはそうだ。しかしLeslie Lamportは構文を通常の数学のように読めるよう設計した。ほとんどのTLA+仕様はテキストの90%を状態不変条件とデータ構造制約に費やし、時相演算子ではない。非境界時相推論が必要なら、最も手軽な道だ。
AlloyとKani、どちらを使うべきか？
Rustコードがあり実装詳細を検証したいならKaniを使う。まだシステムを設計中で、コードを書く前に不変条件が可能かどうかを探索したいならAlloyを使う。
野心的ではなく問題に合ったツールを選べ
時相論理は美しく強力だが、形式検証の前提条件ではない。境界付きモデル検査器と関係モデルファインダーは、すでに知っている言語で性質を表現できる。システムが最終的に停止することを証明はしないが、データベースのステートマシンを破損させる1ずれのエラーを見つける。ほとんどのチームにとって、それが重要なバグだ。
単一の状態を持つ関数でKaniを始めよう。1つのアサーションを書く。ソルバーに、見落としたものを教えてもらおう。