Proving MC/DC unique cause definition compliance

Question

I'm reading the following paper on MC/DC: http://shemesh.larc.nasa.gov/fm/papers/Hayhurst-2001-tm210876-MCDC.pdf.

I have the source code: Z := (A or B) and (C or D) and the following test cases:

-----------------
| A | F F T F T |
| B | F T F T F |
| C | T F F T T |
| D | F T F F F |
| Z | F T F T T |
-----------------

I want to prove that the mentioned test cases comply with unique cause definition.

I started by eliminating masked tests:

• A or B = F T T T T, meaning it masks the first test case from C or D as F and (C or D) = F.
• C or D = T T F T T, meaning it masks the third test case from A or B as (A or B) and F = F.

I then determined MC/DC:

Required test cases for A or B:

• F F (first case)
• T F (fifth case)
• F T (second or fourth case)

Required test cases for C or D:

• F F (third case)
• T F (fourth or fifth case)
• F T (second case)

Required test cases for (A or B) and (C or D):

• T T (second, fourth or fifth case)
• F T (first case)
• T F (third case)

According to the paper, this example doesn't complies to unique cause definition. Instead, they propose changing the second test case from F T F T to T F F T.

-----------------
| A | F T T F T |
| B | F F F T F |
| C | T F F T T |
| D | F T F F F |
| Z | F T F T T |
-----------------

I determined MC/DC for A or B again:

• F F (first case)
• T F (fifth case)
• F T (fourth case)

Then, they introduce the following independence pairs table that shows the difference between both examples (in page 38):

I understand that for the first example, the independence pair that they show changes two variables instead of one, however I don't understand how they are computing the independence pairs.

In the A column, I can infer they take F F T F from the test cases table's A row, and they compute the independence pair as the same test case with only A changed (T F T F).

In B's column, however, they pick F F T F again. According to my thinking, this should equal to the B's column: F T F T instead.

The rest of the letters show the same dilemma.

Also for D's first example column, they show that the independence pair of F T F T is T F F F, which ruins my theory that they are computing the independence pair from the first value, and proving that they are picking it from somewhere else.

Can someone explain better how (and from where) do they construct such independence pair table?

Answer 1

First the let’s re-read the definitions:

(From www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/media/cast-10.pdf)

DO-178B/ED-12B includes the following definitions:

Condition

A Boolean expression containing no Boolean operators.

Decision

A Boolean expression composed of conditions and zero or more Boolean operators. A decision without a Boolean operator is a condition. If a condition appears more than once in a decision, each occurrence is a distinct condition.

Decision Coverage

Every point of entry and exit in the program has been invoked at least once and every decision in the program has taken on all possible outcomes at least once.

Modified Condition/Decision Coverage

Every point of entry and exit in the program has been invoked at least once, every condition in a decision in the program has taken all possible outcomes at least once, every decision in the program has taken all possible outcomes at least once, and each condition in a decision has been shown to independently affect that decision's outcome. A condition is shown to independently affect a decision's outcome by varying just that condition while holding fixed all other possible conditions.

---

So, for the decision '(A or B) and (C or D)' we have four conditions: A,B,C and D

For each condition we must find a pair of test vectors that shows that the condition 'independently affect that decision's outcome'.

For unique cause MC/DC, only the value of the condition considered can vary in the pair of test vectors.

For example let's consider condition A. The following pair of test vectors covers condition A:

(A or B) and (C or D) = Z
 T    F       T    F    T   
 F    F       T    F    F   

With this pair of test vectors (TFTF, FFTF) only the value of A and Z (the decision) change.

We then search pairs for conditions B, C and D.

Using the RapiCover GUI (Qualifiable Code coverage tool from Rapita Systems - www.rapitasystems.com/products/rapicover) we can see the full set of test vectors (observed or missing) to fully cover all conditions of the decision.

RapiCover screenshot

Vector V3 (in yellow in the screenshot above) isn't used in any independence pair. Vector V6 (in red in the screenshot) is missing for MC/DC coverage of condition D.

This is for the definition of 'unique cause' MC/DC.

---

Now for 'masking MC/DC':

For 'masking MC/DC' the requirement that the value of a single condition may vary in a pair of test vectors is relaxed provided that any other change is masked by the boolean operators in the expression.

For example, let's consider the pair of vectors for condition D:

  (A or B) and (C or D) = Z
   T    F       F    T    T   
   T    F       F    F    F 

We can represent these two test vectors on the expression tree:

        and
      /     \
    or1     or2
   /  \    /  \
  A    B  C    D


        and                          and
        [T]                          [F]
      /     \                      /     \
    or1     or2                  or1      or2
    [T]     [T]                  [T]      [F]
   /  \    /  \                 /   \    /   \
  A    B  C    D               A     B  C     D
 [T]  [F][F]  [T]             [T]   [F][F]   [F]

This is a pair for unique cause MC/DC.

Let's now consider a new pair of test vectors for condition D:

  (A or B) and (C or D) = Z
   F    T       F    T    T   
   T    F       F    F    F   

Again we can represent these two test vectors on the expression tree:

        and                          and
        [T]                          [F]
      /     \                      /     \
    or1     or2                  or1      or2
    [T]     [T]                  [T]      [F]
   /  \    /  \                 /   \    /   \
  A    B  C    D               A     B  C     D
 [F]  [T][F]  [T]             [T]   [F][F]   [F]

This is a pair for masking MC/DC because although the values for 3 conditions (A, B and D) have changed the change for conditions A and B is masked by the boolean operator 'or1' (i.e. the value of 'A or B' is unchanged).

So, for masking MCDC, the independence pairs for all condition D can be:

RapiCover screenshot