  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.
