Understanding user understanding: determining correctness of generated program invariants

  • 引用：Staats M, Hong S, Kim M, et al. Understanding user understanding: determining correctness of generated program invariants[C]，Proceedings of the 2012 International Symposium on Software Testing and Analysis. 2012: 188-198.
  • 等级：CCF A ISSTA
  • 链接

1 介绍

  • 问题：软件测试涉及两部分，test input 和 test oracle，测试输入有很多自动化方法，而test oracle没有
  • 最近：出现程序不变量推断的相关研究，可以帮助生成test oracle
  • 问题：现有不变量推断方法需要人为参与，存在以下两个原因：
      1. 不变量应该是一种规范，但是是从我们需要验证的源代码中产生的
      1. 许多现有方法是动态的，只是从有限的运行轨迹中推测出可能的不变量。
      • 一项研究表明，0-60%的不变量在现实软件中是错误的，平均有10%[26]
    • 因此，自动不变量生成技术产生的不变量不适合做oracle，最后还得人工筛选不变量
  • 综上，当 user classification effectiveness，用户分类不变量的能力（分辨正确不变量的能力）好的时候，自动不变量生成技术才能真正发挥作用。然而，目前关注很少。
    • 早些工作探讨了用户使用动态不变量生成作为静态验证辅助工具的能力，得出的结论是区分正确和错误的不变量对用户来说是“相对容易的”[23]。遗憾的是，这项研究没有严格考虑用户的有效性，并且它是使用静态分析工具进行的，这些工具并不总是可用的
  • 本论文中展示两项经验性研究的成果，30人参与用户分类有效性的研究。这项工作目标有两个
      1. 确定使用动态不变量生成技术产生的不变量的用户分类有效性
      1. 了解导致分类成功或失败的原因
    • 实验内容：
        1. 给参与者提供3个Java程序之一，用Daikon生成不变量，要求参与者判断不变量是否正确
        1. 分析评估有效性的因素
    • 关键结果：
        1. 与先前研究结果相反，用户在正确分类不变量方面遇到了困难
        • 因此，为了减少人工检测不正确不变量的需求，除改进不变量生成技术外，还可以通过开发帮助用户理解不变量为何是正确的工具来改进
        1. 导致不变量错误分类的因素很微妙
  • 本文贡献
      1. 两项用户调研，调查用户准确分类，动态不变量检测中不变量的能力
      1. 证据表明：用户很难对正确的和不正确的不变量进行分类，与先前工作矛盾
      1. 对影响用户有效性的几个因素进行了分析
      1. 对结果讨论，讨论影响有效性的因素，突出了改善动态不变量生成的可用性的潜在方法

2 相关工作

  • 介绍了不变量生成技术
  • 上一个不变量用户研究[23]，其使用静态分析工具，得出的结果是好的，不适用于本文

3 研究设计

  • 3个问题
    • RQ1 How effective are users at classifying correct and incorrect invariants?
    • RQ2 How is user classification effectiveness influenced by program complexity/size?
    • RQ3 How does the difficulty of classifying invariants vary?

3.1 实验总览

  • 用户研究实验细则，过

3.2 Java样例程序

3.3 使用动态不变量生成

  • 使用Daikon的原因
      1. First, Daikon is the most mature and well documented freely available toolset, with a large body of related research [9, 10, 23, 26].
      1. Second, Daikon supports Java, which is familiar to our study participants
      1. Third, Daikon’s approach has been adopted by commercial tools, specifically Agitator [3], and thus represents a tool likely to be used in practice.
      1. Daikon是最成熟且文档全面可用的工具，有很多相关研究
      1. 可以使用在Java，参与者熟悉
      1. 已应用在实际
  • 使用Randoop test input generation tool [24]生成测试用例，因为其是Java生成测试用例的成熟工具。每个程序生成1000个测试用例。 为什么是1000，因为不变量正确性在 64.7% - 83.3%，需要足够多的测试用例来产生一些错误的不变量
  • Diakon可以产生3种类型的不变量：
    • method precondition
    • method postcondition
    • class invariant
    • 本实验中去除了method precondition，因为其不容易理解
  • Diakon输出采用 Java Modeling Language（JML）
    • 因其容易理解，且可以使用 JML 扩展编译 Java 来在测试期间检测到不变量的违规

3.4 Determining Invariant Correctness

3.5 Experiment Procedure

3.6 Threats to Validity

4 Results

RQ1

  • 假设和零假设 Hypothesis & null Hypothesis
    • Hypothesis: 用户在分类正确不变量时比分类错误不变量时有效
    • null Hypothesis: 用户对不正确和正确不变量的正确分类百分比分布相同。
  • 假设成立

RQ2

  • Hypothesis:小的简单的程序比大的复杂的程序更容易分类
  • null Hypothesis:程序大小和复杂度不同的程序不变量正确分类分布相同
  • 现有结果二者均不能明显支持（TODO：我还没看程序大小到底多大）

RQ3

  • 我们预期不变量往往要么显然正确或错误，因此非常容易分类，要么非常难分类，因此大多数用户都会错误分类。换句话说，我们预期每个子图都呈双峰分布，大多数不变量几乎被所有用户正确分类（接近100%，“容易”），或者几乎没有被任何用户正确分类（接近0%，“困难”），中间很少。
  • 然而，图中显示，我们的预期在任何研究、案例示例或不变量正确性的组合中都没有得到满足。
  • 因此，似乎没有一些特定的生成不变量类型X会导致所有用户都遇到困难的子集，需要确定与用户分类困难相关的因素

5 Discussion

在本节中，我们将研究与用户效果和不变量难度相关的其他潜在因素。在接下来的部分，我们将讨论我们结果的含义。

5.1 Establishing a Pattern of Difficulty 建立难度模式

  • 本研究的主要目标之一是确定与用户效果相关的因素。
    • 然而，我们需要首先确定是否存在这样的因素
      • 为此我们首先确定用户现过与不变量分类之间的难度是否存在关系（以用户错误分类的百分比衡量），难得不变量不易分类，简单的不变量容易分类
    • 由于没有难易不变量得存在，因此，我们无法确定与用户效果相关的因素
  • 为此我们根据以下假设建立难度模式，并进行实验验证，结果不是很明显
  • Hypothesis: 不变量I的错误分类用户百分比与所有检查I的用户的平均总体效果正相关

5.2 Statistical Analysis

  • 在单一因素和组合因素下，没有产生强有力的预测关系

5.3 Manual Analysis

  • 在我们的初步分析之后，我们对每个不变量进行了手动检查，试图找出用户误分类不变量的定性原因。特别是，我们对高比例的用户（>80%）倾向于误分类的不正确生成的不变量感兴趣。每位作者都独立进行了这项任务，发现了几种在这种情况下出现的模式
    • 模式1：对于信号异常状态的特定返回值的非排他性使用。
    • 模式2：直接、未经检查地操纵类变量值。
    • 模式3：不变量实用函数的潜在意外行为。
  • 由此推断，当使用动态不变量生成时，应注意
      1. 用户理解不变量语义
      1. 了解在应用程序的角落，特殊情况下，不变量可能不成立

6 implications 对未来工作的影响

  • 虽然我们的研究是从软件测试的角度进行的，但所研究的方面适用于任何用户必须理解动态不变量生成结果的情境

6.1 Crack the Code 破解代码

  • 我们以为不变量要么易于分类，要么难以分类，实际上大部分处于中间地带
  • 从统计分析上无法看到不变量分类的难度模型，手动分析只表明了一些导致不变量被错误分类的情景。
  • 我们的研究没有破解代码，说明仍需要改进，该技术仍具有挑战性
  • 然而，在4.3节中我们注意到不变量通常可以按难度排序，而难度与用户有效性有关。未来的工作，可能需要更大的样本量，才能找出原因。

6.2 Generation with Explanation and Better Invariant Filtering 生成带有解释的不变量和更好的不变量过滤

  • 本研究表明，用户很难对正确的和不正确的不变量进行分类，因此有必要改进以帮助他们理解正确的不变量

  • 目前，动态不变量生成是一个黑匣子，以程序轨迹作为输入，产生的程序不变量作为输出。

  • 然而，如果不变量生成能够提供更好地理解每个不变量为何生成，用户可能

      1. 更快地理解为什么一个不变量是正确的，减少证明时间
      1. 识别论证中的缺陷，从而改进识别不正确不变量的过程

  • 目前在Daikon种使用的使不变量失效的方法可以扩展使用更强大的技术。

    • 因为动态不变量生成依赖于程序轨迹，因此许多潜在有用的信息来源和分析技术未被使用
    • 包括：
      • 程序覆盖信息（覆盖的方法，探索的路径）
      • 静态分析技术，特别是证伪程序断言的技术[13]
      • 动态分析技术，符号/共模执行[27]
    • 通过以上技术，可以减少生成不正确不变量的数量

6.3 Quantify the Impact of User Error

  • 不变量分类错误有两类
    • 将正确的不变量分类为不正确
      • 此情况用户会想办法进行反正，花费用户时间
    • 将不正确的不变量分类为正确
      • 此情况较为严重，导致测试出现问题，造成对不变量信任缺失
  • 平均而言
    • 正确生成的不变量有9.1%至31.7%被错误分类
    • 而不正确生成的不变量有26.1%-58.6%被错误分类。
  • 本研究对用户能否实际使用这些不变量提出了质疑，在未来的工作中，了解用户错误如何对测试过程产生负面影响（确定不变量是否正确所需的时间，纠正测试中的假阳性所需的时间）是必要的，以了解动态不变量生成是否是一种成本效益的Oracle生成方法

7 结论

  • 进行亮相研究评估一个在动态不变量生成中关键的方面：用户理解并正确分类生成不变量的能力
  • 我们结果展示用户经常出错，与先前工作相冲突。
  • 进一步分析表明，尽管用户效率和分类不变量的困难度存在一些模式，但不变量困难度与其他因素之间的关系是微妙的。
    • 诸如程序复杂性、不变量大小、引用的类变量数量等因素并没有强相关性。
    • 然而，手动分析确实表明，与异常处理不当相关的某些边界情况可能导致几乎所有用户都错误地对复杂的不变量进行分类。
  • 为此，我们提出一些建议，弥补动态不变量生成技术和用户能力之间的差距
    • 通过额外的研究，进一步完善我们对不变量复杂性的理解；
    • 扩展现有技术，以支持用户理解为什么不变量是正确的，并减少生成的不正确不变量的数量；
    • 量化用户错误对不变量生成实际效果的影响。
    • 评估必须量化生成test oracle的潜在有效性，及用户应用它们的能力