ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 30/4 - 2011  - pp.409-440  - doi:10.3166/tsi.30.409-440
TITRE
Expérimentations en Coq pour un générateur de code qualifiable

TITLE
Experimenting the use of Coq proof assistant for a qualified automated code generator

RÉSUMÉ
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.


ABSTRACT
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 SIMULINK/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.


AUTEUR(S)
Nassima IZERROUKEN, Marc PANTEL, Xavier THIRIOUX, Olivier SSI YAN KAI

Reçu le 16 février 2009.   

MOTS-CLÉS
générateur de code qualifié, vérification formelle, SIMULINK, ordonnancement de blocs, assistant de preuve Coq.

KEYWORDS
qualified code generator, formal verification, SIMULINK, block sequencing, Coq proof assistant.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (361 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier