Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Efficient Algorithm for Generating Minimal Unique-Cause MC/DC Test cases for Singular Boolean Expressions

Robin Lee, Youngho Nam

TL;DR

This work tackles the challenge of generating minimal, provably correct test sets for Unique-Cause MC/DC on Singular Boolean Expressions (SBEs) in safety-critical software. It introduces Robin's Rule, a deterministic four-phase algorithm that directly constructs exactly $N+1$ test cases in $O(N^2)$ time, avoiding exponential truth-table enumeration. Through experiments on a TCAS-II-derived SBEs benchmark and VectorCAST as the coverage oracle, the method achieves 100% Unique-Cause MC/DC across all SBEs, outperforming BDD and SAT-based baselines in minimality and consistency of coverage. The approach offers a practical, scalable solution for rigorous verification in avionics and related safety-critical domains, with future work focusing on extending to Non-SBEs and Masking MC/DC.

Abstract

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.

An Efficient Algorithm for Generating Minimal Unique-Cause MC/DC Test cases for Singular Boolean Expressions

TL;DR

This work tackles the challenge of generating minimal, provably correct test sets for Unique-Cause MC/DC on Singular Boolean Expressions (SBEs) in safety-critical software. It introduces Robin's Rule, a deterministic four-phase algorithm that directly constructs exactly test cases in time, avoiding exponential truth-table enumeration. Through experiments on a TCAS-II-derived SBEs benchmark and VectorCAST as the coverage oracle, the method achieves 100% Unique-Cause MC/DC across all SBEs, outperforming BDD and SAT-based baselines in minimality and consistency of coverage. The approach offers a practical, scalable solution for rigorous verification in avionics and related safety-critical domains, with future work focusing on extending to Non-SBEs and Masking MC/DC.

Abstract

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.

Paper Structure

This paper contains 45 sections, 1 equation, 8 figures, 6 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. Preliminaries
  4. The Need for and Definition of MC/DC
  5. Formal Definitions of Unique-Cause and Masking MC/DC
  6. Unique-Cause MC/DC
  7. Masking MC/DC
  8. Singular Boolean Expressions (SBE) and Coupled Conditions
  9. Related Work
  10. Formal Model and Constraint Solving-Based Generation
  11. Search-Based and Heuristic Approaches
  12. Code Transformation-Based Approaches
  13. Research Trends and Positioning of This Work
  14. The Proposed Algorithm: Robin’s Rule
  15. Phase 1: Preprocessing
  16. ...and 30 more sections

Figures (8)

  • Figure 1: The four-phase process of Robin's Rule.
  • Figure 2: The overall three-step process for generating N+1 test cases from a 'B o B' form.
  • Figure 3: Test case generation process for the 'B o S' form.
  • Figure 4: Application of the exception handling rule.
  • Figure 5: Test case generation
  • ...and 3 more figures