线性约束上的梯形泛化

我们正在开发一个基于模型的模糊测试框架，该框架利用系统行为的数学模型来引导模糊测试过程。传统模糊测试框架随机生成测试，而基于模型的框架可使用约束求解器从行为模型推导出测试。由于模糊测试所探索的状态空间通常很大，测试向量的快速生成至关重要。然而，快速生成测试的需求与约束求解器的使用相矛盾。我们对此问题的解决方案是：使用约束求解器生成初始解，相对于系统模型对该解进行泛化，然后对泛化后的解空间进行快速、重复、随机的采样以生成模糊测试。此工作成功的关键在于一种具有合理大小与性能开销、且能产生可高效采样的泛化解空间的泛化过程。本文描述了一种针对由线性约束的布尔组合所表达的逻辑公式的泛化技术，该技术满足基于模型的模糊测试的独特性能需求。该技术使用梯形解集表示泛化，梯形解集由有序、分层的线性约束合取组成，其表达能力强于简单区间，但比通用多面体更易于操作和采样。支撑材料包含一个ACL2证明，验证了泛化算法底层实现相对于泛化正确性规范的正确性。最后描述了一种后处理过程，其产生受限的梯形解，即使对于整数域也可无回溯地快速高效采样（求解）。虽然给出了非形式化的正确性论证，但限制算法正确性的形式化证明仍是未来工作。