SARDANES

SCADE est un langage largement utilisé pour le développement de systèmes embarqués critiques synchrones. D’abord utilisé pour la spécification, la simulation et la vérification de propriétés de sûreté de haut niveau, ce langage permet aussi de produire un code final via un processus de compilation. Il est alors légitime que l’utilisateur souhaite que les propriétés prouvées sur le modèle soient garanties pour le code objet. Actuellement, le principal obstacle à cela est que la sémantique de SCADE spécifie que les calculs sont effectués en nombres réels. Or le programme final utilise des nombres flottants dont l’arithmétique est très différente de celle des réels, notamment à cause des erreurs d’arrondi. Le but de ce projet est d’utiliser des techniques de transformation d’expressions tenant compte de la précision des calculs pour garantir la préservation des propriétés numériques lors de la compilation de SCADE. Les preuves de correction reposent sur une interprétation abstraite des différentes traces d’exécution obtenues.