FS-B7 — 三类证据闭合:为什么概率、逻辑、实测缺一不可,以及它们如何在 Safety Case 的 GSN 树上组装成一句"SG 满足"

更新

本质与导读

专家养成 · 模块一(功能安全B 阶第 7 讲,B 阶收官。前六讲我们把 B 阶的量化机器一件件造齐:FS-B1 的 FMEDA 失效率分配、FS-B2 的诊断覆盖率 DC、FS-B3 的 FTA 最小割集、FS-B4 的 ASIL 分解、FS-B5 的共因 、FS-B6 把前面所有散数收进 SPFM/LFM/PMHF 三个可验收的数。但到 FS-B6 结尾必须承认一件事:这三个数只是一类证据——概率证据。一个 ASIL D 的 Safety Case,光有概率证据是不成立的。今天这一讲不再造新工具,而是回答一个更根上的问题:要证明"安全目标 SG 满足"这句话,到底需要几类证据、为什么恰好是三类、它们又如何在 GSN 论证树上闭合成一个不悬空的结论。 这是把 B 阶所有零件装回 FS-A1 那条上行聚合链的最后一步。

开篇:硬约束——"SG 满足"是一句无法直接证明的话,只能靠证据组装

回到 FS-A1 立下的骨架:功能安全的上行链,是把"整车够安全"这个回答不了的大命题,逐级聚合证据、论证回"SG 满足"。到了器件层、算完 FMEDA,很多工程师以为"SPFM 99.2% ≥ 99%,过了,SG 就满足了"。这是本讲要拆掉的第一个错觉。

为什么一个达标的百分比不等于"SG 满足"?因为**"SG 满足"是一句关于物理系统的断言,而任何单一证据都只能照亮这句断言可能出错的一个面**。FMEDA 的 99% 建立在两个未经它自己证明的前提上:一是它假设了每个 SM 的诊断覆盖率(DC 是输入,不是 FMEDA 算出来的);二是它假设自己把失效模式枚举全了(bottom-up 的固有盲区——没列进表的失效模式,概率再低也进不了分母)。这两个前提一旦有一个是假的,那个漂亮的 99% 就是建在沙子上的数字。

所以硬约束是:"SG 满足"这个结论,其否证方式不止一种,故其支撑证据也必须不止一类。有几种独立的方式让这句话变成假的,就至少需要几类证据分别把这些否证路径堵死。 本讲先从第一性原理推出"为什么恰好三类",再逐类看它证明什么、盲区在哪、被谁补上,最后看 GSN 树如何把三类证据组装成一个逻辑上闭合、审计员挑不出悬空点的 argument。


中段一:第一性推导——一个安全断言有三种独立的出错方式,故需三类证据

不要从"标准要求 FMEDA + FTA + 测试"这个结论倒背。正着推:断言"这个硬件满足 SG"要为真,必须同时扛住三种彼此独立、无法互相替代的质疑。逐一逼出来:

质疑一:"就算你列的故障都罕见,剩余的危险失效率整体够低吗?" 这是一个关于总量与概率的问题。哪怕每个失效模式都被覆盖得不错,成千上万个模式的残余危险率累加起来仍可能超标。回答它,只能靠自底向上、逐模式累加失效率的定量方法——这正是 FMEDA 给出的概率证据(SPFM/LFM/PMHF)。它回答的是"够不够罕见"。

质疑二:"你自底向上一个个列模式,会不会漏了某条一步捅穿 SG 的结构路径?" 这是一个关于结构与逻辑的问题,而且方向和质疑一相反。FMEDA 的 bottom-up 视角天生看不见"多个部件如何组合出一条通往顶事件的路"——它的盲区正是没被枚举进表的组合。回答它,只能靠自顶向下、从危害顶事件回溯的演绎方法:FTA 与最小割集(FS-B3),它枚举出"哪些故障组合能致顶事件",一阶割集就是致命单点。它回答的是"有没有致命的结构路径"。

质疑三:"你 FMEDA 里给每个 SM 记的那个 DC=99%,凭什么相信它在真实故障来临时真会触发、真会在 FTTI 内切到安全态?" 这是一个关于前提真伪的问题。DC 是 FMEDA 拿来当输入 credit 的假设,而假设本身不能用消费这个假设的同一套计算去证明——那是循环论证。回答它,只能靠真往系统里注入故障、用示波器看 SM 到底动没动的经验方法:Fault Injection(FI)。它回答的是"假设的机制是不是真有效"。

三个质疑对应三条独立的否证路径:概率不足、结构有洞、前提落空。它们无法互相替代——FTA 证不了总量够低(它不加失效率),FMEDA 证不了没漏结构(它自底向上),两者都证不了 SM 真会动(它们都在纸上算)。于是第一性原理逼出结论:"SG 满足"至少需要概率、逻辑、实测三类证据,一类堵一条否证路径,这不是标准的清单式规定,是"一个断言有三种独立死法"的数学后果。 这也解释了为什么 ISO 26262 对 ASIL C/D 同时要求归纳分析(FMEDA)、演绎分析(据 ISO 26262-5,FTA 类演绎分析对 ASIL C/D 为推荐/highly recommended,补 FMEDA 的 bottom-up 盲区)与故障注入验证。


中段二:概率证据——证"够罕见",盲区是"假设为真"

概率证据就是 FS-B6 收束的 SPFM/LFM/PMHF。它的力量在于把成千上万个失效模式的危险贡献加总成可比对门槛的数,给出"这个架构对随机硬件失效整体够不够硬"的定量回答——这是逻辑和实测都给不了的。

但它有两个自己证明不了的盲区,恰恰是后两类证据存在的理由:

其一,DC 是输入不是输出。 FMEDA 表里每个 SM 那一栏的诊断覆盖率,是工程师依据 SM 类型 claim 进去的假设值(FS-B2 讲的"怎么 claim DC")。FMEDA 用这个假设算出 SPFM,但它没有、也不能验证这个假设为真——用被除数去证明除数,是循环。这个盲区留给实测证据(FI)。

其二,枚举完整性无法自证。 SPFM 的分母是"我列进表的所有失效率",但"我有没有列全"这件事,bottom-up 方法在原理上回答不了——你不知道自己不知道的那条路径。这个盲区留给逻辑证据(FTA 从顶事件反向兜底)。

所以概率证据的真实地位是:它回答"够不够罕见",但它的可信度本身依赖另外两类证据把它的两个前提撑住。 把 FMEDA 当成 Safety Case 的全部,等于把整栋楼盖在两根没人检查过的假设柱子上。


中段三:逻辑证据——FTA 从顶事件兜住 FMEDA 的枚举盲区

逻辑证据是 FS-B3 的 FTA 与最小割集。它和 FMEDA 是一对方向相反、互补兜底的分析:FMEDA 自底向上(部件失效 → 效应),FTA 自顶向下(危害顶事件 → 哪些故障组合能致它)。为什么必须两个方向都做?因为一个方向的盲区,恰是另一个方向的正视区。

FMEDA 逐部件列模式,漏的是"跨部件的组合路径";FTA 从顶事件演绎割集,天然会把"哪几个部件一起坏就能捅穿 SG"逼出来——一阶最小割集(单个基本事件即致顶事件)就是致命单点故障,这正是 FMEDA 若枚举不全就会漏掉的东西。反过来 FTA 的短板是它不天然带失效率、给不出总量,于是 FMEDA 把随机硬件失效率喂给 FTA 的底事件、FTA 把结构约束反馈给 FMEDA——工程上两者是互相供数的闭环(据行业实践,FTA 底事件取 FMEDA 的随机失效率、FMEDA 从 FTA 割集获得结构性设计要求)。

所以逻辑证据回答的是"有没有致命的结构路径",它兜住的是概率证据的枚举盲区。 但注意 FTA 同样有它证不到的地方:它证明了"结构上没有一步捅穿的路径",却证不了那些拦路的 SM 真的会动——割集里写着"SM 失效"是一个逻辑节点,这个节点的真实失效行为,仍要靠实测。三类证据的盲区就是这样环环相扣、彼此指向下一类。


中段四:实测证据——Fault Injection 是安全工程的 maker≠checker

实测证据是 Fault Injection:真往运行中的系统注入故障(短路一个节点、拉偏一路电压、翻转一个 bit),用示波器 / HIL 记录 SM 到底有没有检出、有没有在 FTTI(FS-A3)内把系统切到安全态。它是三类证据里唯一碰真实物理的一类,也是最不可省的一类。

它的第一性地位,用本项目反复强调的 maker≠checker 一句话点破:FMEDA 是 maker——它声称每个 SM 有 99% 的诊断覆盖率;FI 是 checker——它独立地去验证这个声称是不是真的。让写 FMEDA 的人用 FMEDA 自己证明 FMEDA 的 DC 假设,就是让 maker 给自己判卷。FI 的全部价值,就在于它是一条独立于 FMEDA 计算之外的证据链:它不接受"DC=99%"这个纸面数字,它去看那 99% 在硬件上兑不兑现。

这解释了一个新手常忽略的因果:FI 验证的恰恰是 FMEDA 的输入前提,而不是 FMEDA 的输出结论。 你不是用 FI 去"复核 SPFM 算得对不对"(那是算术),而是用 FI 去打掉"DC 假设可能为假"这条否证路径——注入真故障,若 SM 未在 FTTI 内动作,则 FMEDA 里那一栏 DC 就是伪证,整个 SPFM 连带崩塌。据 ISO 26262-5,故障注入对 ASIL C/D 硬件的安全机制验证为 highly recommended。所以实测证据回答的是"假设的机制是不是真有效",它把概率证据悬空的那根 DC 柱子钉进物理地基。 至此三类证据各就各位:概率证够罕见、逻辑证无致命结构、实测证机制真动——三条否证路径全部被堵。


中段五:GSN 树——把三类证据组装成"SG 满足"的逻辑骨架,以及"闭合"到底指什么

三类证据齐了,还差最后一步:把它们组装成一句"SG 满足"。散着的三份报告不构成 argument——审计员要看的是"这三份东西如何逻辑地蕴含 SG 满足"。承担这个组装的,就是 Safety Case 的 GSN(Goal Structuring Notation)论证树。

GSN 的因果作用,是给"证据 → 结论"这条跳跃补上中间的推理。它靠两类关键节点:Strategy(策略)节点写明"我凭什么方法把大 claim 拆成小 claim"——比如"按 ISO 26262-9 三故障类拆解,随机 + 系统 + 共因三个子目标联合蕴含 SG";Solution(证据)节点是唯一直接挂证据的叶子,概率证据(FMEDA report)、逻辑证据(FTA/DFA report)、实测证据(FI/V&V report)各挂在对应子目标下。三类证据不是平铺,而是被 Strategy 编织进一棵从 SG 顶目标逐级下推、到证据叶子终止的树(完整 7 步写法与 30 节点 worked 见 Safety Case GSN 写作深度)。

关键是理解"闭合"这个词的确切含义。一棵 GSN 树闭合,当且仅当:每一条从顶目标出发的推理路径,都终止在一个挂了真实证据 ID 的 Solution 叶子上,且没有任何假设(Assumption)悬空未回闭。 反过来,只要有一处证据悬空——引用了一份不存在的报告、一个假设了却从未验证的 DC、一条挂了 FMEDA 却缺 FI 兜底的 SM——这棵树就不闭合

这里必须接回 FS-A1 那句"链断一环即不成立":GSN 树的不闭合,不是"论证弱一点、扣几分",而是逻辑上不再成立。因为根结论"SG 满足"靠下层每个节点支撑,任何一处支撑悬空,支撑关系就断了,根结论失去依据——这是逻辑的全有全无,不是工程的程度问题。一份缺了 FI 实测的 Safety Case,哪怕 FMEDA 和 FTA 都完美,它论证的也只是"如果 SM 假设成立则 SG 满足",而那个"如果"正是最该被质疑、也最容易假的地方。三类证据缺任一类,GSN 就必然在某个子目标下留一个无法回闭的假设——这就是"缺一环 Safety Case 不成立"在证据层的精确机制。


落到工程结论:三类证据的组装流程 + 三条准则

把 B 阶所有零件装回上行链,得到一套可执行的证据闭合流程。给定一个 SG:

  1. 建 GSN 骨架:Top Goal 一字不差等于 SG 文本,用 Strategy 按三故障类(随机 / 系统 / 共因)拆出子目标——这一步决定三类证据各挂哪里。
  2. 概率证据填随机故障子目标:FMEDA 算出 SPFM/LFM/PMHF,对照 ASIL 门槛(D:99% / 90% / 10 FIT),挂 Solution + report ID。
  3. 逻辑证据兜结构:FTA 从顶事件演绎最小割集,确认无一阶割集(致命单点);把随机失效率喂给底事件,与 FMEDA 互相供数。
  4. 实测证据钉前提:对每个被 FMEDA credit 了 DC 的 SM,设计 FI 用例,HIL/bench 注入真故障、示波器核 SM 在 FTTI 内切到安全态——把 DC 假设从纸面钉进物理。
  5. 查闭合:沿树自顶向下抽查每条路径是否终止于有 ID 的证据叶、每个 Assumption(尤其 DC、失效率库、SEooC 的 AoU)是否有 verification 回闭;有悬空即未闭合,补证据或显式标 Residual Risk。

带走三条准则:

  1. 三类证据堵三条独立否证路径,不能互相替代。 概率证"够罕见"、逻辑证"无致命结构"、实测证"机制真有效";少一类,就有一条让"SG 满足"变假的路径没被堵死。达标的 SPFM 只堵了第一条。
  2. FI 验证的是 FMEDA 的输入前提,不是它的输出结论。 DC 是 FMEDA 的假设(maker),FI 是独立的验证(checker);让 FMEDA 自证 DC 是循环论证。安全工程的 maker≠checker,落点就在这里。
  3. "闭合"是全有全无,不是程度。 GSN 树只要有一处证据悬空 / 假设未回闭,根结论"SG 满足"就逻辑上不成立——这正是 FS-A1"断一环即不成立"在证据层的精确形态。

承上启下:B 阶到此收官

承上启下:B 阶到此收官。我们从 FS-B1 的失效率一路造到 FS-B6 的三个度量,今天把它们连同 FTA 的逻辑证据、FI 的实测证据,一起装进 GSN 树,闭合成一句"SG 满足"——概率证够罕见、逻辑证无致命结构、实测证机制真动,三类缺一即树不闭合、Safety Case 不成立。但 B 阶算的、证的,都还停在"证据齐不齐"的层面;真正的工程难点在兑现:那个被 FMEDA claim 了 99% SPFM 的 Lockstep 双核,物理上到底怎么做到 99% 的?下一讲 FS-C1(C 阶进阶工程实现开篇)拆 Lockstep 如何真兑现 99% SPFM——双核比对的物理、CCC(共因)约束、单核 PMHF 的硬边界,正是本讲"实测证据要去验证的那个 SM"落到最硬核的一个实例。预热可读 Lockstep 双核深度


延伸阅读