一句话：构建工业 Simulink 模型基准，系统比较模型测试与模型检测发现需求违规的能力，并给出二者互补与联合使用指南。
Matlab/Simulink 被信息物理系统工业广泛用于动态系统建模，但其需求违规验证常依赖模型测试与模型检测两类主流方法；二者在真实工业模型上的适用性、强弱及互补性尚缺乏系统评估。本文提出一个工业 Simulink 模型基准，对其中模型类型进行分类，总结需求中反复出现的逻辑模式，并分别应用模型测试和模型检测来发现需求违规。基于结果，论文分析了两类方法的优势与局限，表明它们具有互补性：结合使用可显著提升单独方法的能力，并进一步给出如何协同应用两类方法的实践指南。
Matlab/Simulink is a development and simulation language that is widely used by the Cyber-Physical System (CPS) industry to model dynamical systems. There are two mainstream approaches to verify CPS Simulink models: model testing that attempts to identify failures in models by executing them for a number of sampled test inputs, and model checking that attempts to exhaustively check the correctness of models against some given formal properties. In this paper, we present an industrial Simulink model benchmark, provide a categorization of different model types in the benchmark, describe the recurring logical patterns in the model requirements, and discuss the results of applying model checking and model testing approaches to identify requirements violations in the benchmarked models. Based on the results, we discuss the strengths and weaknesses of model testing and model checking. Our results further suggest that model checking and model testing are complementary and by combining them, we can significantly enhance the capabilities of each of these approaches individually. We conclude by providing guidelines as to how the two approaches can be best applied together.
@inproceedings{paperbot5051,
title = {Evaluating model testing and model checking for finding requirements violations in Simulink models},
author = {Shiva Nejati and Khouloud Gaaloul and Claudio Menghi and Lionel C. Briand and Stephen Foster and David Wolfe},
booktitle = {FSE},
year = {2019},
doi = {10.1145/3338906.3340444}
}