Evaluating Model Testing and Model Checking for Finding Requirements Violations in Simulink Models

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.