Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations.

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 inputs and parameters. Therefore, the automotive safety standard ISO 26262 recommends the usage of formal methods in safety-critical software development. In this paper, we report on the application of formal verification to check discrete-time properties of a Simulink model for a park assistant R&D prototype 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.