 |
 |
| News 17 Mars, 2009 : Rencontre ENS-UPVD à Paris - définition du langage source et des applications à traiter 11 Fév., 2009 : visio conférence - lancement du projet (ENS, UBO et UPVD) 5 Fév., 2009 : présentation de SARDANES au workshop ES_PASS : frontiers of abstract interpretation, Toulouse (slides). 1er Fév., 2009 : début du projet! |
Sémantique, Analyse et tRansformation
Des Applications Numériques Embarquées Synchrones 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.
   Membres du projet :
Julien Bertrane, Ecole Normale Supérieure
Patrick Cousot, Ecole Normale Supérieure, responsable scientifique Radhia Cousot, CNRS & Ecole Normale Supérieure Arnault Ioulalen, Université de Perpignan Via Domitia Damien Massé, Université de Bretagne Occidentale Matthieu Martel, Université de Perpignan Via Domitia, coordinateur |
 Appel à projets N° 6 - Méthodes de vérification des systèmes et logiciels Thème : Les techniques d’analyse pour la sûreté et la sécurité, Les techniques de vérification de code et l’intégration de composants Durée : 36 mois Date démarrage : Février 2009 Partenaires : Ecole Normale Supérieure Université de Bretagne Occidentale Université de Perpignan |