[Paper] 从一开始就持续检查 HAL 接口规范

Source: arXiv - 2512.16897v1

概述

本文解决了嵌入式开发者长期面临的一个痛点：确保对硬件抽象层 (HAL) 的调用永不违背供应商规定的合约。作者提出了一种 连续、逐步的模型检查工作流，该工作流从一个极简的骨架开始，在每一次增量代码添加后验证 HAL 接口，从而显著降低了“一刀切”不确定性，这也是形式化验证一直未能进入大多数生产流水线的主要原因。

关键贡献

• 增量验证循环：引入一种实用的流程，在每次开发迭代后检查 HAL 规范，而不是仅在结束时检查。
• 跨步骤的抽象复用：展示如何将软件模型检查器计算得到的抽象向前传递，使后续检查更便宜且更可预测。
• 原型实现与实证证据：在真实的嵌入式项目上进行初步评估，证明该检查在每一次迭代中（包括最终产品）都能成功。
• 工业采纳指南：提供具体建议（例如骨架创建、迭代粒度），弥合学术模型检查与日常嵌入式开发之间的差距。

方法论

1. 骨架创建 – 开发者从仅包含 HAL 函数调用（无业务逻辑）的最小程序开始。
2. 迭代丰富 – 在每个开发冲刺中，向骨架添加一小块功能（例如传感器读取、控制循环）。
3. 模型检查步骤 – 每次添加后，调用现成的软件模型检查器（如 CPAchecker、CBMC）来验证 HAL 的使用仍然符合形式化接口规范（前置条件、后置条件、资源约束）。
4. 抽象继承 – 检查器为上一步构建的抽象（例如谓词集合、抽象域）被复用作为下一步的起点，避免完整重新计算。
5. 反馈循环 – 若检查失败，开发者会收到精确的反例，指出违规的 HAL 调用，从而在添加更多代码之前立即纠正。

该方法刻意 不需要形式化的链接（例如版本控制钩子）在迭代之间；连续性纯粹通过复用模型检查器的内部抽象实现。

结果与发现

• 每次迭代均成功：在作者的案例研究（一个电机控制驱动和一个传感器融合模块）中，HAL 规范在每一次增量修改后都得到了验证，最终形成了一个完全验证的最终程序。
• 性能提升：复用抽象层平均将验证时间缩短了 30‑50 %，相较于对每一步进行全新检查。
• 早期缺陷检测：大多数违规在第一或第二次迭代中就被捕获，避免了后期开发周期中代价高昂的重新设计。
• 开发者接受度：参与者报告说，增量检查感觉“自然”，并且非常契合敏捷冲刺的工作方式，而不像在最后进行一次整体验证那样笨重。

实际意义

• 可预测的 CI 流水线：团队可以将 HAL‑check 嵌入持续集成的轻量级阶段，确保每次运行都能快速结束，要么通过，要么生成可操作的反例。
• 缩短上市时间：提前发现 HAL 的误用，可避免在产品周期后期出现昂贵的硬件调试。
• 更安全的 OTA 更新：在推送固件更新时，开发者只需对修改的模块重新运行增量检查，确保新代码仍然遵守 HAL 合约，而无需重新验证整个系统。
• 供应商无关的安全性：该方法适用于任何拥有形式化规范的 HAL（如 AUTOSAR、Zephyr），可在不同平台之间重复使用，形成通用的安全网。

限制与未来工作

• 范围仅限于 HAL 接口：该技术假设存在一个定义明确、形式化规范的 HAL；将其扩展到任意 API 或混合语言栈需要额外的工具支持。
• 抽象漂移：在非常大的代码库中，复用的抽象可能变得过于粗糙或过于细致，可能导致性能下降；自适应抽象细化是一个未解决的研究方向。
• 初步评估：实验仅涉及两个案例研究；需要更广泛的工业试验来确认可扩展性和集成开销。
• 工具链集成：当前原型依赖手动调用模型检查器；未来工作旨在在流行的 IDE 和 CI 系统（如 GitHub Actions、Jenkins）中实现自动化循环。

通过将形式化验证转变为持续、增量的习惯，本工作为在不牺牲开发者敏捷性的前提下实现更可靠的嵌入式软件铺平了道路。

作者

• Manuel Bentele
• Onur Altinordu
• Jan Körner
• Andreas Podelski
• Axel Sikora

Paper Information

• arXiv ID: 2512.16897v1
• Categories: cs.LO, cs.SE
• Published: 2025年12月18日
• PDF: Download PDF