一种基于状态规格说明的OBDD测试用例生成方法

摘要：为了有效地在规格说明层面对软件系统进行测试，A.J.Offutt[1]针对系统的状态规格说明定义了一系列覆盖准则，并阐述了如何基于系统的状态表示生成满足覆盖准则的基本方法。本文引入了一种应用于大型集成电路设计的数据结构OBDD（有序二叉决策图）作为生成测试用例的基本结构，创新地提出了一种新的生成测试用例方法。

关键词：测试 基于状态说明 全断言覆盖准则 OBDD

中图分类号：TP311 文献标识码：A 文章编号：1007-9416（2013）01-0152-01

在软件测试中生成测试用例的依据是形式覆盖准则[2]。形式覆盖准则为测试人员如何定义测试用例提供依据，通过形式覆盖准则所定义出的测试用例更容易发现软件系统中存在的错误。形式覆盖准则同样也在测试的有效性和充分性之间确定了平衡点。使用形式覆盖准则生成测试用例对软件系统进行测试可以有效保证软件系统的质量。Offutt在他的研究中，定义了四种可以用于状态说明的全断言覆盖准则。有序决策二叉图OBDD （ordered binary decision diagram）是一种用于表示布尔函数的数据结构，由Bryant[3]提出。这篇文章提出了一种基于OBDD生成测试用例的新方法。.

1 基于状态说明的测试

状态说明是规格说明中的一种。FSM可以用于表示状态说明。FSM的节点表示状态，节点间的有向边则表示状态之间的转换事件。 转换事件和转换条件都由布尔变量表示。FSM可以导出到状态变换的谓词表达式，在图1中，状态变换的谓词表达式为 （elevSpeed=0）∧（openButton=pressed）.

2 使用OBDD生成测试用例

全断言覆盖准则要求一个表达式中的所有子项都能影响谓词表达式的值。在p=a∧（b∨c）中，如果子项a 的值为真，那么b和c无论是什么值，都不能改变p，所以在这个谓词表达式中，b和c是多余子项，如果多余子项映射到规格说明中，就是设计当中的一个冗余，甚至是逻辑错误。

OBDD可以针对全断言覆盖准则，对谓词表达式进行分析，检测表达式中是否有多余子项。谓词表达式的OBDD是由终节点和决策节点组成的有向并且不循环图。每一个决策节点N代表一个布尔变量 V1，它拥有的0子节点和1子节点。沿0子节点往下代表V1取值为假，反之则为真。给定一组布尔变量，并确定其顺序，则从根到终节点的路径所经过的决策节点的顺序都相同，这样的决策二叉树称为是有序的。OBDD可以根据改变子项顺序和简化原则进行简化[4]，从而简化测试用例生成过程。

对于表达式p=a∧（b∨c）选择顺序abc，未简化的OBDD如图2（a）所示，对其应用简化准则后，新的OBDD如图2（b）。由根寻找一条到节点c的路径，路径上节点a和节点b的取值，就是节点c可以决定表达式p=a∧（b∨c）的取值环境。此例中，a取1，b取0。确定了子项c的取值环境后，就可以生成针对c的满足全断言覆盖的测试用例：

case1：a=1 b=0 c=0 case2：a=1 b=0 c=1

用同样的方法，生成针对子项a和子项b的满足全断言覆盖的测试用例：

case3：a=0 b=0 c=0 case4：a=1 b=0 c=0

case5：a=1 b=0 c=0 case6：a=1 b=1 c=0

注意到测试用例1，4以及5是相同的，故对于表达式p=a∧（b∨c），满足全断言覆盖准则的测试用例为：

case1：a=1 b=0 c=0 case2：a=1 b=0 c=1

case3：a=1 b=1 c=0 case4：a=0 b=0 c=0

参考文献

[1]A.J.Offutt.Generating test data from state-based specification.SOFTWARE TESTING， VERIFICATION AND RELIABILITY.2003.

[2]Paul Ammann，A.J.Offutt. Introduction To Software Testing.2008.

[3]R.E.Bryant.Graph-based algorithms for Boolean function manipulation.IEEE Trans Computer.Aug.1986.

[4]Bern，J，CH.OBDD-Based Boolean manipulation in CAD beyond current limits.ACM/IEEE Design Automation Conference.1995.