Specifying and Verifying Model Transformations for Certified Systems using Transformation Models

Andres Toom (1) , Arnaud Dieumegard (2) , Marc Pantel (1)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 IRT Saint Exupéry - Institut de Recherche Technologique

Model Driven Engineering (MDE) makes it possible to tackle the ever-rising complexity of developing safety critical systems by providing early verification & validation (V & V) and au- tomated model transformations. In order to have confidence in them, certification guidelines require full traceability between the transformation’s source and target and V & V to prove the correctness of the transformation and verification tools themselves. This work was carried out as a separate study based on the G ENE A UTO 1 project for the development of an automatic code generator for certified systems. It focuses on the use of the MDE “Transformation Model” approach from [1] as a compromise between the current industrial practice, trends in software engineering, safety standards and formal verification. It outlines the key points for the development of model transformations for certified systems and illustrates the use of a form of the “Transformation Model” on a preprocessing step in G ENE A UTO .

Mots clés: MDE; transformation model; embedded systems; certification; qualification; MOF; OCL

Domaines: Systèmes embarqués

Andres Toom, Arnaud Dieumegard, Marc Pantel. Specifying and Verifying Model Transformations for Certified Systems using Transformation Models. Embedded Real Time Software and Systems (ERTS 2014), Feb 2014, Toulouse, France. ⟨hal-02272309⟩