DO-178C (航空ソフトウェア認証)

safety-critical formal-methods

民間航空の搭載ソフトウェアを認証するためのガイダンス。RTCA(米)と EUROCAE(欧、欧州名 ED-12C)が共同維持。「動く」ではなく「安全影響に見合った信頼性が示されている」ことを目標(objective)達成で証明させる。安全臨界認証の航空版。

DAL — 故障の重大度で厳格度が決まる

Design Assurance Level。故障が起きたときの被害の大きさで5段階。レベルが上がるほど達成すべき objective が増える。

DAL	故障条件	許容故障率(/h)	objectives	必要なカバレッジ
A	Catastrophic(機体喪失)	≤ 1×10⁻⁹	71	MC/DC
B	Hazardous	≤ 1×10⁻⁷	69	decision
C	Major	≤ 1×10⁻⁵	62	decision
D	Minor	—	26	statement
E	No effect	—	0	なし

カバレッジの3層

テストがコードをどれだけ網羅したかの基準。DAL が上がるほど厳しくなる。

statement coverage — 全行を1回は実行
decision coverage — 各分岐を true/false 両方
MC/DC (Modified Condition/Decision Coverage) — 各条件が単独で判定結果を左右することを示す。DAL A 必須で、安全臨界テストの最高基準

プロセス領域

objective は6領域に渡る: 計画 / 開発 / 検証 / 構成管理 / 品質保証 / 認証連絡(certification liaison)。何をすべきか(objective)を定め、どうやるかは規定しない objective-driven な点が特徴。

システムへの含意 — DAL は「上」から降ってくる

DO-178C はソフト単体の標準だが、DAL を自分で決めるのではない。航空機システムの安全性評価(ARP4754A の機能ハザード評価、ARP4761 の FHA/PSSA)が「この機能が誤ると Catastrophic か」を判定し、そこからソフトの DAL が割り当てられる。

含意は2つ:

ソフトの厳格度はシステム設計の帰結であって、コード品質を上げれば下がるものではない。
だからアーキテクチャで DAL を下げられる — 冗長化や独立モニタで「単一ソフトの誤りが Catastrophic に至らない」構造にすれば、各ソフトに要求される DAL は緩む(ASIL 分解と同じ発想)。安全はアーキテクチャで作るの典型。

補遺(Almide に効くもの)

補遺	内容
DO-330	ツール認定(tool qualification)
DO-331	モデルベース開発
DO-332	オブジェクト指向技術
DO-333	形式手法 — 定理証明・モデル検査を動的テストの補完/代替として認める

DO-333 が重要 — 機械証明を認証エビデンスにできる枠組みがある。Almide の Perceus 機械証明はここに接続しうる(ただし MC/DC 相当の網羅と E2E 証明連鎖が別途要る)。