7.3 形式化验证入门

7.3 形式化验证入门

本节摘要：测试只能证明"试过的没出错"，形式化验证证明"所有可能情况都不会出某类错"。本节以"输出永远不越过安全包线"为例，走一遍性质证明的完整流程：写性质、跑证明、读反例、修复再证。重点训练反例的阅读能力——一个反例比一份通过报告信息量大得多。本节也划清了形式化的能力边界：它证明的是写出来的性质，不是模型的所有方面。

测试的根本局限

7.2 节的覆盖率再高，也改变不了一个事实：测试采样的只是输入空间里有限个点。保护逻辑的计时阈值、负载突变的发生时刻、参数漂移的组合——输入空间是连续且近乎无限的，而"出事"可能恰好藏在没采到的那个点上。航空、汽车功能安全领域因此把形式化验证写进了推荐流程：用数学方法证明性质在全部输入下成立，让"没试到"不再等于"不知道"。

Simulink 家族里的形式化工具（Design Verifier 一类）把这件事自动化：把模型与性质翻译成逻辑公式，交给证明引擎（模型检验类的算法）在状态空间里系统搜索——找到一条违反性质的路径就交给你一个反例；搜遍状态空间找不到，就给你"性质成立"的证明结论。

性质的写法：从安全需求到证明目标

性质必须写成机器可判定的形式，常见三类模板。不变式：任何时刻都成立，如"切断态下输出恒为零"。可达性（用于负面场景）：存在某条路径到达某状态，常用于证明"某坏状态不可达"，即证其否。时序性质：带先后关系，如"告警后 60 毫秒内必然进入切断或回落运行"。

小林的验收单上有一条："告警态若 50 毫秒内未消除，必须进入切断态。"写成证明目标：从告警态出发，所有路径上 dwell 计时到达 50 毫秒时必处于切断态（或已先行回落）。注意性质里藏着两个前提——计时器按控制节拍递增、迁移条件与规格一致——性质证明的是"模型相对于性质的实现"，规格本身错了，证明通过也白搭。这一点是形式化验证最常见的误用。

% 证明目标登记表（交付证据链的一部分）
目标 PV-07：
  性质：从告警态出发，dwell 到达 50毫秒 的所有执行路径
        下一拍必处于 切断态 或 运行态（回落情形）
  前提：控制节拍 1毫秒 恒定；迁移条件按 5.1 节迁移表
  结果：见下文证明会话
​

跑证明与读反例

证明会话的两种结局，价值密度完全不同。结局一：报告不可达或成立——性质在前提范围内恒真，这份结论进入证据链，对应验收单的"关键性质保证"栏。结局二：给出反例——引擎找到一条从初始状态到违规点的具体路径，附带每一步的状态与信号值。反例是金子：它是一份"错误的最小复现说明书"，按图索骥在仿真里重放，肉眼确认违规瞬间，然后回头查根因——规格歧义、建模疏漏、还是性质本身写错了。

小林第一次跑 PV-07 拿到的就是反例：路径显示告警态下 dwell 计时只到 49 毫秒，系统就被"电流回落"迁移拉回了运行态，50 毫秒切断从未触发——这恰好暴露了规格歧义：需求写"告警持续满 50 毫秒进入切断"，但没定义"告警期间电流反复抖动、计时要不要清零"的语义。反例推动的不是改模型，而是回修规格：明确计时策略（抖动场景采用不清零的滑动窗计时），改完规格改模型，再证通过。

能力边界与成本管理

形式化不是万能证明机，三条边界要心里有数。边界一：只证写出的性质。没写进目标的坏性质，通过了也不被覆盖——性质清单的完备性靠安全分析（FMEA、危害分析）喂给，不靠证明引擎自己长出来。边界二：状态空间爆炸。模型里连续状态、宽位计数器、长时序依赖越多，证明越慢甚至不可完成；工程折中是抽出逻辑部分单独证明（保护状态机适合，连续动力学不适合），连续域的正确性仍靠仿真与理论分析。边界三：前提即边界。所有结论限定在前提假设内，节拍变了、前提破了，证明结论作废——前提清单要与模型配置联动管理（6.1 节的字典正好托管这些假设参数）。

成本管理的经验法则：把形式化留给"低频高危"的逻辑性质——保护联锁、模式切换、故障降级路径。这类性质数量少（一个项目十来条）、后果重、恰好是证明引擎的甜区；拿它去证控制律的动态品质，是用错了手术刀。

⚠️ 常见坑：把"证明通过"当"模型无 bug"。性质清单外的缺陷（数值精度、控制品质、参数敏感性）形式化一概不保。证据链里它只占"关键逻辑性质"一栏，别替它吹成全保书。

常见问题

问：证明跑不动了（状态空间爆炸），有什么工程上的退路？

三条退路按代价排序。抽象化简：把与性质无关的细节先剥离——证明保护逻辑时，电机模型可以退化成"电流是有界输入"这一条假设，状态空间骤减；证明完再把假设交给连续域仿真去背书。分而治之：一个大的时序性质拆成几条小的局部性质分别证明，覆盖面等价、单条难度骤降。降维采样：实在证不动的部分退回"超长时程随机仿真加边界扫描"，明示这是折中而非证明。退路的共同前提是把"证明了什么、没证明什么"写清楚进证据链——折中可以，含糊不行。

问：性质证明通过后，模型改动需要重新证明吗？

按改动影响面决定。性质覆盖范围内的逻辑（状态机、迁移条件、保护动作）动了，必须重证——证明结论绑定的是"当时的模型加前提"。性质范围外的改动（对象参数、求解器配置），评估前提假设是否仍成立（节拍没变、信号界没破），成立则引用原结论并记录评估。这与 7.2 节等效性测试的触发逻辑一致：改动与结论之间的绑定关系，要显式管理而不是凭感觉续期。

本节要点回顾

• 测试与证明的分工：测试覆盖采样点，证明覆盖全部输入空间，安全关键两者都要；
• 三类性质模板：不变式、可达性、时序性质，安全需求先翻译成机器可判定形式；
• 性质证的是实现不是规格：规格错了，通过也白搭——反例常把矛头指回规格；
• 反例是最小复现：按路径重放、定位瞬间、根因三分类（规格、模型、性质）后再证；
• 三条边界：只证写出的、警惕状态爆炸、前提即有效期；
• 成本投向低频高危：保护联锁与模式切换类逻辑性质是证明引擎的甜区。

到此，模型的"体检报告"齐了：规范符合、覆盖达标、性质有证。下一章它要走最后一程——变成在处理器上真实运行的代码。