[Paper] 基于模型的诊断与多重观测：面向 C 软件和布尔电路的统一方法

Source: arXiv - 2512.02898v1

概览

调试 C 程序和数字电路的成本极高，尤其是在涉及多个故障时。本文提出了 CFaults，一种新的故障定位工具，它将所有失败的测试用例统一为一个 MaxSAT 问题，能够为 C 代码和布尔电路提供一致的子集最小诊断。

主要贡献

• 统一的 MaxSAT 表述，一次性处理 多个观测（即所有失败的测试）。
• 基于模型的诊断（MBD）引擎，可无缝工作于 C 软件和布尔电路描述。
• 仅提供 子集最小诊断——消除以往 FBFL 工具中常见的冗余故障候选。
• 在三个基准套件（TCAS、C‑Pack‑IPAs、ISCAS85）上的 实证评估，显示对 C 程序的定位更快，对电路的性能具竞争力。
• 开源实现（CFaults），可集成到现有验证流水线中。

方法论

1. 程序/电路插装 – 将源代码（C）或网表（电路）翻译为命题模型，每条语句或每个门由布尔变量表示。
2. 观测编码 – 将每个失败的测试用例表达为必须被违反的一组约束。CFaults 不再对每个测试单独求解，而是 聚合 所有约束形成单一的 MaxSAT 公式。
3. 最大可满足性（MaxSAT）求解 – 求解器在尽可能满足约束的同时，最小化 被设为 true 的 “故障” 变量数量。最优解对应于最小集合的语句/门，修改这些即可使所有测试通过。
4. 诊断提取 – 将得到的赋值映射回原始源码，生成子集最小的可疑语句（或门）列表。
5. 迭代细化（可选） – 若开发者需要更多候选，CFaults 可以枚举次优解，每个解仍保证子集最小。

整个流水线自动化，仅需提供程序、测试套件以及一个 MaxSAT 求解器（如 Open‑WBO）。

结果与发现

关键要点

• 对软件而言，CFaults 在速度和提供干净、无冗余诊断方面始终优于最先进的 FBFL 工具。
• 在硬件基准上，虽然不是最快，但仍具竞争力，并提供高质量的最小诊断。
• 统一的 MaxSAT 方法消除了对每个测试单独求解的需求，降低了总体运行时间并简化了调试工作流。

实际意义

• 更快的缺陷分拣：开发者可以在一次运行中定位导致一组失败测试的精确语句，缩短 “搜索‑替换” 循环。
• 更清晰的输出：子集最小诊断意味着误报更少，减轻了工程师需要筛选冗余候选的认知负担。
• 跨领域适用性：从事嵌入式固件（C）和硬件验证（布尔电路）的团队可以使用同一工具链，促进软硬件协同设计的一致性。
• 集成潜力：CFaults 可挂接到 CI 流水线——在每次测试失败后运行，自动生成最小故障报告，甚至将结果馈送给自动程序修复工具。
• 可扩展性：借助现代 MaxSAT 求解器，该方法可扩展到中等规模代码库（数十万行代码）和实际电路基准，具备工业级可行性。

局限性与未来工作

• 电路性能：在大型布尔电路套件上，CFaults 略慢于专用硬件工具（如 HSD）；优化编码有望缩小差距。
• 故障模型：当前实现假设 语句级 故障；扩展到更细粒度（如表达式级）或更高层次（如 API 误用）将提升适用范围。
• 求解器依赖：诊断质量和速度依赖底层 MaxSAT 求解器；探索组合或混合求解策略可提升鲁棒性。
• 用户交互：目前 CFaults 输出的是静态的可疑列表。未来工作包括交互式调试辅助（如按执行频率对候选进行排序或与 IDE 集成）。

总体而言，CFaults 在软件与硬件统一、高效的故障定位方面迈出了重要一步，为开发者提供了一个将学术诊断理论与真实调试需求相结合的实用工具。

作者

• Pedro Orvalho
• Marta Kwiatkowska
• Mikoláš Janota
• Vasco Manquinho

论文信息

• arXiv ID: 2512.02898v1
• 分类: cs.SE, cs.AI, cs.LO, cs.SC
• 发表时间: 2025 年 12 月 2 日
• PDF: Download PDF