6.3 形式化验证 (Design Verifier)

文档摘要

6.3 形式化验证 (Design Verifier) 6.3 形式化验证（Design Verifier）：从直觉信任到数学确信的范式跃迁在工程实践的漫长演进中，我们曾习惯于用“跑通了”来宣告一个控制算法的诞生；用“仿真没报错”来宽慰自己模型逻辑大体无虞；用“覆盖率达到85%”来为测试画上阶段性句号。然而，当一辆L4级自动驾驶车辆在暴雨夜驶过未被标注的施工锥桶阵列，当一台植入式心脏起搏器因状态机跳转异常而延迟输出脉冲，当航天器姿控系统在深空通信中断窗口内误判姿态误差方向——那些曾经被我们称为“足够好”的经验性判断，瞬间坍缩为无法承受之重。此时，问题已不再关乎“是否工作”，而在于“能否证明其必然不致害”。