Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development
This addresses the need for efficient testing and verification in automotive software development, but it is incremental as it builds on existing formal methods and tools.
The paper tackles the problem of formalizing informal textual requirements in automotive model-based development by proposing a unified approach for computer-assisted formal specification and automated translation into verification tool languages, enabling automated formal verification and test case generation.
In industrial model-based development (MBD) frameworks, requirements are typically specified informally using textual descriptions. To enable the application of formal methods, these specifications need to be formalized in the input languages of all formal tools that should be applied to analyse the models at different development levels. In this paper we propose a unified approach for the computer-assisted formal specification of requirements and their fully automated translation into the specification languages of different verification tools. We consider a two-stage MBD scenario where first Simulink models are developed from which executable code is generated automatically. We (i) propose a specification language and a prototypical tool for the formal but still textual specification of requirements, (ii) show how these requirements can be translated automatically into the input languages of Simulink Design Verifier for verification of Simulink models and BTC EmbeddedValidator for source code verification, and (iii) show how our unified framework enables besides automated formal verification also the automated generation of test cases.