出荷前のテストは、全部通っていました。手順書の項目に、不合格はひとつもありません。装置は工場で二週間、問題なく回りました。
そして現場で、三日目に止まりました。
飛んでいって、同じ手順を何十回もなぞる。止まりません。ログには、止まった前後だけが残っている。持ち帰って再現を試みる。出ない。それでも対策書は書かなければならない。
このバグは、テストが下手だったから漏れたのではありません。テストという方法では、構造的に届かない場所にいます。
試した範囲と、起こりうるすべて
先に、いちばん誤解されやすいところを書いておきます。
形式手法は、テストを置き換えません。
形式手法が確かめるのは設計です。組み上がった装置ではありません。配線が図面通りか、モータが指令通りの時間で止まるか、センサが仕様通りの閾値で反応するか —— これらはテストにしか分かりません。モデルが抽象化して捨てた部分は、全部テストの担当です。
二つは、違う問いに答えています。テストは「この装置は、動くか」を確かめる。形式手法は「この設計は、破れるか」を確かめる。どちらか一方で足りることはありません。
その上で、違いは一行で書けます。
テストは「試した範囲」を確かめる。形式手法は「起こりうるすべての状態」を確かめる。
この差が効くのは、範囲の外にバグがいるときだけです。そして装置ソフトウェアでいちばん高くつくバグは、たいてい範囲の外にいます。
二軸と、ひとつのインターロック
教科書的な例を一つ置きます。
搬送軸と昇降軸があり、動作範囲が一部重なっている。重なった部分を共有領域と呼びます。安全条件はひとつ。
共有領域に入れるのは、常にどちらか一方だけ。
設計はこうです。各軸は進入前に領域の状態を読む。空いていれば進入し、進入したことを占有センサが検知して、占有フラグが立つ。他方はそのフラグを見て待つ。
読むと、正しく見えます。実際、ほとんどの場合は正しく動きます。
問題はこの順番です。
1. 搬送軸: 共有領域の状態を読む → 空き
2. 昇降軸: 共有領域の状態を読む → 空き ← 搬送軸はまだ進入していない
3. 搬送軸: 進入開始 → 占有センサ検知 → 占有フラグ=占有
4. 昇降軸: 手順 2 で「空き」を読んでいるので、そのまま進入開始
5. 両軸が共有領域内窓は、ステップ 1 と 3 の間にあります。状態を読んでから、占有フラグが立つまで。設計図の上では「確認して、入る」という一本の動作に見えていました。実際には確認と占有確定は別の事象で、その間に他方の確認が入り込めます。
テストを増やしても、ここには収束しない
この設計に、テストは通ります。何度でも通ります。
手順書に沿って動かす限り、二つの確認が同じ窓に落ちることは、まず起きません。窓の幅は制御周期の数回分で、テスト時の指令はスクリプトか操作者が順番に出している。狙って作らない限り、当たらない。
ここが肝心なところです。当たらないテストを千回回しても、当たらない回が千回続くだけです。
発生確率が低いことは、「回数を増やせばいつか当たる」を意味しません。当たるかどうかは、テスト環境がその窓を開けられるかに依存します。上位の周期が現場で変わる。通信が一回遅れる。リトライが入る。段取り替えで指令の間隔がずれる。そこではじめて窓が開いて、二つの確認が同じ隙間に落ちる。
テスト中には出ず、現場で出る。そして現場でも再現しない。この性質は、テスト工数の不足から来ているのではありません。複数の軸・センサ・制御器が同時に動く設計には、特定のインターリーブでしか現れない状態があり、テストはそのインターリーブを選ぶ手段を持っていない —— という構造から来ています。
競合、デッドロック、タイミング依存の不具合は、まとめてこの一群です。
「やってみたが、起きなかった」と「起こり得ない」
テストケースを書くのは、人間です。
だからテストが確認するのは、設計者が思いついたケースです。カバレッジの数字は、書いたケースの中でどれだけ通ったかを測っている。書かなかったケースは、分母に入っていません。想像力の境界が、そのままカバレッジの境界になります。
ここに非対称があります。落ちたテストは、情報が多い。何かが確実に間違っている。しかし通ったテストが教えてくれるのは、「この一本では起きなかった」ということだけです。書かなかったあの順番については、何も言っていない。何も言っていないのに、緑色に見えます。
モデル検査は、ここを機械的にやります。設計を状態と遷移の形で書き、確かめたい性質を書く。あとは初期状態から到達できる状態を、片端から調べる。「両軸が共有領域内にいる状態は到達可能か」に対して、到達可能な状態の全体を調べて答えます。上のステップ 1〜5 のような順番を、誰かが思いつく必要はありません。思いつかなくても、到達可能なら見つかる。
これが「やってみたが、起きなかった」と「起こり得ない」の差です。前者は試した範囲についての報告で、後者は調べた範囲の全体についての結論です。
失敗したときに、何が返ってくるか
もう一つ、実務的な差があります。
テストが落ちたとき、手元に来るのは assertion failed です。どの条件が破れたかは分かる。なぜそこに到達したのかは、自分で追うことになります。
検証が破れたとき、返ってくるのは違反を再現する事象列です。上のステップ 1〜5 が、そのまま出てくる。これを反例と呼びます。読めば、どの隙間を通ったかが分かる。詳しくは 反例とは何か に書きました。
正直に書いておく限界
うまい話に聞こえたなら、限界も同じ密度で書いておく必要があります。三つあります。
一つ。設計しか確かめていません。 検証が「起こり得ない」と言うのは、設計についてです。その設計通りに実装されているか、配線が合っているか、実機のモータが想定時間で止まるかについては、何も言っていません。テストは減りません。減るのは、テストで見つけるつもりだったのに見つからなかった一群だけです。
二つ。状態爆発は、本当にあります。 すべての状態を調べるには、状態空間が調べられる大きさに収まっていなければなりません。軸を増やし、状態変数を増やし、時間の粒度を細かくすれば、組み合わせは指数的に増えます。だからモデルは抽象化です。何を捨てるかを選ぶのが技能であり、限界です。 捨てすぎれば実機に存在しない反例が出る。捨てなさすぎれば、検証が終わらない。ここに魔法はありません。
三つ。証明は、聞いた問いの分しか答えません。 「両軸が同時に共有領域に入らない」を確かめたなら、確かめられたのはそれだけです。三軸目の話も、非常停止からの復帰の話も、含まれていません。安全性質を正しく書くのは、人間の仕事です。 間違った問いを立てれば、間違った問いに対する自信のある答えが返ってきます。「全部証明しました」と言う人がいたら、何を証明したのかを聞いてください。
その上で、残るものは残ります。設計が特定の順番を許しているかどうかは、実機がなくても、誰も思いつかなくても、機械的に確定できる。それだけです。そして、それだけがテストにできないことです。
次に読むもの
検証が破れたときに返ってくる事象列を、現場でどう読み、どう使うかは 反例とは何か で扱います。
この方法が、なぜ趣味の話ではなく規格の要求に入っているのかは なぜ安全規格は、形式手法を求めるのか にあります。