通过集成有界模型检验与覆盖引导模糊测试改进模型测试

由 Simulink 或 Ptolemy 构建的控制逻辑模型已在工业场景中广泛使用。确保控制逻辑模型的安全性与可靠性成为迫切需求。测试用例生成技术被广泛用于保障安全性与可靠性。当前最先进的模型测试工具采用模型检验技术或基于搜索的方法生成测试用例。传统的基于 Simulink 仿真的搜索方法受限于速度慢、开销大等问题。传统的符号执行等模型检验技术在处理非线性元素和复杂循环时性能有限。近年来,覆盖引导模糊测试(fuzzing)技术因其在复杂循环分支上的高效性和显著效果,被认为在测试用例生成方面十分有效。本文中,我们应用模糊测试方法改进模型测试并论证其有效性。模糊测试方法旨在通过变异有价值的种子来覆盖更多程序分支。受此特性启发,我们提出一种新颖的集成技术 SPsCGF,其利用有界模型检验进行符号执行以生成测试用例作为初始种子,然后基于这些有价值的种子进行模糊测试。由此,我们的工作以新颖方式结合了模型检验方法与模糊测试技术的优势。由于控制逻辑模型始终接收信号输入,我们专门设计了针对信号的新颖变异算子,以改进现有模型测试中的模糊测试方法。在由工业案例构成的评估基准上,与最先进工作相比,SPsCGF 可实现高出 8% 至 38% 的模型覆盖率和 3 到 10 倍的时间效率。