# Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development

## TL;DR

This paper presents a unified, automated approach for formal specification, translation, verification, and testing in automotive model-based development, streamlining requirements analysis across different tools.

## Contribution

It introduces a formal requirement specification language and a tool that automatically translates requirements into multiple verification tools' languages, enabling integrated verification and testing.

## Key findings

- Automated translation of requirements into verification tools' languages.
- Unified framework supports formal verification and test case generation.
- Enhances consistency and efficiency in automotive MBD processes.

## Abstract

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.