迈向SMT解决方案的有效采样方法

《IEEE Transactions on Software Engineering》：Towards Effective Sampling of SMT Solutions

　　

摘要：

本研究致力于有效生成满足模理论（SMT）公式的多样化解决方案，主要针对位向量、数组和未解释函数的理论，这是软件和硬件测试中的关键任务。生成多样化的SMT解决方案有助于在验证和测试过程中发现故障和检测安全违规行为。这就引出了SMT采样问题，其目标是构建一个能够全面覆盖约束空间的多样化解决方案集。虽然高覆盖率对于探索系统行为至关重要，但在软件工程场景中，生成的解决方案数量也应保持较少。由于每个SMT解决方案通常对应一个测试用例或测试输入，因此为相同的覆盖率生成较少的解决方案可以直接减少测试时间和资源消耗，从而提高测试效率。在这项工作中，我们引入了PanSampler，这是一种新型的SMT采样器，它能够在生成较少解决方案的情况下实现高覆盖率。PanSampler结合了一种新的多样性感知SMT算法和采样后的优化策略，共同提升了其实际性能。它通过迭代采样、评估候选解并采用局部搜索来优化解决方案，确保在少量样本的情况下实现高覆盖率。在大量实际基准测试上的实验表明，PanSampler在达到高目标覆盖率方面表现出显著的优势，同时所需的解决方案数量比现有最先进的采样器更少。此外，我们对来自真实世界软件系统的实际案例进行的实证评估显示，PanSampler具有更强的故障检测能力。而且，在达到与竞争对手相同的故障检测效果时，PanSampler大大减少了所需的解决方案数量，从而提高了测试效率。我们的评估还验证了PanSampler的有效性...

显示更多