BlueCov：将测试覆盖与基于JBMC的模型检测相集成
软件工程
2023-01-02 v1 编程语言
摘要
自动化测试用例生成工具帮助企业编写测试，并在进行代码变更时通过高回归测试覆盖率提供更大的安全网。测试生成需要尽可能覆盖未覆盖的代码，同时避免为已被现有测试套件覆盖的代码生成冗余测试。在本文中，我们介绍了一种用于将形式化分析与自动测试用例生成相集成的实际工具的工作。测试用例生成基于使用Java有界模型检测器（JBMC）的覆盖分析。模型检测器的反例可被翻译为带有特定参数的Java方法调用。为避免生成冗余测试，必须以与JBMC生成其覆盖目标完全相同的方式度量覆盖率。每个现有的覆盖率度量工具都使用略有不同的插桩，从而使用不同的覆盖准则。这使得与基于形式化分析的测试用例生成器集成变得困难。因此，我们开发了BlueCov作为一种特定的运行时覆盖率度量工具，其使用与JBMC完全相同的覆盖准则。该方法还允许增量式测试用例生成，仅为先前未测试的代码生成测试覆盖，例如，以补全现有测试套件。
引用
@article{arxiv.2212.14779,
title = {BlueCov: Integrating Test Coverage and Model Checking with JBMC},
author = {Matthias Güdemann and Peter Schrammel},
journal= {arXiv preprint arXiv:2212.14779},
year = {2023}
}
备注
Extended version of paper at SAC'23