Towards Formally Verified Optimizing Compilation in Flight Control Software
| Autor: | Bedin França, Ricardo, Favre-Felix, Denis, Leroy, Xavier, Pantel, Marc, Souyris, Jean |
|---|---|
| Přispěvatelé: | Airbus [France], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Programming languages, types, compilation and proofs (GALLIUM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Institut National Polytechnique (Toulouse) (Toulouse INP), ANR-08-SEGI-0021,U3CAT,Unification des Techniques d'Analyse de Code C Critique(2008), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées |
| Jazyk: | angličtina |
| Rok vydání: | 2011 |
| Předmět: |
000 Computer science
knowledge general works [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] avionics software 020204 information systems Computer Science 0202 electrical engineering electronic engineering information engineering 020207 software engineering code optimization [INFO.INFO-ES]Computer Science [cs]/Embedded Systems 02 engineering and technology Compiler verification WCET |
| Zdroj: | PPES 2011: Predictability and Performance in Embedded Systems PPES 2011: Predictability and Performance in Embedded Systems, Mar 2011, Grenoble, France. pp.59-68, ⟨10.4230/OASIcs.PPES.2011.59⟩ |
| DOI: | 10.4230/OASIcs.PPES.2011.59⟩ |
| Popis: | International audience; This work presents a preliminary evaluation of the use of the CompCert formally specified and verified optimizing compiler for the development of level A critical flight control software. First, the motivation for choosing CompCert is presented, as well as the requirements and constraints for safety-critical avionics software. The main point is to allow optimized code generation by relying on the formal proof of correctness instead of the current un-optimized generation required to produce assembly code structurally similar to the algorithmic language (and even the initial models) source code. The evaluation of its performance (measured using WCET) is presented and the results are compared to those obtained with the currently used compiler. Finally, the paper discusses verification and certification issues that are raised when one seeks to use CompCert for the development of such critical software. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|