Toward Optimal MC/DC Test Case Generation

MC/DC coverage prescribes a set of MC/DC sequences. Such a sequence is defined by a specification of the truth values of certain atomic boolean expressions which appear in predicates (i.e. boolean combinations of atomic boolean expressions) in the program. An execution trace satisfies the sequence if it realizes the atomic boolean conditions in accordance with the truth value specification of the sequence. An MC/DC sequence is feasible if there is one such execution trace. The overall goal for an MC/DC test generator is, for each sequence: if feasible, to generate a test input realizing the sequence; otherwise, to prove that the sequence is infeasible. In this paper, we propose a method whose aim is optimal MC/DC coverage for bounded programs, i.e. for each MC/DC sequence, the method either produces a test input, or proves that sequence is infeasible. The method is based on symbolic execution with interpolation, and in this paper, we present a customized interpolation algorithm. We then present a comprehensive experimental evaluation comparing with the only available system CBMC which can operate on reasonably large programs, and further, which can provide optimal coverage for many examples. We will use a benchmark based on RERS which contains the kinds of reactive programs for which MC/DC was motivated by. We show that our method, by a significant margin, surpasses CBMC. In particular, our method often produces an optimal MC/DC result.