Certifying an Automated Code Generator Using Formal Tools: Preliminary experiments in the GeneAuto project.

Nassima Izerrouken (1) , Xavier Thirioux (2) , Marc Pantel (2, 3) , Martin Strecker (2)

1 IRIT - Institut de recherche en informatique de Toulouse
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 Toulouse INP - Institut National Polytechnique (Toulouse)

This paper reports on the study and early experiments of the available technologies for the formal validation and verification of Automated Code Generator which took place in the GeneAuto project. GeneAuto aims at the development of an ACG for a safe subset of the Matlab/Simulink/Stateflow modelling language which will be used for the development of certified safety critical embedded real time systems in the automobile, aeronautic and space domains and therefore subject to the certification authorities and standards of these domains. The chosen technology is illustrated through the development of a scheduler process for a safe subset of block diagrams. Our purpose is to develop and formally verify some parts of the GeneAuto ACG using the Coq proof assistant. Such a certified code generator guarantees that the correctness properties already proved on the model source code will still hold for the executable code.

Mots clés: Validation; Formal verification; Scheduler; Proof assistant; Coq; Certified systems; Automatic Code Generation

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

Nassima Izerrouken, Xavier Thirioux, Marc Pantel, Martin Strecker. Certifying an Automated Code Generator Using Formal Tools: Preliminary experiments in the GeneAuto project.. Embedded Real Time Software and Systems (ERTS2008), Jan 2008, Toulouse, France. ⟨hal-02270296⟩