Formal specification of block libraries in dataflow languages

Arnaud Dieumegard (1, 2, 3) , Andres Toom (2, 4, 5) , Marc Pantel (2, 3)

1 IRT Saint Exupéry - Institut de Recherche Technologique
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 Toulouse INP - Institut National Polytechnique (Toulouse)
4 TTÜ - Tallinn University of Technology
5 IB Krates OÜ

Graphical 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.

Mots clés: model driven engineering; feature modeling; formal specification; software qualification; automatic code generation; Simulink; Scicos; Xcos; Why3

Domaines: Informatique [cs]; Systèmes embarqués

Arnaud Dieumegard, Andres Toom, Marc Pantel. Formal specification of block libraries in dataflow languages. Embedded Real Time Software and Systems (ERTS 2014), Feb 2014, Toulouse, France. ⟨hal-02272313⟩