Formally verified optimizing compilation in ACG-based flight control software

Abstract : This work presents an evaluation of the CompCert formally specified and verified optimizing compiler for the development of DO-178 level A flight control software. First, some fundamental characteristics of flight control software are presented and the case study program is described. Then, the use of CompCert is justified: its main point is to allow optimized code generation by relying on the formal proof of correctness and additional compilation information instead of the current un-optimized generation required to produce predictable assembly code patterns. The evaluation of its performance (measured using WCET and code size) is presented and the results are compared to those obtained with the currently used compiler.
Type de document :
Communication dans un congrès
ERTS2 2012: Embedded Real Time Software and Systems, Feb 2012, Toulouse, France. 2012
Liste complète des métadonnées


https://hal.inria.fr/hal-00653367
Contributeur : Xavier Leroy <>
Soumis le : lundi 19 décembre 2011 - 14:05:16
Dernière modification le : mercredi 2 août 2017 - 10:07:12
Document(s) archivé(s) le : vendredi 16 novembre 2012 - 15:56:08

Fichier

erts2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00653367, version 1

Citation

Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, et al.. Formally verified optimizing compilation in ACG-based flight control software. ERTS2 2012: Embedded Real Time Software and Systems, Feb 2012, Toulouse, France. 2012. <hal-00653367>

Partager

Métriques

Consultations de
la notice

1933

Téléchargements du document

510