ABSTRACT. The automotive industry makes increasing usage of Simulink-based software development. Typically, automotive Simulink designs are analyzed using non-formal test methods, which do not guarantee the absence of errors. In contrast, formal verification techniques aim at providing formal guarantees or counterexamples that the analyzed designs fulfill their requirements for all possible input and parameters. Therefore, the safety standard ISO 26262 recommends the usage of formal methods for the software development process for safety-critical systems.

In this paper, we report on the application of formal verification to check discrete-time properties of a previously tested Simulink model for a park assistant feature using the commercial Simulink Design Verifier tool. During our evaluation, we experienced a gap between the offered functionalities and typical industrial needs, which hindered the successful application of this tool in the context of model-based development. We discuss these issues and propose solutions related to system development, requirements specification and verification tools, in order to prepare the ground for the effective integration of computer-assisted formal verification in automotive Simulink-based development.