0 基于动态分析的软件不变量综合技术 (动态不变量综述)

  • 引用：Wang B, Lu SR, Jiang JJ, Xiong YF. Survey of Dynamic Analysis Based Program Invariant Synthesis Techniques[J]. Journal of Software, 2020, 31(6): 1681-1702(in Chinese). http://www.jos.org.cn/1000-9825/6014.htm
  • 软件学报

2 Searching for invariants using genetic programming and mutation testing

  • 引用：Ratcliff S, White D R, Clark J A. Searching for invariants using genetic programming and mutation testing[C]//Proceedings of the 13th annual conference on Genetic and evolutionary computation. 2011: 1907-1914.
  • CCF C GECCO
  • 链接

1.0 摘要

  • 本文贡献
    • 进化搜索可以用来找到程序不变量，就像Daikon发现的那样
    • 进化搜索能够考虑比基于模板的工具更广泛的不变量范围
    • 通过将突变测试与进化搜索相结合，可以识别出有趣的不变量

1.1 主要内容

  • 现有生成不变量工具的问题：Daikon的方法可以看作一个根据数据驱动暴力构造不变量的方法。尽管目前有许多启发式方法可以来减少不变量的生成数量，并向程序员展示最有用的不变量，但Daikon由于只能产生与模板对应的不变量，所有存在Daikon找不到有用不变量的情况
  • 突变测试
    • 原理：如果使用测试集T来测试程序p，那么假设p是正确的，它应该通过T中的所有测试。然而，如果对程序p进行小的语法更改（即突变）以产生p’，那么除非p和p’在语义上等价，否则p’应该无法通过测试集
    • 目的：评估测试套件的效力。它通过对源代码进行有意义的修改，即“突变”，然后运行测试套件来检测这些变化是否能够被检测到，从而评估测试用例的质量。
    • 不变量与突变测试的关系：使用不变量生成来消除语义等家从而提升突变测试的效率[21]；
      本文使用突变测试来提高不变量生成效率，同时进行排序

3. Automatic Requirement Extraction from Test Cases

  • 引用：Ackermann C, Cleaveland R, Huang S, et al. Automatic requirement extraction from test cases[C]， Runtime Verification: First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings 1. Springer Berlin Heidelberg, 2010: 1-15.

0 摘要

  • 本论文描述了一种从测试中提取功能需求的方法，其中测试采用输入向量（提供给系统）和输出（系统响应输入而产生）的形式。
    • 该方法使用数据挖掘技术从测试数据中推断不变式，并利用自动验证技术来确定这些提出的不变式中哪些确实是不变的，因此可以被视为需求。
    • 来自涉及汽车电子应用的试点研究的实验结果表明，使用完全覆盖软件结构的测试比结构性不可知的黑盒测试能够产生更完整的不变式。

1 介绍

  • 本文提出并评估了一种基于数据挖掘的方法，用于自动从可执行软件构件中提取需求。这项工作的动机是使需求文档更加准确和完整。

  • 用于遵循读-执行-写行为模型的软件

    • 首先，使用自动化测试生成器生成按照几种结构覆盖标准覆盖模型的输入序列集合；每个输入向量产生的输出结果也被收集
    • 然后，将数据挖掘工具应用于测试数据，以推断在整个测试集上保持不变的输入和输出变量之间的关系（不变式）
    • 在后续的验证步骤中，使用自动化工具检查哪些提出的不变式确实是不变的；通过这一步骤的不变式随后被提议作为需求。

  • 本文结构

    • 第2节提供了关于数据挖掘、不变式推理以及用于进行本研究的工具和验证技术的背景。
    • 第3节更详细地概述了我们的方法
    • 第4节和第5节介绍了涉及生产级汽车应用程序的试点研究结果
    • 第6节讨论了相关工作
    • 最后一节包含了我们的结论和未来工作的想法。

2 背景

  • 本项工作受到了Raz等人[18, 17]的启发，他们使用数据挖掘工具从运行系统的执行轨迹中推断不变式，用于异常检测的目的。我们的动机不同在于，我们的工作旨在从模型驱动开发的汽车系统程序测试数据中重建需求。

2.1 从运行中推断不变量

2.3 基于仪器的验证

3 提取需求

  • 步骤如下，依赖于使用覆盖测试和数据挖掘工具，从模型的模拟执行运行生成的测试数据中提出不变式，以及对这些不变式的随后验证。
  • 1 测试用例生成：通过自动化，基于覆盖的测试生成工具，在设计模型上运行生成的输出
  • 2 不变量推理：使用关联规则挖掘工具在第1步的测试数据中发现不变式。该工具提出了一组被认为是被检查模型的不变式的关联规则。我们只报告强度值等于1.0的不变式，这是强度分数可以达到的最大值[22]。这等价于意味着任何报告的不变式在观察到的数据中没有反例，即它是对执行推理的证据的真实不变式。
  • 3 不变式验证：模型覆盖度量仅仅保证关键元素（块、条件、决策等）在测试套件中至少执行了一次。当然，它们不能强制覆盖所有可能行为的完整覆盖（即路径覆盖）。这就是为什么推断出的不变式不能假设为真正的需求，并且必须进一步验证以便作为需求报告
    • 在Raz等人[18,17]这个验证是手动进行的。我们改为通过将每个候选要求转换为监控模型，并使用IBV来确定提出的不变式是否可以被证明无效，来自动化这个验证步骤。
    • 在执行这个验证时，验证工具将生成一个新的测试套件，该测试套件在其尝试最大化模型覆盖的过程中，将尝试违反监控模型。如果监控模型不满足，那么它所代表的假定不变式并非对所有轨迹都成立，因此被丢弃。如果监控模型满足，那么我们可以说，具有很高信心水平地，已经从设计模型中推断出一个有效的不变式，并且可以视为一个需求。

6 相关工作

  • Ernst等人提出的Daikon系统[8]在C、C++、Java和Perl编写的程序中动态检测“可能的不变式”。该方法的早期步骤使用代码插装器获取跟踪数据，这些数据被传递到其推理算法中。这些跟踪数据不能保证对检查中的程序有良好的覆盖；Ernst等人指出，可能需要对检查中的程序进行多次运行并结合。Daikon提出的不变式会检查冗余，但对于除了所提供的跟踪数据之外的测试用例，很难验证不变式的正确性

7 结论

  • 本文提出了一个从可执行软件工件（例如遵循读-计算-写行为模型的控制软件）中重建需求的框架。该方法依赖于对结构覆盖工件的测试数据应用数据挖掘技术，以导出形式为不变式的建议需求，表达输入和输出之间的关系。然后，该方法使用自动化验证步骤来识别假的不变式。该方法在一个用Simulink建模的生产汽车照明控制应用程序上进行了试点；实验数据表明，使用全覆盖测试数据比随机测试数据产生更好的不变式集，并且迭代应用该方法可以进一步改进这些不变式。
  • 作为未来的工作，我们希望进一步试验该方法，使用其他与汽车相关的Simulink模型。我们还希望研究使用不同的覆盖标准（如决策覆盖、MC/DC等）对不变式集质量的影响。最后，本研究中研究的不变式缺乏时间方面的内容；我们有兴趣追求允许推断包含时间元素的需求（例如“如果a发生，则b必须在x时间单位内发生”）的需求生成策略。

4 Dig

  • 引用：Nguyen T V, Kapur D, Weimer W, et al. DIG: A dynamic invariant generator for polynomial and array invariants[J]. ACM Transactions on Software Engineering and Methodology (TOSEM), 2014, 23(4): 1-30.
  • CCF A TOSEM

5 Feedback-driven dynamic invariant discovery

  • 引用：Zhang L, Yang G, Rungta N, et al. Feedback-driven dynamic invariant discovery[C]，Proceedings of the 2014 International Symposium on Software Testing and Analysis. 2014: 362-372.
  • CCF A ISSTA
  • 链接

6 Dysy: Dynamic symbolic execution for invariant inference

  • 引用：Csallner C, Tillmann N, Smaragdakis Y. DySy: Dynamic symbolic execution for invariant inference[C]，Proceedings of the 30th international conference on Software engineering. 2008: 281-290.
  • CCF A ICSE

N. Tillmann, F. Chen, and W. Schulte. Discovering likely
method specifications. Formal Meth. Softw. Eng., pages
717–736, 2006.

Y. Wei, C. Furia, N. Kazmin, and B. Meyer. Inferring better
contracts. In Int’l Conf. Softw. Eng., pages 191–200, 2011.

(疑似也是用户研究？)

[26] N. Polikarpova, I. Ciupa, and B. Meyer. A comparative study
of programmer-written and automatically inferred contracts.
In Int’l Symp. Softw. Test. Analy., pages 93–104, 2009.

（也有用户研究）

J. W. Nimmer and M. D. Ernst. Automatic generation of
program specifications. In Int’l Symp. Softw. Test. Analy.,
pages 232–242, July 2002.