EQ-Robin：多最小唯一原因 MC/DC 测试套件的约束韧性生成
软件工程
2026-02-10 v2
摘要
唯一原因修改条件/决策覆盖 (MC/DC) 在安全关键验证中广泛要求。最近的确定性算法 Robin's Rule 可为单一布尔表达式 (SBE) 构造理论最小的 N+1 个测试案例，提供了当所有生成的测试向量可执行时强有力的保证。然而，工业系统会施加可行性约束：一些输入组合是非法的、不可实现的，或不可安全执行的。如果单个非法向量出现在最小套件中，它会破坏所需的独立配对并使 100% 唯一原因 MC/DC 失效，尽管底层决策逻辑保持不变。本文提出了 EQ-Robin，一个轻量级、约束韧性的管道，生成一族最小 (N+1) 唯一原因 MC/DC 测试套件并选择满足域约束的可行套件。EQ-Robin 通过对表达式抽象语法树 (AST) 应用代数重排，系统性地枚举语义等价但结构不同的 SBE。由于 Robin's Rule 对结构顺序敏感，每个变体产生不同的最小套件。EQ-Robin 然后使用实用约束检查和成本启发式（如设置成本、oracle 复杂度）对候选套件进行过滤和排序。为确保大规模可用性，我们引入了预算受限的探索模式（提前退出、引导重排）以及当给定约束下无完全可行的 N+1 套件时备用的修复策略。我们在 TCAS-II 派生的表达式上演示了核心故障模式和恢复机制，并概述了在代表工业可行性限制的约束情景下对 EQ-Robin 在 TCAS-II SBE 上的实证评估。
引用
@article{arxiv.2509.26458,
title = {EQ-Robin: Constraint-Resilient Generation of Multiple Minimal Unique-Cause MC/DC Test Suites},
author = {Robin Lee and Youngho Nam},
journal= {arXiv preprint arXiv:2509.26458},
year = {2026}
}
备注
11 pages, 4 figures