Dans le cadre du séminaire « Méthodologies et Technologies innovantes pour les systèmes embarqués » organisé par la DGA à Toulouse, les 5 et 6 Novembre 2013, CLEARSY intervient lors de la session Génération de code par les modèles – preuve formelle au travers d’un exposé, « Génération de code formellement prouvé pour des applications embarquées redondantes », au cours duquel nous présentons notre retour d’expérience concernant la génération de code à partir de modèles formels, pour des applications sécuritaires à forte redondance. Les architectures ciblées comptant jusqu’à 9 processeurs, des précautions particulières ont permis de prendre en compte la diversification du code source et/ou du code binaire, et de l’associer à des techniques de vérification formelle appropriées.