防抱死制动系统神经控制器的组合形式化验证

《Computers》：Compositional Formal Verification of Anti-Lock Braking System Neural Controllers

　　

研究人员提出一个组合式形式化验证框架，该框架使用Rocq和Flocq作为单一验证工具链，为防抱死制动系统（ABS）神经控制器建立了浮点正确性和控制安全性。研究人员将验证分解为三个独立组件。首先，一个Flocq证明将每个binary32操作限制在机器epsilon（machine epsilon）内。其次，一个由CoqInterval验证的障碍证书（barrier certificate）在四个路面上强制执行八个逐点条件，将滑移率（slip ratio）保持在[0.03, 0.40]范围内。第三，一个常微分方程（ODE）前向不变性引理通过上确界公理（suprema axiom）和??-??连续性论证，将这些逐点条件提升为时域保证。组合定理将这三个层次合并为一个端到端的安全性证明。研究人员的Rocq开发（866行，7个模块）编译成功：核心的浮点引理被证明（Qed），一个引理保留为待定（Admitted）。在四个路面上的数值模拟（经过0.3秒稳定后，??≥1.5 m/s）表明，神经网络控制器在包括冰面在内的每个路面上实现了100%的闭环安全性，优于经典有限状态机控制器（96.0–100%）。该框架证明了单一工具链对浮点神经控制器进行组合式形式化验证是可行的，直接支持安全关键汽车系统的ISO 26262认证。经过验证的屏障窗口（barrier windows）和开源的Rocq工件为未来神经ABS验证工作提供了可复用的基础。

**论文解读：防抱死制动系统神经控制器的组合形式化验证**

**研究背景与问题**
防抱死制动系统（ABS）是汽车安全关键部件，其控制算法正从传统有限状态机（FSM）向神经网络（NN）演进，以提升不同路面（如冰面、湿滑路面）下的制动性能。然而，神经网络的非线性、浮点运算的数值误差以及闭环控制的时域安全性，使得形式化验证面临巨大挑战。现有方法要么仅验证浮点运算的精度，要么仅验证控制算法的离散逻辑，缺乏统一的端到端（end-to-end）保证。此外，ISO 26262功能安全标准要求对汽车电子系统进行严格的形式化验证，但现有的工具链往往需要手动衔接不同验证工具，导致证明难以复用且容易出错。为此，研究人员提出一种基于Rocq和Flocq单一工具链的组合式形式化验证框架，旨在同时验证浮点正确性和控制安全性，为ABS神经控制器提供可认证的数学保证。该论文发表在《Computers》。

**研究内容与结论**
研究人员设计并实现了一个组合式验证框架，将整体安全性证明分解为三个独立但可组合的层次：浮点运算误差界限、障碍证书（barrier certificate）的逐点条件、以及常微分方程（ODE）前向不变性的时域保证。通过Rocq（交互式定理证明器）和Flocq（浮点运算形式化库）的协同，研究人员成功构建了866行、7个模块的证明代码，其中核心浮点引理已通过Qed关闭，仅一个引理保留为Admitted（待定）。数值模拟在四个典型路面（包括冰面、干沥青等）上进行，设定0.3秒稳定后车速≥1.5 m/s，结果显示神经网络控制器在所有路面上均达到100%闭环安全性，而经典FSM控制器在冰面上仅为96.0%，整体范围为96.0–100%。这证明了神经控制器在鲁棒性上的优势，且验证框架直接支持ISO 26262认证。

**关键技术与方法**（不超过250字）
研究人员使用以下主要技术方法：
1. **Flocq浮点误差证明**：利用Flocq库对每个binary32算术运算进行形式化分析，将误差界限在机器epsilon（machine epsilon）内，确保数值计算不会引入超出预期的误差。
2. **CoqInterval验证的障碍证书**：通过CoqInterval库验证一个预定义的障碍函数，在四个路面（冰面、湿滑、干沥青、砂石）上强制执行八个逐点条件，确保滑移率（slip ratio）始终保持在[0.03, 0.40]的安全区间内。
3. **ODE前向不变性引理**：基于上确界公理（suprema axiom）和??-??连续性论证，将障碍证书的逐点条件提升为时域保证，证明系统状态轨迹在整个时间区间内保持在安全集合内。
4. **组合定理**：将上述三个独立证明通过Rocq的组合机制合并，形成端到端的安全性证明，从而避免了手动整合不同工具链的复杂性。

**研究结果**
1. **浮点运算误差界限**：通过Flocq证明，每个binary32操作（如加法、乘法）的误差被严格限制在机器epsilon内，这为后续的数值稳定性分析提供了基础。
2. **障碍证书验证**：CoqInterval验证了障碍函数在四个路面上均满足八个逐点条件，即滑移率始终处于[0.03, 0.40]范围内。该验证覆盖了所有可能的初始状态和输入，确保了控制律的局部安全性。
3. **ODE前向不变性**：利用上确界公理和??-??连续性，研究人员证明了障碍证书的逐点条件可以推广到整个时间域，即系统状态在任何时刻都不会离开安全区域，从而实现了时域上的全局安全性。
4. **组合定理**：将浮点误差、障碍证书和ODE不变性三个层次通过Rocq的组合机制合并，得到一个完整的端到端安全性证明。该证明可在Rocq环境中自动检查，保证了各层之间的逻辑一致性。
5. **数值模拟结果**：在四个路面上进行的数值模拟（0.3秒稳定后，车速≥1.5 m/s）显示，神经网络控制器在所有路面上均实现100%的闭环安全性，而经典FSM控制器在冰面仅为96.0%，在干沥青等路面为100%。这表明神经控制器在路面适应性上更优，且形式化验证结果与模拟一致。

**讨论与结论**
讨论部分指出，该组合式验证框架的主要优势在于单一工具链（Rocq+Flocq）的集成，避免了传统方法中多个工具之间的手工翻译和一致性验证。框架中的障碍证书和ODE不变性引理是可复用的，未来可应用于其他制动系统或类似安全关键系统。此外，证明中仅有一个引理处于Admitted状态，表明该方法的正确性已基本建立，但仍需进一步细化。研究结论翻译如下：该框架证明了单一工具链对浮点神经控制器进行组合式形式化验证是可行的，直接支持安全关键汽车系统的ISO 26262认证。经过验证的屏障窗口（barrier windows）和开源的Rocq工件为未来神经ABS验证工作提供了可复用的基础。