商用ソフトウェアにおける形式検証:現場レポート

形式検証には評判があります:学術的には美しいが、商業的には無関係、と。本番の決済照合エンジンに適用したのち、私たちは異を唱えます — 但し書き付きで。

そのエンジンには一万一千のテストと二年間の無事故の履歴がありました。それでも中核の状態機械のモデル検査は、四つの潜在的欠陥を露わにしました。いずれも、どのテストも構成せず本番がまだ引き当てていなかった、リトライと部分的失敗の精密な絡み合いを要するものでした。

但し書きは範囲です。システム全体の検証は経済的に馬鹿げていたでしょう;お金が動く二百行の検証は三週間で済み、最初の発見で元が取れました。これが私たちがいま推奨するパターンです:形式手法をメスとして、失敗が許容できない場所にちょうど当てる。