评价模型测试和模型检验以发现Simulink模型中的需求违反
Evaluating Model Testing and Model Checking for Finding Requirements Violations in Simulink Models
摘要：
Matlab/Simulink是一种开发和仿真语言，被网络物理系统（CPS）行业广泛用于动态系统建模。有两种主流的方法来验证CPS 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
