Modified Condition/Decision Coverage (MC/DC) is a mandatory structural coverage criterion for assuring the reliability of safety-critical software. Among its variants, Unique-Cause MC/DC provides the strongest assurance, yet efficient and scalable test generation for Unique-Cause MC/DC remains underexplored. This gap is particularly important because large-scale avionics studies report that 99.7% of conditional decisions are Singular Boolean Expressions (SBEs), for which Unique-Cause obligations can be precisely characterized. We propose Robin's Rule, a deterministic, direct-construction algorithm that generates a provably minimal test suite of N+1 test cases to guarantee 100% Unique-Cause MC/DC for SBEs with N conditions, without enumerating the 2^N truth table. The algorithm runs in O(N^2) time by explicitly constructing an (N+1)xN test table. To evaluate the approach, we build a benchmark of 25 SBEs consisting of 15 TCAS-II-derived conditions and 10 randomly generated SBEs with diverse operators and nesting. We validate achieved coverage using VectorCAST as an oracle and compare against state-of-the-art baseline paradigms using BDD and SAT. Across all benchmarks, Robin's Rule consistently achieves 100% Unique-Cause MC/DC with the theoretical minimum number of tests, while providing stable and efficient generation time. This work offers a practical and provably optimal solution for Unique-Cause MC/DC test generation on SBEs, improving both rigor and scalability for safety-critical verification.


翻译:修改条件/判定覆盖(MC/DC)是保障安全关键软件可靠性的强制性结构覆盖准则。在其变体中,唯一原因MC/DC提供了最强的保证,然而针对唯一原因MC/DC的高效且可扩展的测试生成方法仍未得到充分探索。这一空白尤为重要,因为大规模航空电子研究表明,99.7%的条件判定属于奇异布尔表达式(SBE),其唯一原因义务可被精确刻画。我们提出Robin's Rule,一种确定性的直接构造算法,可为具有N个条件的SBE生成一个可证明最小的、包含N+1个测试用例的测试套件,以保证100%的唯一原因MC/DC,而无需枚举2^N的真值表。该算法通过显式构造一个(N+1)xN的测试表,在O(N^2)时间内运行。为评估该方法,我们构建了一个包含25个SBE的基准集,其中包括15个源自TCAS-II的条件以及10个具有不同运算符和嵌套结构的随机生成SBE。我们使用VectorCAST作为验证工具来确认所达到的覆盖率,并与基于BDD和SAT的最先进基线范式进行比较。在所有基准测试中,Robin's Rule始终以理论最小测试数实现100%唯一原因MC/DC,同时提供稳定高效的生成时间。这项工作为SBE上的唯一原因MC/DC测试生成提供了一个实用且可证明最优的解决方案,提升了安全关键验证的严谨性和可扩展性。

0
下载
关闭预览

相关内容

DC:Distributed Computing。 Explanation:分布式计算。 Publisher:Springer。 SIT:http://dblp.uni-trier.de/db/journals/dc/
异常检测论文大列表:方法、应用、综述
专知
126+阅读 · 2019年7月15日
NAACL 2019 | 一种考虑缓和KL消失的简单VAE训练方法
PaperWeekly
20+阅读 · 2019年4月24日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
9+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 1月22日
VIP会员
相关VIP内容
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
9+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员