第6回：BMCを使う――探索の上限と検証結果の意味¶
今回は，有界モデル検査（Bounded Model Checking，BMC）を使います．探索の上限を変えて反例を探し，反例が見つかった場合と，見つからなかった場合の違いを学びます．最後に，モデルの記述，性質の記述，修正，簡略化を総合演習で振り返ります．
演習では，実行前の予想と結果を比較し，解答・解説で理由を確認します．成果物の提出は求めません．特に「どの条件で，どこまで確認したか」を自分の言葉で説明することを目標とします．
6.1 到達目標と準備¶
- バッチモードとインタラクティブモードでBMCを実行できる．
- 探索上限，遷移回数，反例の状態数を区別できる．
- 有界探索で反例が見つからないことを，一般に証明とは結論できないと説明できる．
- 安全性の有限の違反と，活性のループを含む反例を区別できる．
- 帰納法による証明と，反例探索の役割の違いを説明できる．
- モデルの修正と簡略化の根拠を，検証結果と併せて説明できる．
| 内容 | 目安 |
|---|---|
| 準備とBMCの考え方 | 15分 |
| バッチ・対話的な有界探索 | 25分 |
| ループと結果の解釈 | 15分 |
| 帰納法の紹介 | 10分 |
| 総合演習と振り返り | 35〜50分 |
nuXmv 2.1.0の有限状態モデルを使います．今回扱うのはSATを用いるBMCです．整数・実数を含む無限状態モデル向けのSMTのコマンドとは分けて考えます．
New-Item -ItemType Directory -Force -Path "$HOME\nuxmv-tutorial\lesson06"
Set-Location "$HOME\nuxmv-tutorial\lesson06"
$nuxmvExe = "$HOME\Downloads\nuXmv-2.1.0-win64\bin\nuXmv.exe"
Test-Path $nuxmvExe
実行ファイルのパスは実際の展開先に合わせ，最後がTrueになることを確認します．
mkdir -p "$HOME/nuxmv-tutorial/lesson06"
cd "$HOME/nuxmv-tutorial/lesson06"
nuxmvExe="$HOME/Downloads/nuXmv-2.1.0-macos-universal/bin/nuXmv"
ls -l "$nuxmvExe"
実行ファイルのパスは実際の展開先に合わせ，実行ファイルの情報が出ることを確認します．
ファイルはプレーンテキスト，UTF-8（BOMなし）で保存します．以下のリンクから，使用するモデルを作業フォルダーに保存してください．
6.2 BMCの考え方¶
長さを限定して反例を探す¶
初期状態をs0，次の状態をs1と書くと，長さkまでの探索では，モデルの初期条件と遷移をk回分展開して考えます．安全性の例なら，その範囲に違反状態があるかを調べます．
flowchart LR
A["s0: 初期状態"] --> B[s1]
B --> C[s2]
C --> D["…"]
D --> E[sk]SATベースのBMCでは，モデルの条件と性質への違反をBooleanの制約として表し，SATソルバーに解があるかを調べます．解があれば，そこから反例を取り出せます．
kは状態数ではありません．今回の安全性の例では，k = 4なら初期状態を含む5状態，4回の遷移を考えます．一般のLTLでは，ループの条件や式の展開も関わるため，単なる違反状態までの距離だけで探索上限を決められるとは限りません．
検証式をLTLとして用意する¶
安全性「常にcnt < 4」を，今回は次のように書きます．
LTLSPEC G (cnt < 4);
前の回のINVARSPEC cnt < 4;と同じ状態条件の安全性を表せますが，宣言の種類と使うコマンドは異なります．今回の有界探索の中心はcheck_ltlspec_bmcです．不変条件の証明も行うcheck_invar_bmcは6.7節で分けて扱います．
6.3 バッチモードでBMCを実行する¶
小さい上限では見つからないバグ¶
counter_bug.smvを保存します．初期値0から5まで進み，5に留まるモデルです．
MODULE main
VAR
cnt : 0..5;
ASSIGN
init(cnt) := 0;
next(cnt) := case
cnt = 0 : 1;
cnt = 1 : 2;
cnt = 2 : 3;
cnt = 3 : 4;
cnt = 4 : 5;
TRUE : cnt;
esac;
LTLSPEC G (cnt < 4);
各値の次状態を明示してあります．0 → 1 → 2 → 3 → 4 → 5 → 5 → …と動き，4回の遷移後に性質に違反します．
上限3で実行する¶
以下はOSのシェルに入力します．
& $nuxmvExe -bmc -bmc_length 3 .\counter_bug.smv
"$nuxmvExe" -bmc -bmc_length 3 counter_bug.smv
-bmcはBMCでのバッチ実行，-bmc_length 3は探索上限の指定です．このファイルにはLTL式を1つだけ記述しています．出力の主要部分は次です．
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
これは，今回の上限と設定で反例が見つからなかったという結果です．モデルにバグがないという結果ではありません．
上限4に伸ばす¶
コマンドの3を4に変えて再実行してください．今度は式がfalseとなり，反例にはcnt = 0, 1, 2, 3, 4の5状態が現れます．最後の状態でcnt < 4が偽になります．
6.4 インタラクティブモードで上限を変える¶
BMC用の準備¶
OSのシェルで起動します．
& $nuxmvExe -int
"$nuxmvExe" -int
以下はnuXmv >に入力します．
read_model -i counter_bug.smv
go_bmc
show_property
check_ltlspec_bmc -k 3 -l X
check_ltlspec_bmc -k 4 -l X
show_traces -v
go_bmcは今回のSATベースのBMCに必要な構築を行います．第4回のBDDのgoと目的が異なります．-kで最大の探索上限を指定し，このコマンドは0からその上限までの問題を順に調べます．今回は不変条件への有限の違反を探すため，-l Xでループなしを指定しています．
-- no counterexample found with bound 3 and no loop
上のような表示に続き，上限4の実行では次の主要部分が得られます．
-- specification G cnt < 4 is false
-- as demonstrated by the following execution sequence
Trace Description: BMC Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
cnt = 0
-> State: 1.2 <-
cnt = 1
-> State: 1.3 <-
cnt = 2
-> State: 1.4 <-
cnt = 3
-> State: 1.5 <-
cnt = 4
状態番号は1からですが，初期状態からの遷移回数は0から数えます．ループなしでこの安全性の違反を説明するには，違反した状態までで十分です．
モデルや手法を変えるとき¶
修正後のモデルを保存し，次のように読み込み直します．
reset
read_model -i counter_fixed.smv
go_bmc
check_ltlspec_bmc -k 8 -l X
counter_fixed.smvは3で止まる修正版です．上限8まで反例は見つかりません．その結果だけで一般に証明したとは言わず，今回はBDDの検証でも確かめます．
reset
read_model -i counter_fixed.smv
go
check_ltlspec
こちらではis trueとなります．バグモデルを同じBDD手順で調べれば偽です．今回の有限状態モデルに対する通常のLTL検証と，指定した上限でのBMCを比較してください．
6.5 反例なしという結果を正しく説明する¶
| 結果 | 言えること | 次の確認 |
|---|---|---|
| BMCで反例を発見 | モデルが許す違反経路がある | 反例をコードと照合する |
| 指定した上限で反例なし | その探索条件では反例を発見していない | 上限やループ条件，証明手法を検討する |
| 証明を行う手法で真 | その手法が性質の成立を確認した | モデルと要求，仮定の妥当性を確認する |
| エラーや途中終了 | 検証を完了していない | 構文，機能の利用可否，資源などを確認する |
「モデル名，性質，上限，ループ条件，使用したコマンド，結果」を組にして説明します．例えば次のように書けます．
counter_bug.smvのG (cnt < 4)を，check_ltlspec_bmc -k 3 -l Xで調べ，ループなし・上限3まで反例は見つからなかった．その後，上限4で4回の遷移後の違反を発見した．
有限状態でも，十分な探索を行ったことを示す完全性の根拠がなければ，単に大きなkを指定しただけでは証明になりません．特に一般のLTLでは，モデルの状態数をそのまま上限にすれば十分，と考えないでください．
6.6 活性のBMCとループ¶
応答しない無限の経路¶
response_wait.smvは，idle → busyと進み，処理中に{busy, done}を選べるモデルです．性質は次です．
LTLSPEC G ((phase = busy) -> F (phase = done));
処理中に留まり続ける経路があるため，第3回と同じく偽です．新しく読み込んでBMC用に構築し，次を比較します．
check_ltlspec_bmc -k 4 -l X
check_ltlspec_bmc -k 4 -l *
-l Xはループなし，-l *は各上限で可能なループ位置を調べる指定です．このモデルでは前者で反例が見つからず，後者で反例が見つかります．
-> State: 1.1 <-
phase = idle
-- Loop starts here
-> State: 1.2 <-
phase = busy
-> State: 1.3 <-
1.3では値が省略されているため，busyが引き継がれます．ループ部分に応答がなく，それを繰り返すと無限に応答しません．今回の反例は上限2で見つかりますが，式とモデルによって必要な上限は変わります．
2種類のXを区別します
-l XのXは，コマンドのループなし指定です．LTL式のX pは次状態でpという演算子です．同じ文字でも役割が異なります．
ループなし設定だけで，活性一般の反例探索を十分に行えるわけではありません．このモデルをresponse_fixed.smvのようにbusyの次を必ずdoneに直すと，BMCでは指定上限まで反例がなく，BDDの通常検証では真になります．
6.7 証明につなげる：帰納法【発展・任意】¶
初期状態と，次状態への保存¶
不変条件Pを帰納法で証明する基本は，次の2点です．
- 初期状態で
Pが成立する． Pが成立する状態から遷移すると，次状態でもPが成立する．
2を確認するときは，初期状態から到達しない状態も候補になり得ます．この点が，初期状態からの反例探索との違いです．
invariant_proof.smvは，cnt : 0..3で0 → 1 → 2 → 0と繰り返し，INVARSPEC cnt <= 2;を検証します．新しく読み込み，go_bmcの後に次を実行します．
check_invar_bmc -a classic
このコマンドのclassicは1段階の帰納法を使い，この例ではis trueとなります．通常のLTLの有界反例探索とは異なり，証明を行っています．nuXmvにはほかの帰納法や増分アルゴリズムもありますが，オプションは使用中のヘルプで確認してください．
帰納法が失敗しても，モデルの反例とは限らない¶
induction_inconclusive.smvは，初期値x = 0からずっと0に留まります．ただし，到達しない状態には1 → 2 → 3という遷移があり，性質はx != 3です．
同じ帰納法コマンドではcannot prove ... true or false : the induction failsと表示され，2 → 3というInduction Sequenceが得られます．これは初期状態からの反例ではありません．初期状態からは2に到達できないためです．BDDのcheck_invarでは真になります．
自己確認： 出力のCounterexampleとInduction Sequenceを区別し，初期状態からの違反か，帰納的な保存を示せなかった例かを確認します．「帰納法が失敗したから性質が偽」と結論しないでください．
6.8 演習¶
演習1：上限と反例の長さ【基本】¶
counter_bug.smvについて，安全性違反に必要な遷移回数と状態数を予想します．上限3と4でBMCを実行し，結果を比較してください．
解答例と解説
上限3では反例なし，上限4で偽となり，5状態の反例が得られます．初期状態の値0は遷移回数0で，4回後に初めてcnt = 4になります．
自己確認： 「5状態だから上限5が必要」と取り違えないようにします．また，上限3の結果は性質の証明ではなく，後の違反をまだ探索できていない結果です．
演習2：修正後の結果を説明する【基本】¶
counter_bug.smvをコピーして，3に達したら止まるように変更します．BMCの上限8と，BDDによる通常のLTL検証を行い，それぞれで言えることを説明します．
ヒント
cnt = 3 : 4;以降の増加をなくし，既定の分岐で現在値を保てば修正できます．型と性質は変えません．
解答例と解説
counter_fixed.smvでは，0から3まで進める分岐だけを残し，最後をTRUE : cnt;とします．BMCでは指定上限まで反例なし，通常のLTL検証では真です．
初期状態から到達する値は0〜3だけで，3では増加しないため，実際に安全性が成立します．型を0..3に狭める場合も，遷移を直してから型の範囲に収まることを確認します．
自己確認： 「BMCで真だった」ではなく，どちらの手法のどの出力が証明に対応するか説明します．
演習3：ループ条件を比較する【基本】¶
response_wait.smvで-l Xと-l *を比較します．反例の前半とループを復元し，応答の活性に違反する理由を説明してください．
解答例と解説
ループなしでは上限4まで反例は見つからず，ループを調べるとidleからbusyに進んで留まり続ける反例が得られます．有限の途中まで応答していないだけでは，その後にも応答しないことを表せません．ループのない設定に偏ると，この違反を見落とします．
自己確認： 「上限を伸ばせばループなしでも必ず見つかる」と考えないでください．探索上限と，どの形の実行を表現するかは別の設定です．
演習4：帰納法の出力を吟味する【発展・任意】¶
6.7節の2モデルにcheck_invar_bmc -a classicを実行します．後者では初期状態からの経路と，帰納法が表示した状態列を比較し，BDDのcheck_invarでも確認します．
解答例と解説
タイマーの不変条件は帰納法で証明されます．後者は，x = 2から3への遷移が保存条件を満たさないため，この帰納法では結論できません．しかし，初期値0からはずっと0なので，初期状態からの違反経路はありません．通常の不変条件検証では真です．
自己確認： 「証明できた」「反例を見つけた」「この手法では結論できなかった」の3つを区別します．
6.9 総合演習：処理時間を持つ制御器¶
要求と配布モデル¶
system_bug.smvは，次の意図で作ったモデルです．ただしバグが含まれています．
- 待機中は，待機を続けるか処理を開始する．
- 処理中は
ageを0，1，2と進め，その後に応答する． - 応答の次は待機へ戻る．異常状態には入らない．
ackは応答段階かどうかをDEFINEで表す．- 動作には使わない記録用カウンター
log_tickも持つ．
性質は次の2つです．
LTLSPEC G (phase != error);
LTLSPEC G ((phase = busy) -> F ack);
自分で進める手順¶
- ファイルを読み，変数，初期状態，遷移，導出値を整理します．
- 待機からすぐ処理を開始した場合の状態列を予想します．
-
BMC用に構築し，上限3，次に6で検証します．まず安全性を個別に調べる場合は次を使います．
check_ltlspec_bmc -p "G (phase != error)" -k 3 -l X check_ltlspec_bmc -p "G (phase != error)" -k 6 -l X -
応答の活性を含めて調べるときは，ループを含めます．
check_ltlspec_bmc -k 8 -l * -
反例とコードを対応させ，性質を変えずにバグを修正します．
system_fixed.smvとして保存し，BMCと通常のLTL検証をやり直します． - 修正後のモデルから，今回の性質と動作に不要な情報を除き，
system_compact.smvとします．変更前後の状態数を第5回の方法で比較します． - 結果だけでなく，修正と簡略化の妥当性を自分の言葉で説明します．
ヒント：原因の行
現在のphaseがbusyでage = 2のとき，next(phase)は何を選びますか．ackが真になる条件も照合します．
ヒント：簡略化
log_tickは性質やほかの変数の更新条件に使われていません．一方，ageは完了するタイミングに関わります．削除する変数がどこから参照されるか確認します．
解答例と解説：反例と修正
すぐに処理を開始した場合の(phase, age)は，(idle, 0) → (busy, 0) → (busy, 1) → (busy, 2) → (error, 0)です．安全性違反は最短で4回後なので，上限3では見つからず，上限6なら見つかります．異常状態に留まり，ackは偽のままなので，応答の活性にも違反します．
原因はphase = busy : error;です．phase = busy : done;へ変えると意図した応答に進みます．修正後の全体と比較してください．修正後は上限8のBMCで反例なし，通常のLTL検証では2式とも真です．
自己確認： age = 2で処理が完了する遷移では，phaseとageが同時に更新されます．現在値を固定して計算し，応答に入ったときのageは0になることも説明します．
解答例と解説：簡略化と状態数
log_tickの宣言，初期値，次状態の指定を除きます．簡略化後の全体を参照できます．残したphaseとageの遷移は記録値に依存しないので，今回の性質の意味と真偽を保てます．ackは元からDEFINEなので，独立した状態数には数えません．
| モデル | 状態数の上限 | 到達可能な状態数 | 通常のLTL検証 |
|---|---|---|---|
| バグあり | 4 × 3 × 4 = 48 |
20 | 2式とも偽 |
| 修正後 | 48 | 20 | 2式とも真 |
| 記録変数を削除 | 4 × 3 = 12 |
5 | 2式とも真 |
バグの修正で状態数が必ず減るわけではありません．また，ageを単純に除いて処理の継続回数も変える場合は，元と同じタイミングの振る舞いとは言えません．性質の真偽が一致することと，元のモデルと完全に同じ振る舞いであることを区別します．
自己確認： BMCの範囲，通常検証で確認した性質，簡略化で保った観察対象を，それぞれ説明します．
6.10 よくある誤りと全体の振り返り¶
| 状況 | 見直すこと |
|---|---|
| BMC用のモデルが未構築 | 読み込み後にgo_bmcを行う |
| 不変条件をLTLのコマンドで探した | 宣言の種類とコマンドを対応させる |
| 反例なしを真と解釈した | 上限・ループ条件・手法を確認する |
| 活性の反例が見つからない | -l Xだけで探索していないか確認する |
| 修正後も古い結果になる | 保存し，resetから再構築する |
| 帰納法の失敗をバグと解釈した | 初期状態から到達できる状態列か調べる |
| SATソルバーや機能のエラー | 使用する配布版とエラー内容を確認し，担当者と動作確認する |
ヘルプはhelp -p check_ltlspec_bmc，help -p check_invar_bmcで確認できます．SATソルバーに関するエラーは，反例なしの結果とは異なります．別のソルバーを必要とすると決め付けて追加する前に，授業で使用する配布版の機能を確認してください．
- バッチと対話モードで，上限を指定してBMCを実行できる（6.3〜6.4節）．
- 状態数と遷移回数，探索上限を区別できる（演習1）．
- 反例なしと証明の違いを説明できる（6.5節・演習2）．
- 活性の違反をループから説明できる（6.6節・演習3）．
- 帰納法の結果を，反例探索の結果と区別できる（6.7節・演習4）．
- 要求からモデル・性質・修正・簡略化までを一貫して説明できる（総合演習）．
全6回を通して学んだのは，モデルを動かす操作だけではありません．「何をモデルに含め，どの入力や仮定を許し，どの性質を，どの手法と範囲で確認したか」を説明することが重要です．解説を閉じて総合演習を振り返り，曖昧な点は次へ戻って確認してください．
| 振り返る内容 | 戻り先 |
|---|---|
| 状態・遷移・反例 | 第1回 |
| 初期値・次状態・同時更新・非決定性 | 第2回 |
| 安全性・活性・空虚な成立 | 第3回 |
| 環境入力・モジュール・制約 | 第4回 |
| 状態数・簡略化・抽象化 | 第5回 |
参考資料¶
- nuXmv公式ドキュメント：使用バージョンのマニュアルのBounded Model Checking，LTL検証，不変条件の検証を参照します．
- 使用中のnuXmvの
help -pで，アルゴリズムとオプションの適用範囲を確認してください．check_invar_bmcの上限指定は，選ぶアルゴリズムによって意味が異なります．