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 eectué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.
\ No newline at end of file
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.
