システムにおける「許容される安全性」とは

safety-criticalsystems-engineering

DO-178C / ISO 26262 / IEC 62304 の3基準を横断して読むと、業界が実際に「安全」と呼んでいるものの正体が見える。安全 = バグゼロでも事故ゼロでもなく、「危害の大きさに見合うまで定量的に下げた残存リスク + それを第三者が監査できる証跡」。エンジニアリングとしての含意を8点に抽出する。

1. 安全は確率で定義される(ゼロではない)

DO-178C の Catastrophic は 故障率 ≤ 10⁻⁹/飛行時間。これは「10億飛行時間に1回未満の致命故障」で、歴史的な「全機隊の生涯で致命事故 ≤1回」という許容から逆算された数字。業界は明示的に非ゼロの故障率を受け入れている。「絶対安全」は要求されていない — 結果の重さに対して十分に稀、が安全の定義。

2. リスクに比例した傾斜配分

DAL / ASIL / Safety Class はすべて同じ思想 — 被害が大きいほど厳格に、小さければ緩く。すべてを均等に検証しない。S×E×C(ISO)、故障条件の重大度(DO)、危害クラス(IEC)は同じ「consequence でメリハリをつける」原則の別表現。検証リソースは有限なので、どこに費やすかの配分こそが工学判断。

3. プロセス > プロダクト

認証が監査するのは成果物だけでなく作り方(要件レビュー・構成管理・独立性・トレーサビリティ)。理由は深い — 一般のソフトの正しさは証明不能だから、「正しい」の代わりに「正しく作った証跡」を要求する。成果物の正しさを直接示せない領域で、プロセスが信頼の代理になっている。

4. システム安全はアーキテクチャで作る(コードだけではない)

最も「システム」な点。単一故障で死なせない設計 — 冗長・独立・モニタ・fail-safe 状態。ISO の ASIL 分解(要求を独立な要素へ冗長配分し各要素の ASIL を下げる)が象徴的で、安全はバグの無いコードからではなく故障しても安全側に倒れる構造から生まれる。だからソフトの DAL/クラスは、上位のシステムハザード解析から割り当てられる(DO-178C は ARP4754A/4761 の下流、62304 は ISO 14971 の中)。

5. カバレッジ = 「漏れが無い」の証明

テストの基準は「通った」ではなく「試していない論理が無い」。MC/DC(各条件が単独で判定を左右することを示す)は、テストの存在ではなく抜けの不在を要求する。安全臨界では「動いた」は証拠にならない。

6. 責任範囲は依存物まで及ぶ

コンパイラ・OS・ランタイム・ツールも検証対象。SOUP(出自不明ソフト, IEC)、tool qualification(DO-330)は、「信頼を外注できない」ことの強制。使う部品すべてに正当化が要る。→ WASM ランタイムは典型的な SOUP。

7. トレーサビリティ — すべてが要求に紐づく

要求 → 設計 → 実装 → テストが全部繋がっていること。根拠なく存在するコード/機能は許されない。「なんとなく入れた」は監査で落ちる。

8. 独立検証

検証者 ≠ 実装者(DAL A は独立性必須)。自己検証は信頼されない。

つまり、業界が許容する安全性とは

安全 = f(危害の大きさ)
     ① 残存故障率を consequence に見合うレベルまで下げ(定量目標)
     ② それをアーキテクチャ(冗長・独立・fail-safe)で達成し
     ③ プロセス・証跡・独立検証で「達成した」を第三者に示す

「bug-free」は誰も要求していないし、できない。代わりに “管理されたリスク” を “監査可能な形で” 示すゲーム。

Almide の機械証明はどこに効くか

Perceus の機械証明は ①(全入力で性質が成り立つ=確率でなく証明)と ⑤(網羅の最上位) を直撃する — coverage より強い保証。だが ③ プロセス・④ アーキテクチャ冗長・⑥ ランタイム・⑦ トレーサビリティ・⑧ 独立検証には触れない。つまり形式証明は8本柱の1本で、強力だが単独では認証に届かない。ギャップ分析の「言語の保証 ≠ 認証」はここに起因する。

関連

Graph

Backlinks