Detecting Simulink Compiler Bugs via Controllable Zombie Blocks Mutation
Detecting Simulink Compiler Bugs via Controllable Zombie Blocks Mutation
复制标题
通过可控僵尸块突变检测 Simulink 编译器错误
DOI：
10.1145/3540250.3549159
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Rong Chen
中科院分区：
文献类型：
--
作者：
Shikai Guo;He Jiang;Zhihao Xu;Xiaochen Li;Zhilei Ren;Zhide Zhou;Rong Chen
作为一种流行的网络物理系统（CPS）开发工具链，MathWorks Simulink被广泛用于安全关键应用（例如航空航天和医疗保健）的CPS模型原型。由于所有CPS模型都依赖于编译，因此在实践中确保Simulink编译器（即Simulink的编译器模块）的正确性和可靠性至关重要。然而，由于数百万行源代码和缺乏完整的正式语言规范，Simulink编译器测试是具有挑战性的。虽然已经提出了几种自动测试Simulink编译器的方法，但仍然存在变异空间有限和变异多样性不足的问题。为了解决这些挑战，我们提出了COMBAT，一种新的用于Simulink编译器测试的差分测试方法。COMBAT包括等效模输入（EMI）突变组件和多种变体生成组件。EMI突变组件在种子CPS模型的任意点插入断言语句（例如，If /While块）。这些语句将每个插入点分解为真和假分支。然后，COMBAT将所有通过插入点的数据馈送到真正的分支中，以保持CPS变体的等价性。通过这种方式，假分支的主体可以被视为一个新的变体空间，从而解决了第一个挑战。多元变体生成组件利用马尔可夫链蒙特卡罗优化对种子CPS模型进行采样，并在变体空间中生成长序列块的复杂突变，从而解决了第二个挑战。实验表明，COMBAT在Simulink编译器测试中明显优于最先进的方法。在五个月内，COMBAT报告了Simulink R2021b的16个有效bug，其中11个bug已被MathWorks Support确认为新bug。
As a popular Cyber-Physical System (CPS) development tool chain, MathWorks Simulink is widely used to prototype CPS models in safety-critical applications, e.g., aerospace and healthcare. It is crucial to ensure the correctness and reliability of Simulink compiler (i.e., the compiler module of Simulink) in practice since all CPS models depend on compilation. However, Simulink compiler testing is challenging due to millions of lines of source code and the lack of the complete formal language specification. Although several methods have been proposed to automatically test Simulink compiler, there still remains two challenges to be tackled, namely the limited variant space and the insufficient mutation diversity. To address these challenges, we propose COMBAT, a new differential testing method for Simulink compiler testing. COMBAT includes an EMI (Equivalence Modulo Input) mutation component and a diverse variant generation component. The EMI mutation component inserts assertion statements (e.g., If /While blocks) at arbitrary points of the seed CPS model. These statements break each insertion point into true and false branches. Then, COMBAT feeds all the data passed through the insertion point into the true branch to preserve the equivalence of CPS variants. In such a way, the body of the false branch could be viewed as a new variant space, thus addressing the first challenge. The diverse variant generation component uses Markov chain Monte Carlo optimization to sample the seed CPS model and generate complex mutations of long sequences of blocks in the variant space, thus addressing the second challenge. Experiments demonstrate that COMBAT significantly outperforms the state-of-the-art approaches in Simulink compiler testing. Within five months, COMBAT has reported 16 valid bugs for Simulink R2021b, of which 11 bugs have been confirmed as new bugs by MathWorks Support.