Optimal Test Suite Generation for Modified
Condition Decision Coverage using SAT solving
Takashi Kitamura1 , Quentin Maissonneuve1,2 , Eun-Hye Choi1 , Cyrille Artho3 ,and Angelo Gargantini41Nat. Inst. of Advanced Industrial Science and Technology (AIST), Japan{t.kitamura,e.choi}@aist.go.jp
2
University of Nantes, France, quentin.maisonneuve1@etu.univ-nantes.fr
3
KTH Royal Institute of Technology, Sweden, artho@kth.se4
Università di Bergamo, Italy, angelo.gargantini@unibg.it

Abstract. Boolean expressions occur frequently in descriptions of computer systems, but they tend to be complex and error-prone in complex
systems. The modified condition decision coverage (MCDC) criterion insystem testing is an important testing technique for Boolean expression,as its usage mandated by safety standards such as DO-178 [1] (avionics)
and ISO26262 [2] (automotive). In this paper, we develop an algorithm
to generate optimal MCDC test suites for Boolean expressions. Our algorithm is based on SAT solving and generates minimal MCDC test suites.
Experiments on a real-world avionics system confirm that the technique
can construct minimal MCDC test suites within reasonable times, andimproves significantly upon prior techniques.

1

Introduction

Boolean expressions occur frequently in descriptions of computer systems, andare prevalent in software and hardware artifacts, such as programs, specifications,and hardware descriptions. On the other hand, they tend to be complicated andthus error-prone. Boolean expression testing is a technique to effectively test
such complicated Boolean expressions. Modified Condition Decision Coverage(MCDC), a. k. a., Active Clause Coverage (ACC), is one of main coverage criteria for testing Boolean expressions. The MCDC criterion requires that eachcondition in a decision is shown by execution to independently affect the outcome of the decision, where “decision” means “Boolean expression” [3].
To demonstrate the notion, take the following Table 1. A MCDC test suite
Boolean expression: φ1 = s ∧ (t ∨ u) (1). The test for φ1 = s ∧ (t ∨ u).
suite in Table 1 consisting of the four test cases
No. s t u φ1satisfies the MCDC criterion for this Boolean ex1 110 1
pression. Observe that, for example, the pair of
2 100 0the first and third test cases confirms that con3 010 0
dition s independently affects the outcome of the
4 101 1expression: the value of condition s changes thevalue of φ1 while the values of the other conditions, i. e. t and u, remain unchanged. Observe similarly that the first and second test cases confirm that fort, and the second and fourth confirm that for u. Boolean expressions such as (1)often represent abstract versions of actual logical expressions used in software
artifacts; e. g., the following logical expression, (z > 1) ∧ (f (x) ∨ (x < y + 1)),can be represented by (1), where the conditions (z > 1), f (x), and (x < y + 1)
are abstracted by s, t, and u respectively.
The usage of the MCDC criterion is motivated by several rationales.
1. MCDC can detect an erroneous use of and for or (or vice versa) in a Boolean
expression; this is called “Operator Reference Fault (ORF)” [4].
2. MCDC is a stricter form of decision coverage than decision coverage, which
stipulates each decision must evaluate to true and false.
3. The size of a test suite to satisfy the MCDC criterion (MCDC test suite, forshort) is reasonably small, and hence testing with MCDC incurs a reasonable test cost. For a Boolean expression φ with n conditions, the size of its
minimal MCDC test suite is n + 1 (e. g., [4], [5], [6]), instead of 2n required
for exhaustive testing. (This will be explained more in details in Section 2.2.)
Thus, MCDC effectively detects faults at reasonable cost. Due to such practical rationales, MCDC has been widely used. Various safety standards mandate
its use in testing safety-critical components, such as DO-178 [1] (avionics) andISO26262 [2] (automotive).
Driven by such industrial demands, MCDC has been actively studied fromvarious aspects, e. g., development of variants of MCDC [4,7], model-based testing with MCDC [7], coverage-driven test generation (a. k. a., CDTG) for programcodes [8], empirical studies on its effectiveness [9,10,11], and testing Deep Neural Networks (DNNs) with MCDC [12]. Among them, test case generation for
MCDC for Boolean expressions, which, given a Boolean expression, to find its
MCDC test suite, is a basic function for such testing techniques with MCDC,
and thus has been an important subject. Jones and Harrold developed algorithms for MCDC test reduction [13]. Arcaini et al. [14] developed a Boolean
expression testing framework to construct a small test suite including MCDC.
Bloem et al. [7] proposed yet another approach for MCDC test generation indeveloping a model based testing technique using MCDC.
In this paper, we develop an algorithm to construct small or even minimum
MCDC test suites; i. e., given a Boolean expression φ with n conditions, generate
an MCDC test suite whose size is equal to or smaller than n + 1. To realize suchan algorithm, we use SAT solving as the key technique. To evaluate the proposed
technique, we conduct experiments where we apply it to a real-world avionics
system in comparison with state-of-the-art techniques. The experiments confirm
that the technique can construct minimal MCDC test suites within reasonable
times, and improves significantly upon prior techniques.
This paper is organized as follows. The next section states the problem that
we tackle. Section 3 describes technical details of the proposed technique. Section
4 reports our evaluation of the proposed technique via experimental results.
2Section 5 states the significance of the work w. r. t., existing studies. Section 6
mentions possible future directions of this work.

2

Preliminaries

2.1

Definitions and Problem Formulations

In this subsection, we define the notion of ACC more formally. It is important tonote that there have been proposed several variants of ACC, including General
Active Clause Coverage (GACC), Restricted Active Clause Coverage (RACC),
Correlated Active Clause Coverage (CACC), General Inactive Clause Coverage(GICC), Restricted Inactive Clause Coverage (RICC) [4,15], Reinforced Condition Decision Coverage (RCDC) [11,16], and Observable Modified Condition
Decision Coverage (OMCDC) [17].
RACC is the classical and traditional form of ACC testing. On the other
hand, recently, CACC has become known to be more practical in industrial
usage. In this paper, we thus focus on RACC and CACC, but note that our
proposed techniques in this paper can be applied to the other variants of ACC.
In the following, we define RACC and CACC. First, as in this paper we aim
to develop ACC test generation techniques, we handle logical formulas as thetarget object that our techniques process; however, we mainly deal with themin the form of Boolean expressions by abstracting conditions in logical formulas
by Boolean variables. This is as exemplified by the example in Section 1. We
call Boolean variables in Boolean expressions conditions. We also use the term
predicate as a shorthand for Boolean expression.
Next we introduce the notion of determination:
Definition 1 (Determination). Let φ be a predicate and c be a condition of
φ. We say that condition c determines φ, if all the other conditions in φ havevalues so that changing the truth value of c changes the truth value of φ.
ACC stipulates that each condition of predicate φ independently determines
the result of φ. Thus, it is convenient to name the condition on which we arefocusing as the major condition, and all of the other conditions are minor conditions. Formally, for a predicate φ with n conditions c1 , c2 , · · · , cn , and a condition ci in φ, i. e., i ∈ {1 · · · n} called the major condition, conditions cj suchthat j ∈ {1 · · · n} ∧ (i 6= j) are called minor conditions.
Definitions of test cases and test suites are also provided as follows:
Definition 2 (Test case and Test suite). A test case of a predicate φ is apossible truth assignment for all the conditions in φ. A test suite is a set of test
cases.
The definitions of RACC and CACC are now ready as follows:
Definition 3. [RACC and CACC] Let φ be a predicate and T be a test suite. A
CACC pair of a condition c of φ is a pair of test cases of φ, satisfying that (1)3condition c determines φ as the major condition in both test cases and (2) thevalues of c are different. An RACC pair is a CACC pair such that the values
for the minor conditions are same in the two test cases. We say that T covers acondition of φ in RACC (resp. CACC), if it includes an RACC (resp. CACC)
pair of the condition. The test requirement of RACC (resp. CACC) for φ is that
T should cover all the conditions of φ. RACC (resp. CACC) is a measure todescribe the degree to which test requirements of RACC (resp. CACC), i. e., howmany conditions, are covered by T .
Note that RACC only differs from CACC in that the former requires theminor conditions of a test case pair have to have the same values, while thelatter does not. Therefore, we can say RACC is stricter criterion than CACC;
i. e., a RACC test suite for a predicate φ is also a CACC for it, but not viceversa. We call a test suite satisfying RACC (resp. CACC) test requirements a
RACC (CACC) test suite.
2.2

Sizes of Minimum ACC Test Suites

The size of a test suite often plays a critical factor for the feasibility and success ofreal-world (software and hardware) system testing, and has been a main concern
in theory and practice of testing techniques. A main reason for it is that “fullautomation” of test case execution, despite of a large body of research on it,
is still largely limited in practice due to problems such as the oracle problem.5
Another reason is that execution of one test case, even if automated, is often too
expensive for allowed time and/or financial constraints; and thus the number oftest cases that can be executed is limited.
Regarding properties on the ACC test suite size, it is often mentioned inliterature that the size of a minimum ACC test suite is “around” n + 1, for a
predicate with n conditions:
1. “Achieving MCDC requires, in general, a minimum of n + 1 test cases for adecision with n inputs.”, by Hayhurst et al. [5], where “decision” here means“predicate” in our setting.
2. “MCDC requires for n input variables a test suite at least of size n + 1.”, byFelbinger et al. [6], where ‘variables’ here mean ‘conditions’ in our setting.
3. “It turns out that for a predicate with n clauses, n + 1 distinct test requirements, rather than the 2n one might expect, are sufficient to satisfy active
clause coverage.”, by Amman and Offutt [4], where ‘clause’ here means ‘condition’ in our setting.
These claims are similar but not equivalent: the first two claims state that atleast n + 1 test cases are required to for an ACC test suite for a predicate with n
conditions, while the third one states n + 1 test cases are sufficient. Although it
can be conjectured from these that the minimum sizes of ACC test suites exist
around n + 1, according to our best knowledge, a formal proof of this property
is still an open problem.
5

The challenge of distinguishing the corresponding desired and correct behavior frompotentially incorrect behavior given a test case for a system under test.

4

2.3

Boolean Satisfiability Problem (SAT) and SAT Solvers

The Boolean satisfiability problem (SAT), known to be an NP-complete problem,is the problem of determining if there exists an interpretation, a. k. a., model,that satisfies a given Boolean expression. SAT solvers are software tools that
automatically solve SAT problems. As many NP-complete problems can be reduced to SAT, the development of efficient SAT solvers is an important andactive research subject. We use SAT solvers for our ACC test generation.

3

Algorithm for Optimal MCDC Test Generation

In this section, we develop an algorithm for generating an optimal test suite for
MCDC. We explain our algorithm by first introducing the notion of Predicate
Determining Condition (PDC), based upon which we develop our algorithm.
3.1 Predicate Determining Condition (PDC)
We explain the notion of predicate determining condition (PDC), introduced
in [4], which we use in developing our ACC test generation algorithm.
Definition 1 provided the definition of determination. PDC, given the target
predicate φ and the major condition of φ, provides the condition, as a logicalformula for minor conditions, under which the major condition c determines φ.
Definition 4 (Predicate determining condition: PDC). Let φ be a predicate φ and c be a condition in φ. The predicate determining condition (PDC)of a predicate φ and a condition c, denoted by φc , is a predicate under which thevalue of c determines that of φ.
Since a predicate expresses a set of test cases, the PDC of condition c can bealso interpreted as all test cases for which c determines φ.
An advantage of PDCs is that we can compute them. Given a predicate φand a condition c, the PDC is computed as follows:
Proposition 1. Let φc=True (and φc=False ) represent the predicate φ with every
occurrence of c replaced by ‘ True’ (and ‘ False’), respectively. Neither φc=Truenor φc=False has any occurrences of condition c. The PDC of condition c for a
predicate φ is obtained by connecting the two expression with exclusive-or:
φc = φc=True ⊕ φc=False(2)

This proposition holds, as the requirement that condition c independently affects
the outcome of predicate φ can be described as the following formula, whichcorresponds to (2): (φc=True ∧ ¬φc=False ) ∨ (¬φc=True ∧ φc=False ).
Example 1. Let φ be φ1 = s ∧ (t ∨ u) of Boolean expression (1). The PDC ofpredicate φ and condition s, i. e., φs , can be derived as follows:
φs = φs=True ⊕ φs=False(3)= (True ∧ (t ∨ u)) ⊕ (False ∧ (t ∨ u))(4)= (t ∨ u) ⊕ False(5)= (t ∨ u)(6)5This means that for the major condition s to determine predicate φ, there arethree choices for truth assignments, (t, u), (t, ¬u), and (¬t, ¬u).
We remark that if the PDC of a predicate and a condition is not satisfiable, then this means that it is not feasible to create an ACC test pair for thatcondition. We call such a condition an infeasible condition.
3.2

SAT-encoding

The key device to develop our algorithm is the SAT-encoding of the following
problem: “For a predicate φ and the number of test cases k, is it possible toconstruct an ACC test suite?”. We explain about the SAT-encoding of thisproblem in this subsection. The encoding uses a matrix model with p columns
and n rows as Boolean conditions xnp to encode the test suite, as follows: 1
x1 . . . x1p
.. 
X =  ...
.(7)

xk1 . . . xkp

This matrix model of a test suite expresses that the i-th row represents the ith test case, and the p-th column of the row represents the value of the p-th
parameter of the i-th test case.
Using the matrix model to represent a test suite, we construct the SAT
encoding to construct an ACC test suite with the size k, as follows:
encode(φ, condsφ , k) =k_
j=1,i6=j



^

k
_

c∈condsφi=1(1)(¬xjc ∧ φjc )(3)(xic ∧ φic )

∧
(2)

!

^

∧
(xid ⇔ xjd )d∈condsφ s.t. c6=d

(8)
(4)

where φic is PDC of condition c whose Boolean conditions are those in the i-th
row of the matrix model, and condsφ is a set of feasible conditions in φ. This SATencoding specifies the following: Sub-formula (2) specifies that for a condition of
the predicate, say c, in at least one row of the matrix table, i. e., in one test caseof the test suite, the value of the condition in the test case, xc , must be ‘True’,
while the PDC of the condition c must be also true. On the other hand, subformula (3) specifies that the same condition must be ‘False’, while the PDC ofc must be ‘True’, in at least one test case. The i 6= j in formula (3) clarifies thatthe value of condition c cannot be ‘True’ and ‘False’ in the same row. This subformula can be omitted, but carefully placed redundant SAT formula can speed
up the solving process. The outermost conjunction (1) indexed by conditions ofφ imposes that the above sub-formulas (2) and (3) are to be applied to all theconditions in the predicate under test φ.
6

Sub-formulas (1), (2), and (3) are encoding for CACC, since sub-formulas (2)and (3) together satisfy condition (1) and (2) of Definition 3, and sub-formula(1) guarantees it for all the conditions. Sub-formula (4) specifies the condition
for RACC that stipulates that values of all the minor conditions are equivalent.
For RACC, we may also omit φjc in (2); this is possible, since if constraints (2)and (4) hold and xjc = False, then the i-th test case and the j-th test case differ
only in the value of xc so that φjc and φic should be equivalent.
The encoding for a given test suite size induces a SAT formula, such that
‘SAT’ for the evaluation of the formula entails the existence of an ACC test suitewith that size; in that case, the solution contains all the information on the ACC
test suite. On the other hand, ‘UNSAT’ means the refutation of the existence ofsuch a test suite.
Example 2. The following snippet of SAT-formula is the SAT-encoding of Boolean
expression φ1 with the test suite size 4. The sub-formulas (i), (ii), and (iii), respectively, express that conditions s, t and u are confirmed to independently
affect the outcome of the predicate.
(s1 ∧ φ1s ) ∧(¬s2 ∧ φ2s ) ∧ (t1 ⇔ t2 ) ∧ (u1 ⇔ u2 ) ∨




 


3
3
1
3
1
3
4
4
1
4
1
4
(¬s
∧
φ
)
∧
(t
⇔
t
)
∧
(u
⇔
u
)
∨
(¬s
∧
φ
)
∧
(t
⇔
t
)
∧
(u
⇔
u
)


s
s






.


.
.








4
4
1
1
4
1
4
1
(¬s ∧ φs ) ∧ (t ⇔ t ) ∧ (u ⇔ u ) ∨ ∨ (s ∧ φs ) ∧





 
2
2
4
2
4
2
3
3
4
3
4
3
(¬s ∧ φs ) ∧ (t ⇔ t ) ∧ (u ⇔ u ) ∨ (¬s ∧ φs ) ∧ (t ⇔ t ) ∧ (u ⇔ u )
(i)




(t1 ∧ φ1t ) ∧(¬t2 ∧ φ2t ) ∧ (s1 ⇔ s2 ) ∧ (u1 ⇔ u2 ) ∨




 

V 
(¬s3 ∧ φ3s ) ∧ (t1 ⇔ t3 ) ∧ (u1 ⇔ u3 ) ∨ (¬s4 ∧ φ4s ) ∧ (t1 ⇔ t4 ) ∧ (u1 ⇔ u4 )






.
.
.
(ii)

V
(u1 ∧ φ1u ) ∧ · · ·


(iii)

(9)
3.3

Algorithm

We proceed with the actual algorithm on how to find a smaller ACC test suiteusing SAT-encoding. For the discussion, we first argue about properties on thesize of ACC test suites. From our literature review in Section 2.2, we conjecturethat the minimum size of ACC test suites should be around n + 1 for a predicate
with n conditions. However, because no formal proof for this lower bound exists
yet, we use the following proposition, which is a weaker form of the conjecture,
but which can be proved easily:
Proposition 2. For a predicate with n conditions, the minimum size of a CACC/RACC test suite is at most 2n.
7

Algorithm 1: The main part of our algorithm for CACC
Input: A Boolean Expression (φ)
Output: A CACC test suite
1 Compute the feasible conditions of φ, and store them in condsφ ;2 if(|condsφ | == 0) return (“Exception: No feasible conditions exist.”);3 Set size ← 2 ∗ |condsφ |, for the initial test size;
4 while true do
5(isSAT,model) ← checkSat(encode(φ, condsφ , size));6
if(isSAT == UNSAT) return suite;
7
Make test suite from model;
8
size ← size − 1
9 end

Proof. From Definition 3, an RACC test suite should include at least one RACC
pair for each condition in φ. Since we can make an RACC pair with two test
cases, 2n is enough for the size of an RACC test suite for φ with n conditions.
Since a RACC test suite is also an CACC one, this property also holds for CACC.
Using Proposition 2, the algorithm is designed as in Algorithm 1. The algorithm, at the beginning (in Line 1), computes feasible conditions of φ. Computing
all the feasible conditions can be done by collecting conditions whose PDCs are
satisfiable (possibly, using a SAT solver). Based on the computed feasible conditions (condsφ ) and their number (|condsφ |), the algorithm starts searching fora minimum test suite. It iteratively attempts to generate an ACC test suite bydecrementing the size of a test suite by one, starting from 2 ∗ |condsφ |. In each
iteration, the algorithm applies the SAT-encoding of the current test size, andapplies a SAT solver to the encoded formula. The decremental iteration continues while the encoded formula is satisfiable, and terminates when it encounters‘unsatisfiable (UNSAT)’ (Line 6). The test suite found in the last satisfying iteration is minimal. Line 2 handles a corner case, where no feasible conditions arecontained in φ, by throwing an exception.
The encoded formula in each iteration is a SAT problem over Boolean variables, and the test size. The size starts at ‘2 ∗ |condsφ |’ and is reduced by one
in each iteration. Thus, the algorithm is guaranteed to terminate with a minimum ACC test suite, in principle. In practice, however, limited computational
resources may prevent us from finding the minimum one. The SAT solver may
take a lot of time and/or a lot of memory, as the attempted search approaches the
optimal size. Thus, a concern is scalability of the algorithm, which we examine
by experiments in Section 5.
The algorithm uses 2n for the initial test size based on Proposition 2. We
have two main reasons to adopt this proposition, instead of the conjecture forn + 1. First, our algorithm is certainly correct using the proved proposition with
2n, instead of using the (unproved) conjecture with n + 1. Second, our algorithmwith 2n for the initial size performs well in practice, outperforming existing
techniques, as shown in Section 5. Moreover, if the worst-case bound of n + 1 is
8

proven in the future, we can easily adapt that result in our algorithm, by settingn + 1 as the initial size.

4

Related Work

Test suite reduction and minimization is one of central subjects in software
testing. To the best of our knowledge, the earliest work which discusses the test
suite sizes in MCDC testing is by Jones and Harrold [13]. They develop a test
suite reduction technique for MCDC, which, given a predicate φ and an MCDC
test suite T , finds an MCDC test suite T 0 such that T 0 ⊂ T . The basic approachof the technique is to construct such an MCDC test suite T 0 , by iteratively
choosing or removing one test case from the given MCDC test suite T basedon the contribution weight computed for each test case in T . For example, their‘build-up’ approach constructs an MCDC test suite by iteratively adding a test
case in T with the highest contribution weight to T 0 , starting from the empty
set as the initial test suite of T 0 . Note that the JH-algorithm is a test reduction
technique, rather than MCDC test generation; however, by complementing thealgorithm with a function to prepare initial MCDC test suites, it can be used asa test generation technique for MCDC.
Arcaini et al. [14] developed a general framework for test generation for
Boolean expression testing with various coverage criteria, including MCDC. The
technique constructs an MCDC test suite with the basic approach of accumulating an MCDC pair (a pair of test cases) for each condition in turn. Offutt
et al. [18], in developing a model-based testing technique with MCDC testing,discuss a similar technique to construct an MCDC test suite. However, bothtechniques require a test suite of size 2n for a predicate with n conditions, which
is usually larger than the test suites that our algorithm generates.
Bloem et al. [19] devised an algorithm to construct MCDC test suites, also
in developing their model-based testing technique using MCDC. The technique
is similar to those by Arcaini et al. [14] and Offutt et al. [18], in the respectthat its basic procedure is to accumulate an MCDC pair for each condition in
turn; however, they apply an improvement to this basic approach to reduce thesize of generated test suites. The improvement is that the algorithm, for every
condition, checks if the current test suite already includes an MCDC pair for thecondition, when adding an MCDC pair for each condition. If the MCDC pairalready exists in the test suite, the algorithm skips adding an MCDC pair forthat condition. They also use SAT-solving to realize the technique.
Our algorithm is inspired by the SAT-based test generation technique for
combinatorial interaction testing (CIT) by Hnich et al. [20]. The key of theirtechnique is a SAT-encoding of the problem of finding a CIT test suite with a
specified size. It is confirmed that the technique can construct CIT test suites
with reasonably small sizes, compared with other approaches. Due to the significance, this work is followed by a number of studies for extension or acceleration(e. g., [21]). Our work in this paper thus can be seen as a new application direc9

Table 2. The benchmark set consists of 20 logical expressions, retrieved from “Traffic Collision Avoidance System (TCAS)“ of an avionics
system [8]. The logical expressions in the benchmark set contain 5 to 15 (feasible and infeasible) conditions, as indicated by #conds. The
table also shows the infeasible conditions (I.C.) for each benchmark; ACC pairs cannot be made for such infeasible conditions.

10

No Boolean expression#conds I.C.
1 a(!b+!c)d + e
5
2 !(ab)(d!e!f +!de!f +!d!e!f )((ac(d + e)h) + (a(d + e)!h) + (b(e + f )))7
3 !(cd)(!ef !g!a(bc+!bd))7
4 ac(d + e)h + a(d + e)!h + b(e + f )7
7
5 !ef !g!a(bc+!bd)
6 (!ab + a!b)!(cd)!(gh)((ac + bd)e(f g+!f h))8
7 (ac + bd)e(f g+!f h)8
8 (a((c + d + e)g + af + c(f + g + h + i)) + (a + b)(c + d + e)i)!(ab)!(cd)!(ce)!(de)!(f g)!(f h)!(f i)!(gh)!(hi)9
9 a(!b+!c + bc!(!f gh!i+!ghi)!(!f glk+!g!ik)) + f
99 b, h10 a((c + d + e)g + af + c(f + g + h + i))(a + b)(c + d + e)i
11 (ac + bd)e(i+!g!k+!j(!h+!k))10
10
12 (ac + bd)e(i+!g!k+!j(!h+!k))(ac + bd)e(i+!g!k+!j(!h+!k))13 (!ab + a!b)!(cd)(f !g!h+!f g!h+!f !g!h)!(jk)((ac + bd)e(f + (i(gj + hk))))11
14 (ac + bd)e(f + (i(gj + hk)))
11
15 (a(!d+!e + de!(!f gh!i+!ghi)!(!f glk+!g!ik))+!(!f gh!i+!ghi)!(!f glk+!g!ik)(b + c!m +12f ))(a!b!c+!ab!c+!a!bc)
12
16 a + b + c+!c!def !g!h + i(j + k)l
17 a(!d+!e + de!(!f gh!i+!ghi)!(!f glk+!g!i!k))+!(f gh!i+!ghi)!(!f glk+!g!ik)(b + c!m + f )12
18 a!b!c!d!ef (g+!g(h + i))!(jk+!jl + m)
13
13
19 a!b!c(!f (g+!f (h + i))) + f (g+!g(h + i)!d!e)!(jk+!jl!m)
20 a!b!c(f (g+!g(h + i)))(!e!n + d)+!n(jk+!jl!m)14

tion of the SAT-based test generation technique to MCDC testing, and also as
an import of new technical element to MCDC testing field.

5

Experimental Evaluation

In this section, we conduct experiments to evaluate our proposed technique. Dueto the space limitation, we only evaluate the proposed algorithm for the CACC
case, as it is the most basic, practical, and interesting case among ACC variants.
To clarify the purpose of the experiments and evaluation, we set the following
research questions:– RQ1: Does our algorithm perform better than existing techniques, with respect to the sizes of generated test suites and computation times?
– RQ2: Can our algorithm find minimal CACC test suites?
For investigating these RQs, we implemented our algorithm in Scala. Also
to conduct the experiments, we prepared a benchmark set of logical expressions
retrieved from “Traffic Collision Avoidance System (TCAS)“ of a real-world
avionics system [8]. The details about benchmark data are shown in Table 2.
For RQ1, we also implemented the MCDC test generation technique basedon the JH-algorithm and the technique by Bloem et al., as the the state-of-theart techniques by ourselves, since implementations of these techniques are notavailable. Since JH-algorithm is an MCDC test reduction technique instead oftest generation, we complemented it with the function to randomly generate
MCDC test suites so that JH-algorithm can reduce them as initial test suites.
The function is realized to randomly generate m ACC pairs for each conditionof a given formula. Therefore, the most basic form of m = 1 means 2n test
cases, where n is the number of conditions in the given formula. We prepared
several variants that vary in the sizes of initial MCDC test suites, as follows:m = 1, 50, 200, and 400, respectively denoted by JH 1 , JH 50 , JH 200 , and JH 400 .
Also for RQ1, the timeout is set to 60 seconds for our algorithm for a propercomparison and evaluation.
For RQ2, we measure the time required for our algorithm to find minimal
test suites by finding UNSAT for the benchmark set, thus proving that no test
suite smaller than the previously found satisfiable assignment exists. For this,the timeout is set to 1800 seconds for our algorithm.
Table 3 shows the experimental results. We answer the research questions,by observing the experimental results, in the following.
Answer to RQ1. From the experimental results, we conclude that our algorithm
performs better than the state-of-the-art techniques in both the size of generated
test suites and computation times. First, our algorithm wins against the otheralgorithms for all the benchmark data. On other hand, the algorithm variants
based on the JH-algorithm or the technique by Bloem et al., only perform equallywell to ours only in a couple of cases. Moreover, our algorithm can build suchsmaller test suites fairly quickly, i. e., within a few seconds for all the benchmark
11Table 3. The results of our experiments. This table shows the sizes of the generated CACC test suites (‘#tests‘) and the computation
times in seconds (‘time’) of the algorithms (JH1 , JH50 , JH200 , JH400 , by Bloem et al., and our algorithm) for the benchmark set in
Table 2. To properly answer RQ1 and RQ2, we use two timeout settings for our algorithm, 60 seconds (time<60 ), and 1800 seconds(time<1800 ). A ‘—’ in columns ‘time<1800 ’ means a minimum test suites is found within in 60 seconds, and the time is given in column‘time<60 ’. The bold font in the columns for ‘#tests‘ denote instances in which the test suite size is smaller than or equal to those foundby other algorithms, while that in the columns for ‘time‘ means the algorithms returned the test suite within 60 seconds. For columnsof our algorithms, a ‘*’ denotes a minimal test suite is found with the guarantee of finding ‘UNSAT‘ by the SAT solver. ‘#wins’ denotes
the number of cases where the algorithm generates the smallest test suite among all algorithms within 60 seconds; multiple winners may
exist for each benchmark data. ‘impr(%)’ denotes the reduction rate on the test suite size by our algorithm compared with that by thecorresponding algorithm of the column; e.g., the test suite size by our algorithm is smaller than that by JH400 by 19.7% in total.
The experiments were performed on a machine with a Quad-Core Intel Xeon E5 3.7 GHz and 64 GB Memory running on Mac OS High
Sierra 10.13.3. For running the programs, Scala option “-Xmx8g -Xms1024m” is used. As the back-end SAT solver, we used SMT solverZ3 [22].

12

JH1
JH50
JH200
JH400
Bloem et. al. our algorithm (2n for the initial size)
No #tests time #tests time #tests time #tests time #tests time #tests time<60 #tests time<1800
1
6 0.9
6 4.2
6 10.46 10.86
0.9 6*
0.5—
9 1.7
8 11.18 11.38 12.18
1.5 5*
1.3
—
2
3
7 1.6
7 2.9
7 2.8
7 2.9
7
1.3 6*
1.0—
12 1.7
7 18.1
6 52.5
6 98.49
1.4 6*
0.9
—
4
5
9 1.4
8 5.1
8 5.1
8 5.0
9
1.4 8*
0.9
—
6
9 1.8
8 13.7
7 49.5
7 118.69
1.7 3*
1.5—
7
10 1.7
8 20.7
7 69.4
7 89.010
1.7 7*
1.0—
8
15 2.7
12 24.7
12 96.9
10 208.6
11
2.5 4*
2.6—
9
11 2.610 16.9
10 27.2
10 44.511
2.2 9*
3.0
—
10
9 2.1
8 18.8
7 71.7
7 138.19
1.8 7*
1.0—
11
12 2.6
10 27.3
10 125.5
9 290.012
2.5 8*
1.8—
12
12 2.6
10 27.4
10 126.7
9 289.112
2.5 8*
2.5—
13
15 3.813 27.0
12 99.0
13 243.413
3.6 9*
3.5—
14
12 3.313 30.8
12 148.7
12 369.9
13
3.0 9*
1.8—
15
18 4.417 34.5
16 150.6
16 414.1
17
4.3 9*
5.8—
16
13 3.513 35.4
12 142.8
11 304.3
13
3.2 11*2.0—
17
18 4.915 35.9
13 165.6
13 435.5
16
4.4 11
4.6
11*
80.7
18
15 4.113 37.9
13 127.4
13 286.7
14
3.8 13
2.6
13
>1800
19
20 4.218 38.2
16 175.0
16 481.1
14
4.0 12
3.3
12*
197.7
20
18 4.618 42.0
16 194.8
15 540.5
16
4.4 12
3.6
12*
167.3
#wins
2
3
4
3
2
20
—
impr(%)
32.0
23.4
18.2
16.2
25.7
—
—

data, which is much faster than the other techniques. The improvement rateachieved by our algorithm is also significant; it can generate test suites that arefrom 16.2% up to 32.0% smaller than the the other techniques.
Answer to RQ2. From the experiments, we confirm that the resulting test suite isof size equal or less than n+1 in 17 out of 20 cases. We can also confirm that in 19
cases our algorithm can find the guaranteed minimum sizes by finding ‘UNSAT’
within 1800 seconds. For the case where the algorithm cannot guarantee theminimum size of the test suite (i. e., for benchmark #18), there may exist asmaller CACC test suite.

6

Conclusion and Future Work

We believe our algorithm to construct small or even the minimum MCDC test
suites will play a significant role broadly in the software testing field, since (1)MCDC has become a de-facto standard coverage criterion in testing safetycritical systems, and (2) the technique, as a basic testing technique, can beused in combination with other testing techniques, such as model-based testingand program-code-level testing.
Model-based testing, a sub-discipline of model-based development (MBD),
is another key technique in safety-critical domains such as in avionics and automotive. A number of studies have attempted to introduce MCDC testing inmodel-based testing techniques, to enhance the accountability as well as its bugdetecting ability [18,7,23,24]; also see Section 4. Generally, these techniques deal
with state transition systems as models, and regard a sequence of states as a test
case. To derive effective test cases, these techniques apply the MCDC criterion
to the transition guards, which specify as a logical formula the conditions fortransitions to take place. This approach is reasonable since real-world transition
systems often become complex and error-prone, however, their test generation
components are not efficient w.r.t. the test suite size and computation time. Ouralgorithm can complement such model-based testing techniques.
Another application area of our algorithm is Coverage-Directed Test case
Generation (CDG/CDTG). CDTG is a white-box testing technique, working
at program code level to generate test cases, to achieve a higher code coverage.
CDTG and its adaptation for MCDC have been actively studied [25,26,27]. Such
CDTG techniques targeting MCDC analyze the structure of the given program,
especially logical formulas embedded in the program, and try to find test inputs that reach each logical formula in the program. Although these techniques
differ in several dimensions such as search techniques (e. g., dynamic symbolic
execution [25], model checking [26], search-based optimization [27]), they havein common that they prepare MCDC test suites for embedded logical formulas
before starting the search. Similar to the situation of model-based testing, ourproposed algorithms can effectively complement such CDTG techniques.
We consider several directions for future work. One direction is to extend ouralgorithm to deal with general logical formulas, e. g., x = 0 ∧ (x > 0 ∨ y = 0),13

instead of their abstracted forms in Boolean expressions, i. e., s ∧ (t ∨ u). It issince our algorithm may produce unusable tests for such an abstracted predicate.
For example, recall Table 1 is an MCDC test suite for s ∧ (t ∨ u). Note, however,that the first test case, i. e., {s = True, t = True, u = False}, is unusable ifs ∧ (t ∨ u) originates from x = 0 ∧ (x > 0 ∨ y = 0) by abstraction, since there is
no assignment that makes s = True (i. e., x = 0) and t = True (i. e., x > 0) at
the same time. One approach for this would be to impose additional constraints
among abstracted variables, to specify hidden relations between s and t. In theexample, a constraint like ¬(s ∧ t) would encode that. The PDC of s for thispredicate would be constructed as follows: φs=True ⊕ φs=False ∧ ¬(s ∧ t). We needcareful investigations on this approach including how to specify such additional
constraints automatically and how it affects the size of test suite.
Another direction is to further accelerate or scale our algorithm. Although
it was shown by the experiments that our algorithm works fairly well for a realworld system in the avionics domain, it may need to be prepared for larger
and more complex systems. Toward this technical improvement, we think thetechnique using incremental SAT solving [21] can be effectively applied. Thirdly,
we consider to apply our technique to other ACC variants explained in Section 2.
We are also interested in applying it to improve the testing technique for Deep
Neural Networks based on MCDC proposed by [12].
Acknowledgment. We thank Hélène Waeselynck and anonymous reviewers
whose comments have greatly improved this paper.

References
1. RTCA: DO-178C: Software considerations in airborne systems and equipment
certification (2011)
2. ISO26262: Int. org. for standardization, road vehicles - functional safety - (2009)
3. Chilenski, J.J., Miller, S.P.: Applicability of modified condition/decision coverage
to software testing. Software Engineering Journal 9(5) (1994) 193–200
4. Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University
Press (2008)
5. Kelly J., H., Dan S., V., John J., C., Leanna K., R.: A practical tutorial on
modified condition/decision coverage. Technical Report NASA/TM-2001-210876,
NASA (2001)
6. Felbinger, H., Pill, I., Wotawa, F.: Classifying test suite effectiveness via model
inference and ROBBDs. In: Proc. 10th Int. Conf. on Tests and Proofs (TAP 2016),
Vienna, Austria. (2016) 76–93
7. Bloem, R., Hein, D.M., Röck, F., Schumi, R.: Case study: Automatic test casegeneration for a secure cache implementation. In: Proc. 9th Int. Conf. on Tests
and Proofs (TAP 2015), L’Aquila, Italy. (2015) 58–75
8. Weyuker, E.J., Goradia, T., Singh, A.: Automatically generating test data from aboolean specification. IEEE Trans. Software Eng. 20(5) (1994) 353–363
9. Dupuy, A., Leveson, N.: An empirical evaluation of the MC/DC coverage criterionon the HETE-2 satellite software. In: Proc. 19th Digital Avionics Systems Conf.
(DASC2000)

14

10. Vilkomir, S., Starov, O., Bhambroo, R.: Evaluation of t-wise approach for testing
logical expressions in software. In: Proc. Sixth IEEE Int. Conf. on Software Testing,
Verification and Validation, ICST 2013 Workshops, Luxembourg. (2013) 249–256
11. Kapoor, K., Bowen, J.P.: A formal analysis of MCDC and RCDC test criteria.
Softw. Test., Verif. Reliab. 15(1) (2005) 21–40
12. Sun, Y., Huang, X., Kroening, D.:
Testing deep neural networks (2018)arXiv:1803.04792.
13. Jones, J.A., Harrold, M.J.: Test-suite reduction and prioritization for modified
condition/decision coverage. IEEE Trans. Software Eng. 29(3) (2003) 195–209
14. Arcaini, P., Gargantini, A., Riccobene, E.: How to optimize the use of SAT and
SMT solvers for test generation of boolean expressions. Comput. J. 58(11) (2015)
2900–2920
15. Chilenski, J.J.: An investigation of three forms of the modified condition decision
coverage (MCDC) criterion. Technical Report DOT/FAA/AR-01/18, Office ofAviation Research (2001)
16. Vilkomir, S.A., Bowen, J.P.: From MC/DC to RC/DC: formalization and analysis
of control-flow testing criteria. In: Formal Methods and Testing, An Outcome of
the FORTEST Network, Revised Selected Papers. (2008) 240–270
17. Whalen, M.W., Gay, G., You, D., Heimdahl, M.P.E., Staats, M.: Observable modified condition/decision coverage. In: 35th Int. Conf. on Software Engineering,
ICSE ’13, San Francisco, CA, USA. (2013) 102–111
18. Offutt, A.J., Liu, S., Abdurazik, A., Ammann, P.: Generating test data fromstate-based specifications. Softw. Test., Verif. Reliab. 13(1) (2003) 25–53
19. Bloem, R., Greimel, K., Koenighofer, R., Roeck, F.: Model-based MCDC testing ofcomplex decisions for the java card applet firewall. In: Proc. of the Fifth Int. Conf.
on Advances in System Testing and Validation Lifecycle (VALID 2013). (2013) 1–6
20. Hnich, B., Prestwich, S., Selensky, E.: Constraint-based approaches to the covering
test problem. In: Proc. of CSCLP 2004. Volume 3419 of LNAI. (2005) 172–186
21. Yamada, A., Kitamura, T., Artho, C., Choi, E.H., Oiwa, Y., Biere, A.: Optimization of combinatorial testing by incremental SAT solving. In: Proc. of 8th IEEE
Int. Conf. on Software Testing, Verification and Validation (ICST 2015). (2015)
1–10
22. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proc. of 14th Int.
Conf. on Tools and Algorithms for the Construction and Analysis of Systems,(TACAS 2008) Hungary. (2008) 337–340
23. Heimdahl, M.P.E., Devaraj, G.: On the effect of test-suite reduction on automatically generated model-based tests. Autom. Softw. Eng. 14(1) (2007) 37–57
24. Gargantini, A., Heitmeyer, C.L.: Using model checking to generate tests fromrequirements specifications. In: Proc. 7th European Conf. of Software Engineering,
Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations ofSoftware Engineering, (ESEC/FSE’99). (1999) 146–162
25. Pandita, R., Xie, T., Tillmann, N., de Halleux, J.: Guided test generation forcoverage criteria. In: Proc. of 26th IEEE Int. Conf. on Software Maintenance(ICSM 2010), Timisoara, Romania. (2010) 1–10
26. Bokil, P., Darke, P., Shrotri, U., Venkatesh, R.: Automatic test data generation
for C programs. In: Proc. of Third IEEE Int. Conf. on Secure Software Integration
and Reliability Improvement, SSIRI 2009. (2009) 359–368
27. Awedikian, Z., Ayari, K., Antoniol, G.: MC/DC automatic test input data generation. In: Proc. of Genetic and Evolutionary Computation Conf. (GECCO 2009),
Canada. (2009) 1657–1664

15