ご相談くださる方は、「形式手法を導入したい」とはおっしゃいません。たいていは、すでに起きた出来事についての質問から始まります。ひとつでも心当たりがあれば、その質問ひとつからで十分です。
以下は、実際によくいただく八つです。
シミュレーションでは出なかったのに、現場でデッドロックが起きた
そのデッドロックが成立する正確なイベント列を反例としてお返しします。シミュレーションが覆えないのは、事象の割り込み順序（インターリーブ）です。
2 つの軸が同時に動いても衝突しないと、組み上げる前に確かめたい
これは反例がそのまま答えになる質問です。確認と動作のあいだに相手の軸が割り込む場合まで含めて調べ尽くします。実物は 反例とは何か と、トップページに置いてあるトレースをご覧ください。
センサを読んで動く、その一瞬に値が変わったら
読み取りと動作のあいだが原子的でないときに生じる欠陥クラスです。そのすきまに割り込む順序を探し出します。
保守作業中の事故を、手順そのもので断てるのか
保守手順を状態とガードに移し、人が中にいる状態から起動に到達できる経路が残っていないかを確認します。
バイパス状態のまま正常運転に入るのを防げるか
バイパスの一生を状態として置き、解除されないまま運転・出荷に到達する経路があるかを調べます。
バッファを増やせば、待ちの詰まりは解消するのか
パラメータを振りながら同じ検査を回します。増やしても解消しない設計であれば、その事実を反例としてお見せします。
既存装置の改造で、もとの設計に由来する欠陥だけを指摘できるか
設計文書からシーケンスとインターロックを形式化して調べます。ソースコードからモデルを自動復元することは、現時点では提供していません。
うちが何日もかけてデバッグした本物のバグを、それで再現できるのか
そのバグが成立する設計上の条件をモデルに移し、同じ反例が出るかを確かめます。導入可否を判断する方法として、これがいちばん速いと考えています。
どの質問でも、返るものは同じです
お渡しするものは —— その問題が成立するイベント列そのものか、あるいは、取り決めた範囲においてそれが起こり得ないという確認です。どちらも、次の設計会議にそのまま持ち込める形でお渡しします。
上のどれかがご自身の質問なら、その質問ひとつでご相談ください。何を相談すべきか決まっていない段階でも構いません。
続けて読む
「起こり得ないという確認」がテストの「やってみたが起きなかった」と何が違うのかは テストと形式手法は、何が違うのか で扱います。
なぜこの調べ方が趣味の話ではなく規格の要求に入っているのかは なぜ安全規格は、形式手法を求めるのか にあります。