ICST 2025
Mon 31 March - Fri 4 April 2025 Naples, Italy

Unique-Cause MC/DC (UCM) is the most desired form of MC/DC in many safety-critical applications. For a given predicate, the UCM considers the independent pair of each condition by fixing the corresponding condition and flipping the other conditions. For the given N conditions in a predicate, the existing static symbolic execution tool, CBMC, generates MC/DC (Modified Condition/Decision) goal constraints of size, N+1 that constitutes its minimal independent pairs. However, we propose a novel UCM Sequence Generator (UCM-Gen) that generates all possible inequality comparisons of the sequences/combinations of the N conditions which helps in computing the independent pairs further. The UCM-Gen outputs UCM Annotated Program which when given to the program verifiers, produces the UCM Score (%). In our work, we have considered CBMC to get the SAT/UNSAT results for each sequence of the UCM Annotated Program. Upon analysing these results, we calculate the total number of independently affected conditions (i.e., I value) for all the predicates in the given program. Furthermore, this work is compared with the CBMC’s mode of MC/DC implementation. Interestingly, our proposed approach based UCM score (%) is always greater than the CBMC’s MC/DC score (%) and hence claiming that their corresponding test cases contribute in effective bug finding.