Génération automatique de tests logiciels dans le contexte de la certification aéronautique

Autor: Jeangoudoux, Clothilde
Přispěvatelé: Performance et Qualité des Algorithmes Numériques (PEQUAN), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Sorbonne Université, Stef Graillat, Sorbonne Université - UFR d'Ingénierie (UFR 919), Sorbonne Université (SU), Sorbonne Universites, UPMC University of Paris 6, Chrisoph Lauter, Fabrice Larribe, Jeangoudoux, Clothilde
Jazyk: francouzština
Rok vydání: 2019
Předmět:
Arithmétique des ordinateurs
[INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE]
Arithmétique à virgule flottante
arith- métique à virgule flottante
[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
constraint programming
Programmation par contraintes
programmation par contraintes
rithmétique des ordinateurs
analyse d’erreur
Générateur automatique de tests
Certification aéronautique de programmes numériques
Constraint programming
[INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]
multi-précision
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Floating-point
[INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC]
d’intervalles
[INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic
Analyse d'erreur
[INFO.INFO-NA]Computer Science [cs]/Numerical Analysis [cs.NA]
Computer arithmetic
[INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation
[INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Aircraft certification of numerical software
binary and decimal arithmetics
Error analysis
[INFO.INFO-NA] Computer Science [cs]/Numerical Analysis [cs.NA]
binaire et décimale
d'intervalles
Automatic test generator
[INFO.INFO-AO] Computer Science [cs]/Computer Arithmetic
multiple precision
[INFO.INFO-MO] Computer Science [cs]/Modeling and Simulation
interval
Zdroj: Arithmétique des ordinateurs. Sorbonne Université, 2019. Français. ⟨NNT : 2019SORUS148⟩
Arithmétique des ordinateurs. Sorbonne Universites, UPMC University of Paris 6, 2019. Français
Popis: This work has been done in the context of the validation and verification of numerical softwarefor aircraft certification. In this thesis we develop an automatic generator of reliable numerical test, ac-cording to the development rules mandated by the certification process. The tests, composed of stimu-lations associated with an expected behavior, are thus generated from a specification of the functionalbehavior of the software. Validation by test of the software means that, with the simultations given as in-puts of the software, we compare the obtained result (binary) with the expected behavior identified usingthe functional specification (decimal). This work uses Constraint Programming (numerical constraints)and a combinatorial method of continuous domain resolution (intervals) to construct a paving of the fea-sible set by inner boxes (containing only solutions) and outer boxes encompassing the boundary of thefeasible region. All tests are then developed using the Mutation Testing on constraints, which evaluatesthe quality of the current test campaign and adds new tests if needed. Conversions between binary anddecimal formats are inevitable and introduce computational errors which can impact the reliability oftest results. We strengthen our solution through the development and use of reliable arithmetic (multi-precision decimal interval arithmetic and binary/decimal mixed-radix arithmetic).
Ces travaux de thèse s’inscrivent dans le contexte de la validation et de la vérification de logicielsnumé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 parle 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 lo-giciel 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éeutilise la programmation par contraintes (numériques) et une méthode combinatoire de résolution endomaine 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 zoneréalisable. L’ensemble des tests est ensuite élaboré à l’aide du test par mutation sur les contraintes, quipermet d’évaluer la qualité de la campagne de test courante et d’ajouter de nouveaux tests si néces-saire. Les conversions entre les formats binaires et décimaux sont inévitables et introduisent des erreursde calculs pouvant avoir un impact sur la fiabilité des résultats des tests. Nous renforçons notre solu-tion grâce à l’utilisation et développement d’arithmétiques fiables (arithmétique d’intervalles décimalemulti-précision et arithmétique en bases mixtes binaire/décimale).
Databáze: OpenAIRE
Externí odkaz: