https://www.mdu.se/

The evolution of automotive systems has been rapid. Nowadays, electronic brains control dozens of functions in vehicles, like braking, cruising, etc. Model-based design approaches, in environments such as MATLAB Simulink, seem to help in addressing the ever-increasing need to enhance quality, and manage complexity, by supporting functional design from predefined block libraries, which can be simulated and analyzed for hidden errors, but also used for code generation. For this reason, providing assurance that Simulink models fulfill given functional and timing requirements is desirable. In this paper, we propose formal syntax and semantics of Simulink blocks and their composition, and introduce the tool SIMPPAAL that automates a previously introduced pattern-based, execution-order preserving transformation of Simulink atomic and composite blocks into stochastic timed automata. The resulting model can then be analyzed formally with UPPAAL Statistical Model Checker. We validate the approach on an industrial prototype called the Brake-by-Wire system. This work enables the formal analysis of industrial Simulink models, by automatically generating their semantic counterpart.