Expérimentations en Coq pour un générateur de code qualifiable / Experimenting the use of the Coq proof assistant for a qualified automated code generator

IZERROUKEN, Nassima ; PANTEL, Marc ; et al.

In: Méthodes formelles pour l'analyse statique et la compilation, Jg. 30 (2011), Heft 4, S. 409-440

academicJournal - print, 2 p

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.

Titel:	Expérimentations en Coq pour un générateur de code qualifiable / Experimenting the use of the Coq proof assistant for a qualified automated code generator
Autor/in / Beteiligte Person:	IZERROUKEN, Nassima ; PANTEL, Marc ; THIRIOUX, Xavier ; SSI YAN KAI, Olivier
Link:	View record from PASCAL Archive
Zeitschrift:	Méthodes formelles pour l'analyse statique et la compilation, Jg. 30 (2011), Heft 4, S. 409-440
Veröffentlichung:	Paris: Lavoisier, 2011
Medientyp:	academicJournal
Umfang:	print, 2 p
ISSN:	0752-4072 (print)
Schlagwort:	Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences et techniques communes Sciences and techniques of general use Mathematiques Mathematics Logique mathématique, fondements, théorie des ensembles Mathematical logic, foundations, set theory Logique et fondements Logic and foundations Théorie de la preuve et mathématiques constructives Proof theory and constructive mathematics Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Informatique théorique Theoretical computing Fonctions logiques, booléennes et de commutation Logical, boolean and switching functions Logiciel Software Génie logiciel Software engineering Performances des systèmes informatiques. Fiabilité Computer systems performance. Reliability Démonstration automatique Automatic proving Demostración automática Génération code Code generation Generación código Langage OCaml OCaml language Lenguaje OCaml Modélisation Modeling Modelización Méthode formelle Formal method Método formal Norme sécurité Safety standard Norma seguridad Système critique Critical system Sistema crítica Sécurité informatique Computer security Seguridad informatica Séquenceur Sequencer Secuenciador Séquençage Sequencing Transport public Public transportation Transporte público Vérification programme Program verification Verificación programa Vérification formelle Formal verification Verificación formal Coq proof assistant SIMULINK block sequencing formal verification qualified code generator
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: French Original Material: INIST-CNRS Document Type: Article File Description: text Language: French Author Affiliations: IRIT- Université de Toulouse INPT-ENSEEIHT 2 rue Camichel, 31071 Toulouse, France ; Continental Automotive France SAS 1, Av. Ourliac, 31036 Toulouse, France Rights: Copyright 2015 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems ; Mathematics

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.