0-2014-jfla-s.md

plugin: "general"
authors: "Julien Signoles"
title: "Comment un chameau peut-il écrire un journal ?"
book: "Journées Francophones des Langages Applicatifs (JFLA)"
year: 2014
category: kernel
short: "In French. Presentation of the journalization mechanism of Frama-C."

Dans Frama-C, plate-forme d'analyse de code C développée en OCaml, un journal est un script OCaml généré automatiquement et permettant de reproduire les actions utilisateurs, notamment effectuées via l'interface utilisateur. Outre la reproductibilité des résultats qui est nécessaire dans un contexte industriel soumis à des exigences de certication fortes comme la norme avionique DO-178C, un journal permet d'automatiser le pilotage de l'outil dans un contexte d'utilisation particulier. Cet article présente comment le mécanisme de génération du journal de Frama-C, appelé journalisation et requérant intrinsèquement de l'introspection, a été développé en OCaml, en combinant typage statique et dynamique.