up: Publications

Certifying an Automated Code Generator Using Formal Tools : Preliminary Experiments in the GeneAuto Project

Nassima Izerrouken, Xavier Thirioux, Marc Pantel, Martin Strecker


Abstract

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.

Online Copy

Available here

BibTeX Entry

@InProceedings{ IzThPaSt2008.2,
author = {Izerrouken, Nassima and Thirioux, Xavier and Pantel, Marc and Strecker, Martin},
title = "{Certifying an Automated Code Generator Using Formal Tools : Preliminary Experiments in the GeneAuto Project}",
booktitle = "{European Congress on Embedded Real-Time Software (ERTS), Toulouse, 29/01/2008-01/02/2008}",
year = {2008},
publisher = {Soci\'et\'e des Ing\'enieurs de l'Automobile},
address = {http://www.sia.fr/dyn/publications_detail.asp?codepublication=R-2008-01-10C01},
pages = {(electronic medium)},
language = {anglais}
}


Last modified: Thu Jul 30 11:02:52 CEST 2009