Seminar Room 1, ground floor (Building IMAG)
2 mars 2017 - 14h00
« De Frama-C à Lustre »
par Loïc Correnson de CEA - Equipe LIST
Résumé : La plateforme Frama-C permet de prouver des propriétés fonctionnelles et des propriétés de robustesse sur des fonctions C, grâce au langage de spécifications ACSL, et grâce aux plugins WP et EVA déjà bien rodés.
Cependant, ACSL n'est pas adapté à la spécification de propriétés temporelles des programmes réactifs synchrones écrits en C. Au contraire, Lustre est un langage idéal pour écrire des observateurs et spécifier de telles propriétés. Mais les programmes C réactifs ne sont pas nécessairement produits à partir d'un source Lustre/Scade.
Cet exposé présente un nouveau plugin Frama-C qui combine les API publiques de EVA et WP pour extraire un modèle Lustre à partir d'un programme C réactif et synchrone. Il présente aussi comment utiliser ce plugin pour spécifier et prouver des propriétés écrites en Lustre sur un vrai logiciel de contrôle-commande.
