Matlab/Simulink is widely used for model-based development of embedded systems. In particular, safety-critical applications are increasingly designed in Matlab/Simulink. At the same time, formal verification techniques for Matlab/Simulink are still rare and existing ones do not scale well. In this paper, we present an automatic transformation from discrete-time Matlab/Simulink to the input language of UCLID. UCLID is a toolkit for system verification based on SMT solving. Our approach enables us to use a combination of bounded model checking and inductive invariant checking for the automatic verification of Matlab/Simulink models. To demonstrate the practical applicability of our approach, we have successfully verified the absence of one of the most common errors, i. e. variable over- or underflow, for an industrial design from the automotive domain.

MATLAB Simulink is the most widely used industrial tool for developing complex embedded systems in the automotive sector. The resulting Simulink models often consist of more than ten thousand blocks and a large number of hierarchy levels. To ensure the quality of such models, automated static analyses and slicing are necessary to cope with this complexity. In particular, static analyses are required that operate directly on the models. In this article, we present an approach for slicing Simulink Models using dependence graphs and demonstrate its efficiency using case studies from the automotive and avionics domain. With slicing, the complexity of a model can be reduced for a given point of interest by removing unrelated model elements, thus paving the way for subsequent static quality assurance methods.