Expérimentations en Coq pour un générateur de code qualifiable

摘要

Cet article présente une utilisation pragmatique de méthodes formelles pour la conception et la vérification de certains composants du générateur de code séquentiel GeneAuto, qualifiable pour les systèmes embarqués critiques selon les normes de certification DO178B. Ce générateur accepte un sous-ensemble des langages Simulink/Stateflow et SciCOS et produit du langage C au standard MISRA. Nous présentons les motivations principales du choix de l'assistant de preuve Coq, la méthode d'utilisation et son application à l'ordonnanceur de blocs. Le programme OCaML extrait, expérimenté pour des modèles industriels réels, fait partie de l'outil actuellement disponible.%This paper presents a pragmatic use of formal methods for the design and verification of components for the GeneAuto code generator that produces sequential software, which can be qualified according to the current standards for safety critical embedded systems for public transportation (i.e. DO178B). This code generator handles a subset of the Simuunk/Stateflow and Scicos languages and produces MISRA C code. This paper presents the main concepts guiding the choice of the Coq proof assistant, the proposed method, and its application to the block sequencer. The extracted OCaML program has been experimented and validated using real industrial models and is part of the currently available toolset.