Les dépôts de projets se font directement sur le site de l'IRT SAINT EXUPERY à l'adresse suivante :
Appel à projets IRT St EXUPERY Edition Novembre 2023 : https://www.irt-saintexupery.com/frae/

 

Merci de prendre connaissance de la fiche technique dans le dispositif d'appel à projets IRT ST EXUPERY Edition Novembre 2023 : FICHE TECHNIQUE

LES EXPERTS

Les Experts scientifiques et industriels sont des personnes « extérieures » à la Fondation.

EN SAVOIR +

COVERIF

Vers une combinaison de l’interprétation abstraite et de la programmation par contraintes pour la vérification de propriétés critiques pour des programmes embarqués avec des calculs en virgule flottante

Pouvoir vérifier la correction et la robustesse des programmes et systèmes devient un enjeu majeur dans une société où les applications embarquées sont de plus en plus nombreuses et où leur caractère critique ne cesse d’augmenter. C’est notamment un enjeu crucial pour le calcul basé sur l’arithmétique des nombres à virgule flottante, qui a des comportements assez inhabituels et qui est de plus en plus utilisée dans les logiciels embarqués. Notons par exemple le phénomène de “catastrophic cancellation” qui invalide la plupart des chiffres significatifs d’un résultat ou encore, des suites numériques dont le point de convergence est très différent sur les réels et sur les flottants. Un problème vient aussi de la difficulté à relier le calcul sur les flottants avec un calcul “idéalisé” qui serait effectué avec des nombres réels, la référence de fait lors de la conception du programme. Pour certaines valeurs d’entrée, le flot de contrôle lié aux réels peut ainsi passer dans une branche de la conditionnelle tandis qu’il passe par l’autre pour les flottants. S’assurer qu’un code, malgré cette divergence de flot de contrôle calcule tout ce qu’il est censé calculer, avec une erreur minimale, est l’objet de l’analyse de robustesse, ou de continuité. Le développement d’un ensemble de techniques et d’outils pour vérifier l’exactitude, la correction et la robustesse est donc un challenge important dans le domaine des logiciels embarqués critiques. L’objectif de ce projet est de contribuer à relever ce défi en explorant de nouvelles méthodes basées sur une collaboration fine entre interprétation abstraite (IA) et programmation par contraintes (PPC). Plus précisément, il s’agit de repousser les limites inhérentes à ces deux techniques, d’améliorer la précision des estimations, de permettre une vérification plus complète des programmes utilisant des calculs sur les flottants, et de rendre ainsi plus robustes les décisions critiques liées à ces calculs. Un des originalités de ce projet est de combiner les deux approches, pour permettre à la preuve de robustesse de bénéficier d’une précision accrue, par l’utilisation de techniques PPC, et le cas échéant, pour exhiber des cas non robustes. Il s’agit aussi de marier les forces des deux techniques : la PPC propose des mécaniques algorithmiques puissantes, mais chères en temps de calcul, pour atteindre des domaines d’une précision arbitraire fixée. L’IA n’offre pas de contrôle fin sur la précision atteinte, mais a développé de nombreux domaines abstraits qui capturent très rapidement des invariants de programme de formes diverses. En intégrant certains mécanismes de la PPC (arbre de recherche, heuristiques) dans des domaines abstraits, on pourra, en présence de fausses alarmes, raffiner le domaine abstrait en se basant sur une notion de précision. La première difficulté à résoudre est d’asseoir les bases théoriques d’un analyseur basé sur deux paradigmes substantiellement différents. Lorsque les interactions entre PPC et IA seront bien formalisées, le deuxième verrou que nous visons à lever est de gérer des contraintes de formes générales et des domaines abstraits potentiellement non-linéaires. Enfin, un verrou important du projet concerne l’analyse de robustesse de systèmes plus généraux que les programmes, par exemple les systèmes hybrides, qui modélisent les programmes de contrôle commande Les résultats des recherches menées dans ce projet seront validés sur des exemples réalistes issus du monde industriel, afin d’en déterminer l’intérêt et la pertinence. L’utilisation d’exemples réels est un des points clefs de la validation des approches explorées : de par la complexité dans le pire des cas des problèmes traités, les techniques proposées ne traitent de manière acceptable que des sous classes de problèmes. Ainsi, les solutions adoptées restent souvent liées aux problèmes ciblés.

Coordinateur et contact :

GOUBAULT Eric
goubault@lix.polytechnique.fr

  • Durée : 48 mois
  • Date de démarrage : 30/09/2015
  • Projet : terminé
 

Subvention FRAE : 375 583,50 €
Abondement FRAE : 37 558 €

Fondation de Recherche pour l'Aéronautique et l'Espace
F.R.A.E. - Bâtiment B612 - 3 rue Tarfaya - CS 34436 - 31405 Toulouse Cedex 4
Tél. : 05 61 00 67 80 - Mail : nathalie.spindler@irt-saintexupery.com