Formal specification of block libraries in dataflow languages

International audienceGraphical dataflow-style modeling languages like Simulink and Scicos are widely used in the development of embedded control systems as high-level engineering lan- guages. A significant part of their modeling power is captured in function block libraries. In this paper we present an on-going work on the model-based formalisation of such libraries, which intends to bridge the gaps between the different parts of the development process: high-level requirements, design, implementation and verification. Our approach is based on a specification domain specific language (DSL), which captures the variability of blocks through a software product line approach. We have defined translations to other languages like the Why3 language for verification, different documentation formats, code generator configuration files, etc. These experiments have been carried out in the context of the GeneAuto embedded code generator project and are being extended and applied in its successor projects ProjectP and Hi-MoCo