[toc]

Ⅰ Automatic test case and test oracle generation based on functional scenarios in formal specifications for conformance testing

• TODO:还挺难的，慢慢看吧
• 引用：Liu S, Nakajima S. Automatic test case and test oracle generation based on functional scenarios in formal specifications for conformance testing[J]. IEEE Transactions on Software Engineering, 2020, 48(2): 691-712.
• CCF A TSE
• 链接

1 介绍

动机

• 因为用户更关注程序的行为而非内部结构，specification-based testing是一种有效的测试方法来检查conformance
• 由于一个功能通常有程序中一个或一组程序路径实现，因此理想情况下，conformance testing应该覆盖specification中归能的所有可能的路径,然而，这提出了一种挑战
  • 原则上，specification-based testing 仅根据specification生成测试用例，不考虑程序结构，这将导致需要的功能被检查但有的路径没有被测试。
  • 一种解决方法是进行结构测试，在此过程中故意生成满足路径覆盖的测试用例。目前，有许多从业者希望此类conformance testing可以自动化。正如业界公认的[15]，自动化结构测试很难，尤其在复杂代码中。符号执行在小规模程序中提供了有限的解决方案，但在复杂大规模的程序时遇到了严重的困难[16]。
  • 另一种解决方法是formalize用户的需求，达到每个功能都使用形式化符号精确定义的水平[17].此时，不仅可以自动生成测试用例[18]，还可以自动推导出用于测试解雇分析的明确定义的测试oracle。
  • 但一个有趣的尚未解决的问题是，如何仅仅基于specification自动生成测试用例，以便执行specification中所有功能，又能覆盖相应程序中所有相关的程序路径

方法

• 本文提出了一种 functional scenario-based vibration test case generation method（基于功能的情景振动测试用例生成方法。称为Vibration-Method或简称V-Method，反映在测试用例生成时“振动这一特征”
  • 该方法适用于数据类型丰富的信息系统的测试。其基本原则是将formal specification中的转换为等效的functional scenarios，然后基于这些functional scenarios以“振动的方式”生成测试用例
  • 测试用例生成和“振动”是我们方法的组成部分，决定了方法的有效性
  • 一个操作的 functional scenario 定义了其输入和输出的具体关系，在formal specification的背景下,功能场景被表达为一个谓词表达式，通过pre-condition和post-condition来形成，并期望定义用户需求specification中（通常为自然语言）中的一个所需功能
  • 正如2.1中所解释的，使用我们之前的工作[11],[21]中提出的算法自动推导出一个操作的所有功能场景，我们所倡导的策略是，生成的测试用例应覆盖所有的功能场景，同时覆盖程序中所有represntative program paths （REP），REP是通过将循环展开为条件执行语句得到的所有可执行语句的子集

贡献

• 1.:基于functional scenarios 提出了两个新的测试用例生成标准。
  • a. 一个要求生成足够的测试用例以覆盖specification中的所有功能场景，这与[2,22,23]中基于specification的测试方法不同
  • b. 另一个需要测试用例每一个功能场景的更多细节
  • 这两个标准 可以通过 input和output驱动的生成策略来实现
    • input-driven strategy: 选择输入变量的值（即测试用例），随后从specification中导出输出的期望值
    • output-driven strategy: 选择输出输出变量的期望值，随后根据所选的预期结果生成输入变量的相应测试用例。
  • Matinnejad等人在[24]、[25]中提出了在测试用例生成中考虑输出多样性的想法，但现有工作中缺乏从给定输出值派生测试用例的具体而准确的方法。我们的方法提供一具体和明确的基于形式化规格的方法，改进了这一点。
• 2.：描述了一系列自动测试用例生成的算法，部分算法在之前工作提出过[23]，但许多部分是在本工作中新开发的
• 3.：开发了一个名为V-Step的“振动”步骤，用于启发生成测试用例，目的是覆盖所有的REP。
• 4.：基于功能情景提出了一种分析测试结果自动派生oracle的机制。现有的类似方法使用整个前置和后置田间来形成每个测试结果分析的测试oracle，但我们的方法仅适用相关功能场景，只是前置和后置条件的一部分，来进行测试结果分析，更加高效

2 测试策略和标准

• 整体策略：从formal specification自动化生成测试用例，以覆盖specification中所有的功能场景，同时尽可能的实现程序覆盖

2.1 功能场景

• 一个specification的操作S定义为 $S(S_{iv},S_{ov})[S_{pre},S_{post}]$
  • $S_{iv}$: 在操作后输入变量中未改变的值
  • $S_{ov}$: 在操作后操作产生或修改的值
  • $S_{pre}，S_{post}$: 操作的前置，后置条件（为简化问题，假设相关的不变量已经并入前置和后置条件中，并且前置和后置条件都不含量化表达式）
• 为了编写操作的前置和后置条件，采用了机构化面向形式语言SOFL[28]，其整合了VDM-SL[29]和数据刘图。
• 令 $P$ 为实现操作 $S$ 的程序,为了确保 $P$ 实现正确，应保证
  $$\forall_{\sigma \in \sum } · S_{pre}(\sigma) \Rightarrow S_{post}(\sigma,P(\sigma)) （1）$$
  ,其中 $\sum$ 表示 $S$ 所有可能的状态，$S$ 可以看作程序 $P$ 的一种抽象，其总体上是一个状态转换系统,像一个函数，从初始状态映射到结束状态。该公式成立需要满足条件，所有初始状态 $\sigma$ 都满足 $S_{pre}$ 时，最终状态状态 $\sigma$ 下的输出满足 $S_{post}$
• 理论上，使用测试验证公式（1）需要穷尽测试，尝试 $S$ 所有可能的输入，这是不现实的。我们的方法旨在对specification $S$ 生成足够的测试用例，以覆盖用户独特功能需求中所定义的所有功能。这样的功能可以由下面的功能场景定义给出。

Definition 1:functional scenario

• 令 $S_{post} \equiv (G_1 \wedge D_1) \vee (G_2 \wedge D_2).. \vee(G_n \wedge D_n)$,其中 $G_i(i \in \{1,...,n\})$ 表示一个成为守卫条件的谓词，不包含在 $S_{ov}$的输出中， $D_i$ 是一个定义的条件包括至少一个在 $S_{ov}$ 中的输出变量，但不包含守卫条件。 然后，一个功能场景的定义为一个合取 $S_{pre} \wedge G_i \wedge D_i$,同时 $(S_{pre} \wedge G_1 \wedge D_1) \vee (S_{pre} \wedge G_2 \wedge D_2) \vee ... \vee (S_{pre} \wedge G_n \wedge D_n)$ 被称为操作 S 的功能场景形式（functional scenario form FSF）
• 将 $S_{pre} \wedge G_i \wedge D_i$ 视为一个功能场景，因为其定义了一个独特的功能：当初始状态满足 $S_{pre} \wedge G_{i}$ (或者直观的说，输入满足时)，最终状态有 $D_i$ 定义。 将定义条件与 pre-条件和守卫条件的合取分开，将便于我们基于这个合取生成测试数据，并基于合取和定义条件形成测试oracle。

Definition 2:complete specification

• 令 $(S_{pre} \wedge G_1 \wedge D_1) \vee (S_{pre} \wedge G_2 \wedge D_2) \vee ... \vee (S_{pre} \wedge G_n \wedge D_n)$，则 $S$ 完备当且仅当 $G1 \vee G2 \vee … \vee Gn \Leftrightarrow true $恒成立
• 注意，这里对操作规范的完全性定义可能与传统理解不同，传统理解要求规范定义用户的所有需求。相反，我们的定义要求任何满足前条件的输入必须满足其中一个守卫条件（例如，G1），从而保证只要所有的定义条件都是可满足的，操作的输出就可以由相应的定义条件（例如，D1）定义。正如我们将在后续的第4.5节中讨论的，规范的完全性影响了我们测试方法的有效性。

Example 1: Check Triangle

• $Check_Triangle_{iv}=\{d1,d2,d3\}$
• $Check_Triangle_{ov}=\{t_{type}\}$
• $Check_Triangle_{pre}=true$
• $Check_Triangle_{post}=(d1=d2 \; and \;d2=d3 \; t_{type}="equilateral\;triangle"...$
• 根据以上specification可以得到以下功能场景
  • （1）
    • $G_1:d1=d2 \; and\; d2=d3$
    • $D_1:t_{type} = "equilateral\;triangle"$
    • $FS_1:G_1\; and\;D_1 \; (\Leftrightarrow Check_Triangle_{pre}\; and \; G1 \; and\;D1)$
  • （2）
    • $G_2:d1=d2 \; or \; d2=d3 \; or \; d1=d3$
    • $D_2:t_{type} = "isosceles\;triangle"$
    • $FS_2:G_2\; and\;D_2 \;$
  • （3）
    • $G_3:d1\not ={}d2 \; or \; d2\not ={}d3 \; or \; d1\not ={}d3$
    • $D_3:t_{type} = "other \;triangle"$
    • $FS_3:G_3\; and\;D_3 \;$
  • （4）
    • $G_4:d1\leq 0 \; or \; d2\leq 0 \; or \; d3\leq 0$
    • $D_4:t_{type} = "now-triangle"$
    • $FS_4:G_4\; and\;D_4 \;$

2.2 测试用例生成标准

Define 3 test data

• 测试数据是对所有输入变量从其类型中分配值的一种赋值。

Define 4 test case

• 测试用例是测试数据和期望输出值的组合
• 令 $S_{iv} = \{x_1,x_2,...x_n\},S_{ov}=\{y_1,y_2..y_m\}$ 为操作 $S$ 的所有输入集和输出集. 令 $Type(z)$ 表示输入变量或输出变量的类型，$z\in\{x_1,x_2..x_n,y_1,y_2..y_m\}$.
• 一个测试用例，用 $tc$ 表示，是一个从集合 $S_{iv}$ 到集合 $S_{ov}$ 的映射，即
  $$tc: S_{iv} \cup S_{iv} \rightarrow Values$$
  $$tc(z) \in Type(z)$$
  ,其中 $Values=Type(x_1)\cup ...Type(x_n)\cup Type(y_1) \cup .. Type(y_m)$
• 一个测试用例经常被表示为一组 输入变量或输出变量和相应的值的组合，例如 $tc=\{(x1,5),(x2,3),(y1,8)\}$

Define 5 test set

• 一个测试集合是一组测试用例的集合。通常表示为一组成对的集合。
• 一个测试套件是一个预期用于特定目的的测试集合。

Define 6 test condition

• 令 $S_{pre}\wedge G \wedge D$ 为操作 $S$ 的一个功能场景，随后 $S_{pre}\wedge G$ 称为功能场景的 测试条件
• 由于测试条件 $S_{pre}\wedge G$ 只包含操作的输入数据，因此用于检查条件 $D$ 是否正确实现的测试数据（或没有预期结果的测试用例）仅基于测试条件生成。 定义条件形成了测试oracle，如2.3所述

Define 7 restricted domain

• 操作S的受限域是操作域的子集，在每个子集中，每个值都满足操作规范的前置条件。

Define 8 program

• 一个程序是一个5元组 $(S_0,SN,CN,R,T)$ , $S_0$ 是开始节点， $SN$ 状态节点集合，$CN$ 条件节点集合，$R$ 关系中节点，$T$ 是终止节点，它们满足以下条件
  • 1. $S_0 \in SN \cup CN$
  • 2. $R:(SN\cup CN) \times (SN\cup CN) $
  • 3. $T \in SN$
• 一个程序可以被表示为一个由五个元素 $S_0,SN,CN,R,T$ 组成的语义等价图，满足上述三个条件。
  • 程序中的每个语句，包括空语句（用 skip 表示），都由 SN 中的一个节点表示，称为语句节点。
  • 每个条件（一个谓词）都由 CN 中的一个节点表示，称为条件节点。
  • 节点之间的连接（包括语句节点和条件节点），反映了语句之间的控制流，由关系 R 表示。
  • 起始节点 S0 表示程序的第一个语句或条件。
  • 终止节点 T 中的节点表示在程序的执行中必须最后执行的语句。
  • 一个程序还具有这样的特点，即每个条件节点都与另外两个唯一的节点相连接，每个节点都是一个语句节点或条件节点

Define 8 program path

• 令 $P=(S_0,SN,CN,R,T)$ 为程序，一个程序路径 $p$ 一个节点序列 $[S_0,n_1,n_2,...n_m],n_m\in T$.
• 我们令 $E(p) = \{(S_0,n1),(n_1,n_2),...(n_{m-1},n_m)\}$
• 程序路径是由节点序列组成的，从程序的起始节点开始，以一个终止节点结束。这条路径也可以被视为由路径上所有边构成的关系。为了避免任何可能的混淆，我们使用 $E(p)$ 来表示路径对应的关系。

Define 9 representative program path

• 令 $P=(S_0,SN,CN,R,T)$ 为程序，使用 $Rpp(P)$ 表示程序的代表性路径集合，需要满足下面两个条件
  • (1) $\forall_{e\in R \exist_{p\in Ppp(P)} · e \in E(p)}$
  • (2) $\forall_{p\in Rpp(P)} · \neg \exist_{p_1\in Rpp(P)} · E(p) \subseteq E(p1)$
• $Rpp(P)$ 并不代表 $P$ 的唯一一组代表程序路径，根据定义，它包含了覆盖 $P$ 的所有控制流边的所有程序路径，如条件 (1) 所示，并且不包含在其相应关系中重叠控制流边的不同程序路径，如条件 (2) 所暗示的。在本文中，我们总是使用 $Rpp(P)$ 来表示基于测试需求确定的感兴趣的代表程序路径集合。

Define 10 traversd path

• 令 $P=(S_0,SN,CN,R,T)$ 为程序，$P$ 的一个路径 $p$ 被称为被遍历的，当 $P$ 被执行时，如果 $p$ 中的所有节点都按照它们在路径上出现的顺序被执行（在语句的情况下）或评估（在条件的情况下），我们说 $p$ 被遍历了。
• 根据以上10个定义，即可为测试用例生成定义标准

Criterion 1:scenario-path coverage (SPC)

• 令 $P$ 为实现操作 $S$ 的程序，$(S_{pre}\wedge G_1 \wedge D_1) \vee ()S_{pre}\wedge G_2 \wedge D_2) \vee ... \vee (S_{pre}\wedge G_n \wedge D_n)$ 为操作 $S$ 的FSF. 令 $T$ 为从 $S$ 中生成的测试集。 $T$ 满足以下4个条件
  • (1) $\forall_{i\in\{1,...n\}} \exist_{tc\in T} · S_{pre}(tc)\wedge G_i(tc)$
  • (2) $\neg (G_1 \vee G_2 ... \vee G_3 \Leftrightarrow true) \Rightarrow \exist_{tc\in T} · S_{pre}(tc)\wedge \neg (G_1\vee G_2 \vee ...G_n)(tc)$
  • (3) $\exist_{tc\in T} · \neg (S_pre(tc))$
  • (4) $\forall_{p\in Ppp(P)} \exist_{tc\in T} · traversed(p,tc)$
• 该标准称为场景路径覆盖SPC。 该标准建议生成的测试集覆盖规范中的所有功能场景和程序中的所有代表程序路径。具体来说满足以4个条件
  • (1)对于每个功能场景，必须存在一个在 $T$ 中的测试用例满足功能场景的测试条件
  • (2)如果所有守卫条件的析取不能覆盖操作的受限域，那么必须存在一个在 $T$ 中的测试用例满足所有守卫条件析取的否定
  • (3)必须存在一个违反前置条件的测试用例
  • (4)对于每个代表性程序路径，必须存在一个测试用例在程序中遍历了这个路径，用 $traversed(p,tc)$ 表示
• 该测试标准中
  • (1)(2)共同体现了基于精确定义的功能性测试场景测试条件的等价类划分技术来生成测试用例[30,31]
  • (3)不能帮助确定测试用例是否发生了错误，因为SOFL中的置-后置风格规范允许在违反前置条件时程序的任何行为，这与完善的精化理论[32]一致，但它可以起到类似于健壮性测试技术[33]的作用，并帮助测试者或开发者判断在这种情况下程序的行为对用户来说是否可接受。
  • (4) 对应于简单路径覆盖测试[31]

Criterion 2

P. W. O’Hearn, “Continuous reasoning: Scaling the impact of formal
methods,” in Proceedings of the 33rd annual ACM/IEEE symposium
on logic in computer science, 2018, pp. 13–25.

Krka, I.; Brun, Y.; Medvidovic, N. Automatically Mining Specifications from Invocation Traces and Method Invariants; Technical Report; Citeseer; Center for Systems and Software Engineering, University of Southern California: Los Angeles, CA, USA, 2013. [Google Scholar]

De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S. Automated abstractions for contract validation. IEEE Trans. Softw. Eng. 2010, 38, 141–162. [Google Scholar] [CrossRef]

David R. MacIver, Zac Hatfield-Dodds, and Many Other
Contributors. Hypothesis: A new approach to property based testing. Journal of Open Source Software,
4(43):1891, 2019.