CompCert qualifié pour l’avionique
ISIT
AbsInt annonce une avancée majeure avec la qualification officielle de son compilateur CompCert pour le Multi-Function Computer New Generation (MFC_NG) des avions ATR 42/72. Il s’agit d’une première permettant d’obtenir des crédits de certification via l’utilisation d’un compilateur, dans le cadre des normes aéronautiques DO-178C, DO-333 et DO-330.
Cette qualification ouvre la voie à une réduction significative des efforts de certification. En effet, l’utilisation de CompCert permet de démontrer la préservation des propriétés entre le code source et le code objet, même en présence d’optimisations compilateur. Cela autorise, dans certains cas, à remplacer certaines étapes de tests bas niveau par des vérifications formelles réalisées au niveau du code source.
CompCert se distingue comme le premier compilateur commercial optimisé formellement vérifié. Le code machine généré est mathématiquement prouvé conforme à la sémantique du langage C, garantissant un haut niveau de fiabilité. Il prend en charge plusieurs architectures, notamment ARM, PowerPC, x86, RISC-V et TriCore.
Grâce à cette qualification, les industriels du secteur aéronautique peuvent accélérer leurs cycles de développement, améliorer leurs performances applicatives et réduire les risques liés aux erreurs de compilation, tout en respectant les exigences de sécurité les plus strictes.
Cette qualification ouvre la voie à une réduction significative des efforts de certification. En effet, l’utilisation de CompCert permet de démontrer la préservation des propriétés entre le code source et le code objet, même en présence d’optimisations compilateur. Cela autorise, dans certains cas, à remplacer certaines étapes de tests bas niveau par des vérifications formelles réalisées au niveau du code source.
CompCert se distingue comme le premier compilateur commercial optimisé formellement vérifié. Le code machine généré est mathématiquement prouvé conforme à la sémantique du langage C, garantissant un haut niveau de fiabilité. Il prend en charge plusieurs architectures, notamment ARM, PowerPC, x86, RISC-V et TriCore.
Grâce à cette qualification, les industriels du secteur aéronautique peuvent accélérer leurs cycles de développement, améliorer leurs performances applicatives et réduire les risques liés aux erreurs de compilation, tout en respectant les exigences de sécurité les plus strictes.
