一句话:提出 SLforge,面向 Simulink 等商业 CPS 工具链自动生成模型并差分测试,以发现工具链缺陷。
商业信息物理系统(CPS)工具链(如 MathWorks Simulink)广泛用于 CPS 数据流模型的设计、仿真与验证,并生成部署在嵌入式系统中的代码二进制;形式化验证这类工具链目前不可行,测试加固因而关键。现有差分测试框架 CyFuzz 难以生成语言特性丰富的模型,且未利用非形式 Simulink 规范,也缺少现有 Simulink 模型研究来指导生成真实模型。为此,论文提出 SLforge,自动生成富语言特性的 Simulink 模型,并对商业工具链做差分测试,以发现缺陷。评估在真实商业工具链上检验模型生成与缺陷发现能力。
Cyber-physical system (CPS) development tool chains are widely used in the design, simulation, and verification of CPS data-flow models. Commercial CPS tool chains such as MathWorks' Simulink generate artifacts such as code binaries that are widely deployed in embedded systems. Hardening such tool chains by testing is crucial since formally verifying them is currently infeasible. Existing differential testing frameworks such as CyFuzz can not generate models rich in language features, partly because these tool chains do not leverage the available informal Simulink specifications. Furthermore, no study of existing Simulink models is available, which could guide CyFuzz to generate realistic models.
@inproceedings{paperbot4506,
title = {Automatically finding bugs in a commercial cyber-physical system development tool chain with SLforge},
author = {Shafiul Azam Chowdhury and Soumik Mohian and Sidharth Mehra and Siddhant Gawsane and Taylor T. Johnson and Christoph Csallner},
booktitle = {ICSE},
year = {2018},
doi = {10.1145/3180155.3180231}
}