针对B方法中明确定义的约束条件，采用内部和外部性能模糊测试技术

《Formal Aspects of Computing》：Internal and External Performance Fuzzing of Well-Defined Constraints for the B Method

性能模糊测试用于发现ProB模型检查器的约束求解后端（如CLP(FD)、Z3、CDCL(T)）中的性能问题，并比较内部集成与外部控制器架构的差异。通过改进BanditFuzz算法生成Well-defined的B约束，结合Thompson采样和多臂老虎机策略，成功定位多个性能缺陷，包括SICStus Prolog的call_cleanup/2错误和Z3的时序处理问题。实验表明外部架构可有效检测ProB版本间的性能回归，而内部集成更易访问底层工具实现。研究验证了BanditFuzz在非SMT-LIB领域的适用性，并为后续优化提供关键洞察。

　　本文探讨了将BanditFuzz算法应用于B方法及其模型检查器ProB的约束求解后端，以发现潜在的性能问题。B方法是一种形式化方法，用于软件和系统开发，以及数据验证。其核心是使用B语言编写规范，该语言基于谓词逻辑、算术和集合论。ProB是B方法的一个模型检查器、动画器和约束求解器，它提供了多种约束求解后端，包括CLP(FD)、SAT和SMT。本文的研究重点在于利用性能模糊化技术，生成能够揭示不同后端之间显著性能差异的输入，从而提高模型检查和约束求解的效率和稳定性。

性能模糊化是一种软件测试技术，通过生成特定的输入来揭示程序的性能瓶颈或异常行为。BanditFuzz作为一种性能模糊化算法，使用两个多臂老虎机代理来控制模糊生成器和变异器，以生成具有显著性能差异的输入。与传统的模糊测试方法相比，BanditFuzz能够更精确地定位性能问题，同时保持输入的简洁性，以便于开发人员理解和调试。在将BanditFuzz应用于B方法时，需要特别关注输入的“定义良好性”（well-definedness, WD），因为B方法要求所有约束都必须满足定义良好的条件，以确保求解过程的正确性和完整性。

ProB的约束求解后端，尤其是其原生的CLP(FD)后端，需要处理定义良好的约束，这涉及对约束中潜在的未定义操作进行检查和修正。例如，如果一个约束中包含除以零的操作，那么该约束需要添加一个定义良好的前提条件，以确保其不会导致错误。此外，ProB还支持将约束转换为SMT-LIB格式，以便与第三方求解器如Z3进行交互。Z3的两种翻译方式，即基于量词的公理化公式和基于lambda函数的构造性翻译，分别对应不同的约束处理策略。本文的研究重点在于如何在B方法的语境下，将BanditFuzz算法进行适配，以确保生成的约束不仅具有定义良好的特性，还能揭示不同求解器之间的性能差异。

在实现BanditFuzz时，研究者面临两个主要的架构选择：内部集成和外部控制。内部集成意味着将模糊化过程直接嵌入ProB的源代码中，从而可以充分利用ProB的内部功能，如B编译器，来优化约束处理和求解。然而，这种集成方式限制了对不同ProB版本之间性能差异的比较，因为其依赖于特定的ProB版本。相比之下，外部控制架构则允许比较不同版本的ProB及其依赖的求解器，例如SICStus Prolog的不同版本，这为性能回归测试提供了更大的灵活性。然而，外部控制架构可能受到通信开销的影响，导致性能测量的准确性下降。因此，研究者在实验中使用了ProB的Java API，以减少外部控制带来的干扰。

在实验部分，研究者分别对ProB的内部集成架构和外部控制架构进行了测试。在内部集成架构下，他们发现了一些性能问题，例如在Prolog 4.8.0版本中，由于call_cleanup/2函数的bug，导致某些约束求解过程出现异常延迟。而在Prolog 4.9.0版本中，这一问题得到了修复，从而改善了整体性能。此外，研究者还发现了一些与约束求解相关的其他问题，如某些约束导致Z3求解器出现段错误，或者某些求解器在处理空集时未能正确识别，从而导致超时。这些发现不仅帮助改进了ProB的约束求解器，还对相关求解器如Z3进行了优化。

在外部控制架构下，研究者测试了不同ProB版本之间的性能差异。他们发现，在某些情况下，新版本的ProB在处理特定约束时的性能比旧版本有所下降，这表明可能存在性能回归。例如，在比较ProB 1.13.1-nightly版本与1.13.0版本时，研究者发现某些约束在旧版本中执行更快。此外，他们还测试了CLP(FD)后端在不同设置下的性能表现，如CHR（约束处理规则）、SMT模式以及求解器强度设置。结果表明，某些设置在特定约束上表现更优，而其他设置则可能在更复杂的情况下表现出更好的性能。

本文还讨论了与性能模糊化相关的其他研究工作。例如，SlowFuzz和PerfFuzz是早期的性能模糊化工具，它们使用基于进化算法的变异方法来生成具有高复杂度的输入。而Saffron和PySE则引入了强化学习的概念，通过调整生成器的策略来优化性能测试。在SMT求解器领域，SPRFinder是一种专门针对性能回归的模糊化工具，它使用修改后的BanditFuzz算法来比较不同版本的求解器性能。此外，还有基于机器学习的方法，如Healy等人的工作，通过预测求解器性能来优化求解策略。这些方法虽然各有优劣，但它们的核心目标都是发现和优化求解器的性能表现。

在讨论部分，研究者总结了实验中发现的问题和经验教训。例如，生成的约束可能过于复杂，导致无法有效比较不同求解器之间的性能差异。此外，由于约束的生成和变异过程可能重复利用相同的定义良好性条件，导致生成的约束具有相似的性能表现。为了克服这些问题，研究者建议引入更复杂的生成策略，例如自适应配置，以调整约束的复杂度，从而发现更多不同的性能问题。同时，他们也指出，虽然内部集成架构提供了更多的控制权，但外部控制架构在开发和维护过程中具有更高的灵活性，能够更好地支持不同版本之间的性能比较。

最后，本文得出结论，BanditFuzz作为一种性能模糊化工具，在B方法和ProB的约束求解后端中具有显著的价值。它不仅能够发现潜在的性能问题，还能为工具的优化和改进提供重要的反馈。尽管内部集成架构在某些方面具有优势，但外部控制架构在支持多版本比较和避免依赖特定版本方面更为灵活。因此，研究者建议未来将BanditFuzz作为外部工具进行开发，以便更好地适应不同的需求和场景。同时，他们也指出，未来的研究可以进一步探索其他性能指标，如内存使用和吞吐量，以更全面地评估工具的性能表现。