证明MC/DC唯一原因定义符合性

Question

我正在阅读关于MC/DC的以下文章:http://shemesh.larc.nasa.gov/fm/papers/Hayhurst-2001-tm210876-MCDC.pdf.

我有源代码:Z := (A or B) and (C or D)以及以下测试用例:

-----------------
| 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 |
-----------------

我想证明所提到的测试用例符合唯一原因定义.

我开始消除蒙面测试:

• A or B = F T T T T,这意味着它掩盖所述第一测试情况下,从C or D作为F and (C or D) = F.
• C or D = T T F T T,意思是它掩盖了A or Bas 的第三个测试用例(A or B) and F = F.

然后我决定MC/DC:

所需的测试用例A or B:

• F F (第一个案例)
• T F (第五种情况)
• F T (第二或第四种情况)

所需的测试用例C or D:

• F F (第三种情况)
• T F (第四或第五种情况)
• F T (第二种情况)

所需的测试用例(A or B) and (C or D):

• T T (第二,第四或第五个案例)
• F T (第一个案例)
• T F (第三种情况)

根据该论文,该示例不符合唯一原因定义.相反,他们建议将第二个测试用例更改F T F T为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 |
-----------------

我确定MC/DC了A or B试:

• F F (第一个案例)
• T F (第五种情况)
• F T (第四个案例)

然后,他们引入了以下独立对表,显示了两个示例之间的差异(第38页):

我理解,对于第一个例子,它们显示的独立对改变了两个变量而不是一个变量,但我不明白它们是如何计算独立对的.

在A列中,我可以推断它们F F T F从测试用例表的A行中获取,并且它们将独立对计算为仅具有Achanged(T F T F)的相同测试用例.

B然而,在专栏中,他们F F T F再次选择.根据我的想法,这应该等于B专栏:F T F T相反.

其余的字母显示出同样的困境.

同样对于D第一个示例专栏,他们表明独立对F T F T是T F F F,这破坏了我的理论,即他们从第一个值计算独立对,并证明他们从其他地方挑选它.

有人可以更好地解释他们如何(以及从哪里)构建这样的独立配对表？

Answer 1

首先让我们重新阅读定义:

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

DO-178B/ED-12B包括以下定义:

条件

不包含布尔运算符的布尔表达式.

决策

由条件和零个或多个布尔运算符组成的布尔表达式.没有布尔运算符的决策是一个条件.如果某个条件在决策中出现不止一次,则每次出现都是不同的条件.

决策覆盖范围

程序中的每个进入和退出点至少被调用一次,程序中的每个决定都至少采取了一次可能的结果.

修改条件/决策覆盖范围

程序中每个进入和退出点至少被调用一次,程序中的每个条件都至少采取了一次所有可能的结果,程序中的每个决策都至少采取了一次所有可能的结果,并且每个条件在一项决定中,已经证明可以独立地影响该决定的结果.通过在保持固定所有其他可能条件的同时改变该条件,显示条件独立地影响决策的结果.

因此,对于'(A或B)和(C或D)'的决定,我们有四个条件:A,B,C和D

对于每个条件,我们必须找到一对测试向量,表明条件"独立地影响该决策的结果".

对于唯一原因MC/DC,只有所考虑的条件的值可以在测试向量对中变化.

例如,让我们考虑条件A.以下一对测试向量涵盖条件A:

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

使用这对测试向量(TFTF,FFTF),只有A和Z的值(决定)发生变化.

然后我们搜索对条件B,C和D.

使用RapiCover GUI(Rapita Systems的Qualifiable Code coverage工具 - www.rapitasystems.com/products/rapicover),我们可以看到完整的测试向量(观察或缺失),以完全覆盖决策的所有条件.

RapiCover截图

Vector V3(上面屏幕截图中的黄色)不用于任何独立对.条件D的MC/DC覆盖缺少矢量V6(屏幕截图中的红色).

这是为了'独特原因'MC/DC的定义.

现在'掩盖MC/DC':

对于"屏蔽MC/DC" ,如果表达式中的布尔运算符屏蔽了任何其他更改,则放宽单个条件的值在一对测试向量中可能变化的要求.

例如,让我们考虑条件D的一对向量:

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

我们可以在表达式树上表示这两个测试向量:

        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]

这是一对独特的原因MC/DC.

现在让我们考虑条件D的一对新测试向量:

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

我们再次可以在表达式树上表示这两个测试向量:

        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]

这是用于屏蔽MC/DC的一对,因为虽然3个条件(A,B和D)的值已经改变,但条件A和B的变化被布尔运算符'or1'掩盖(即'A或B的值' '没有变化).

因此,为了屏蔽MCDC,所有条件D的独立对可以是:

RapiCover截图