Direction de recherche : Stef GRAILLAT
Co-encadrement : LAUTER Christoph, LARRIBE Fabrice

Génération automatique de tests pour la certification de codes en aéronautique

Ces travaux de thèse s'inscrivent dans le contexte de la validation et de la vérification de logiciels numériques pour la certification aéronautique. Dans cette thèse, nous proposons une solution de génération automatique de tests numériques fiables qui respectent les règles de développement imposées par le processus de certification.

Les tests, composés de stimulations associées à un comportement attendu, sont ainsi générés à partir d'une spécification du comportement fonctionnel du logiciel. Valider le logiciel par le test revient à lui donner les stimulations en entrée et comparer le résultat obtenu (binaire) au comportement déterminé à l'aide de la spécification fonctionnelle (décimal). La solution proposée utilise la programmation par contraintes (numériques) et une méthode combinatoire de résolution en domaine continu (intervalles) pour construire un pavage de l'espace réalisable par des boîtes intérieures (ne contenant que des solutions) et des boîtes frontières englobant généralement la frontière de la zone réalisable.

L'ensemble des tests est ensuite élaboré à l'aide du test par mutation sur les contraintes, qui permet d'évaluer la qualité de la campagne de test courante et d'ajouter de nouveaux tests si nécessaire. Les conversions entre les formats binaires et décimaux sont inévitables et introduisent des erreurs de calculs pouvant avoir un impact sur la fiabilité des résultats des tests.

Nous renforçons notre solution grâce à l'utilisation et développement d'arithmétiques fiables (arithmétique d'intervalles décimale multi-précision et arithmétique en bases mixtes binaire/décimale).

Soutenance : 21/05/2019

Membres du jury :

Jean-Michel Muller, CNRS Research Director [Rapporteur]
Gilles Trombettoni, Professor at Université de Montpellier [Rapporteur]
Sylvie Boldo, Inria Research Director
Fabrice Kordon, Professor at Sorbonne Université
Stef Graillat, Professor at Sorbonne Université
Christoph Lauter, Assistant Professor at University of Alaska
Fabrice Larribe, Engineer at Safran Electronics & Defense

Publications 2016-2023

• 2023
  • S. Graillat, Y. Ibrahimy, C. Jeangoudoux, Ch. Lauter : “A parallel compensated Horner scheme for SIMD architecture”, (2023)
• 2019
  • C. Jeangoudoux : “Automatic Test Generation for Numerical Software in the Context of Aircraft Certification”, soutenance de thèse, soutenance 21/05/2019, direction de recherche Graillat, Stef, co-encadrement : Lauter, Christoph, Larribe, Fabrice (2019)
• 2018
  • C. Jeangoudoux, Ch. Lauter : “A Correctly Rounded Mixed-Radix Fused-Multiply-Add”, 2018 IEEE 25^th Symposium on Computer Arithmetic (ARITH), Amherst, MA, United States, (IEEE) (2018)
  • M. Ceberio, A. Contreras, C. Jeangoudoux, F. Larribe : “Constraints over Intervals for Specification Based Automatic Software Test Generation”, 18^th international symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2018), 18^th international symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2018), Book of Abstracts, Tokyo, Japan, pp. 54-55 (2018)
• 2017
  • S. Graillat, Y. Ibrahimy, C. Jeangoudoux, Ch. Lauter : “A Parallel Compensated Horner Scheme”, CSE 2017, SIAM Conference on Computational Science and Engineering (CSE), Atlanta, United States (2017)
  • S. Graillat, C. Jeangoudoux, Ch. Lauter : “MPDI: A Decimal Multiple-Precision Interval Arithmetic Library”, Reliable Computing Journal, vol. 25, Volume 25 (Special volume containing refereed papers from SCAN 2016), pp. 38-52 (2017)
• 2016
  • S. Graillat, C. Jeangoudoux, Ch. Lauter : “A Decimal Multiple-Precision Interval Arithmetic Library”, book of abstracts : 17^th International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics., Uppsala, Sweden (2016)