クリーンルーム手法
クリーンルーム手法とは、ひとことで言えば、形式手法と統計的品質管理を組み合わせ、ソフトウェアの欠陥を未然に防ぐことを目的とした開発手法です。IBMのHarlan Millsらが提唱し、半導体製造のクリーンルームになぞらえて命名されました。コードを書く前に数学的な仕様記述で正しさを証明し、テスト段階では統計的サンプリングで信頼性を測定します。開発者はデバッグを行わず、設計段階で欠陥混入を防ぐことに注力します。航空宇宙や軍事システムなど、極めて高い信頼性が求められる分野で採用されており、結果としてセキュリティバグも極小化されます。

