论文标题
通过整合有限的模型检查和覆盖范围指导性模糊来改善模型测试
Improve Model Testing by Integrating Bounded Model Checking and Coverage Guided Fuzzing
论文作者
论文摘要
Simulink或托勒密建立的控制逻辑模型已在行业场景中广泛使用。迫切需要确保控制逻辑模型的安全性。测试案例生成技术被广泛用于确保安全和保障。最先进的模型测试工具采用模型检查技术或基于搜索的方法来生成测试用例。基于Simulink仿真的传统基于搜索的技术会受到低速和高架开销等问题的困扰。在处理非线性元素和复杂循环时,传统的模型检查技术(例如符号执行)的性能有限。最近,由于其高效率和对复杂的循环分支的效果,覆盖范围引导的模糊技术对测试案例的生成有效。 在本文中,我们采用模糊方法来改善模型测试并证明有效性。模糊的方法旨在通过突变有价值的种子来涵盖更多的程序分支。受此功能的启发,我们提出了一种新颖的集成技术SPSCGF,该技术利用有限模型检查符号执行,以生成测试用例作为初始种子,然后根据这些值得种子进行模糊。通过这种方式,我们的工作结合了模型检查方法和模糊技术的优势。由于控制逻辑模型始终接收信号输入,因此我们专门为信号设计了新型的突变操作员,以改善模型测试中现有的模糊方法。在由工业案例组成的评估的基准测试中,SPSCGF与最先进的作品相比,SPSCGF可以实现8%至38%的模型覆盖率和3x-10倍的时间效率。
The control logic models built by Simulink or Ptolemy have been widely used in industry scenes. It is an urgent need to ensure the safety and security of the control logic models. Test case generation technologies are widely used to ensure the safety and security. State-of-the-art model testing tools employ model checking techniques or search-based methods to generate test cases. Traditional search based techniques based on Simulink simulation are plagued by problems such as low speed and high overhead. Traditional model checking techniques such as symbolic execution have limited performance when dealing with nonlinear elements and complex loops. Recently, coverage guided fuzzing technologies are known to be effective for test case generation, due to their high efficiency and impressive effects over complex branches of loops. In this paper, we apply fuzzing methods to improve model testing and demonstrate the effectiveness. The fuzzing methods aim to cover more program branches by mutating valuable seeds. Inspired by this feature, we propose a novel integration technology SPsCGF, which leverages bounded model checking for symbolic execution to generate test cases as initial seeds and then conduct fuzzing based upon these worthy seeds. In this manner, our work combines the advantages of the model checking methods and fuzzing techniques in a novel way. Since the control logic models always receive signal inputs, we specifically design novel mutation operators for signals to improve the existing fuzzing method in model testing. Over the evaluated benchmarks which consist of industrial cases, SPsCGF could achieve 8% to 38% higher model coverage and 3x-10x time efficiency compared with the state-of-the-art works.