Unique-Cause Modified Condition/Decision Coverage (MC/DC) is widely required in safety-critical verification. A recent deterministic algorithm, Robin's Rule, constructs the theoretical minimum of N+1 test cases for Singular Boolean Expressions (SBEs), providing strong guarantees when all generated test vectors are executable. However, industrial systems impose feasibility constraints: some input combinations are illegal, unachievable, or unsafe to execute. If a single illegal vector appears in a minimal suite, it can destroy a required independence pair and invalidate 100% Unique-Cause MC/DC, even though the underlying decision logic remains unchanged. This paper presents EQ-Robin, a lightweight, constraint-resilient pipeline that generates a family of minimal (N+1) Unique-Cause MC/DC test suites and selects a feasible suite that satisfies domain constraints. EQ-Robin systematically enumerates semantically equivalent but structurally distinct SBEs by applying algebraic rearrangements on the expression's Abstract Syntax Tree (AST). Because Robin's Rule is sensitive to structural order, each variant yields a distinct minimal suite. EQ-Robin then filters and ranks candidate suites using practical constraint checks and cost heuristics (e.g., setup cost, oracle complexity). To ensure usability at scale, we introduce a budgeted exploration mode (early exit, guided rearrangement) and a fallback repair strategy when no fully feasible N+1 suite exists under given constraints. We demonstrate the core failure mode and recovery mechanism on a TCAS-II-derived expression and outline an empirical evaluation of EQ-Robin on TCAS-II SBEs under constraint scenarios representative of industrial feasibility limitations.
翻译:唯一因修正条件/判定覆盖(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通过实际约束检查与成本启发式规则(如设置成本、预言机复杂度)对候选套件进行筛选与排序。为确保大规模可用性,我们引入了预算化探索模式(提前退出、引导重排)以及在给定约束下不存在完全可行的N+1套件时的备用修复策略。我们以TCAS-II衍生表达式为例演示了核心失效模式与恢复机制,并概述了在代表工业可行性限制的约束场景下对TCAS-II SBE进行EQ-Robin实证评估的框架。