Verification of Requirements in Simulink Design Verifier and UPPAAL - an Industrial Case Study

Model checking has reached a state of maturity that allows its adoption for the verification of complex embedded systems, such as the ones found in vehicles. Little research has been carried out in order to determine how model checking can be integrated with the current design and verification practices at the industry. In this case study we take a real control subsystem of a Scania vehicle, specified as a Simulink model, and use two popular model checker (Simulink Design Verifier and Uppaal) for verifying its functional requirements according to the design specification. Our goal is to understand the real challenges faced by engineers performing model checking, and also to assess the possibilities and limitations of the available tools. The main difficulties encountered relate to the fact that most of the work still has to be performed manually, and depends significantly on the skills of the user. In particular, much effort has to be spent in formalizing the system requirements and in model-to-model transformation. This work shows that better tool support is required for these activities before model checking can be ready for widespread use in current development processes.QC 20220215ESPRESSO/VeriSpe