让测试人员摆脱污染测试目标的困扰
Freeing Testers from Polluting Test Objectives
摘要：
测试是检测软件缺陷的主要方法。测试人员面临的一个主要挑战在于制作有效的测试套件，能够以可管理的努力检测最大数量的错误。为了做到这一点，他们依赖于覆盖标准，它定义了一些精确的测试目标。然而，许多常见的标准指定了大量的目标，这些目标在实践中是不可行的或多余的，比如覆盖死代码或语义相等的突变体。众所周知，这样的目标对测试套件的设计是有害的，会影响测试人员工作的效率和精度。这项工作引入了一个健全的和可扩展的正式技术，能够修剪出一个大的白盒标准面板产生的不可行和冗余的目标的重要组成部分。简而言之，我们将这个具有挑战性的问题简化为证明测试代码中逻辑断言的有效性。该技术是在一个工具中实现的，该工具依赖于最弱前提演算和SMT求解来证明断言。该工具构建在Frama-C验证平台之上，我们根据特定的可扩展性需求对其进行了仔细调整。实验表明，该工具可以修剪出高达27%的测试目标在一个程序和规模的应用程序的20万行代码。
英文摘要：
Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting efficient test suites, able to detect a maximum number of bugs with manageable effort. To do so, they rely on coverage criteria, which define some precise test objectives to be covered. However, many common criteria specify a significant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the efficiency and precision of testers' effort. This work introduces a sound and scalable formal technique able to prune out a significant part of the infeasible and redundant objectives produced by a large panel of white-box criteria. In a nutshell, we reduce this challenging problem to proving the validity of logical assertions in the code under test. This technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C verification platform, which we carefully tune for our specific scalability needs. The experiments reveal that the tool can prune out up to 27% of test objectives in a program and scale to applications of 200K lines of code.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
