Génération automatique de tests logiciels dans le contexte de la certification aéronautique
| Autor: | Jeangoudoux, Clothilde |
|---|---|
| Přispěvatelé: | Sorbonne Université - UFR d'Ingénierie (UFR 919), Sorbonne Université (SU), Sorbonne Universites, UPMC University of Paris 6, Stef Graillat, Chrisoph Lauter, Fabrice Larribe, 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é |
| Jazyk: | francouzština |
| Rok vydání: | 2019 |
| Předmět: |
Arithmétique des ordinateurs
Arithmétique à virgule flottante arith- métique à virgule flottante [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] constraint programming Programmation par contraintes automatic test generator programmation par contraintes computer arithmetic rithmétique des ordinateurs analyse d’erreur Constraint programming floating-point certification aéronautique de programmes numériques error analysis multi-précision [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] d’intervalles [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic Analyse d'erreur générateur automatique de tests [INFO.INFO-NA]Computer Science [cs]/Numerical Analysis [cs.NA] [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation binary and decimal arithmetics d'intervalles binaire et décimale multiple precision aircraft certification of numerical software interval |
| Zdroj: | Arithmétique des ordinateurs. Sorbonne Universites, UPMC University of Paris 6, 2019. Français Arithmétique des ordinateurs. Sorbonne Université, 2019. Français. ⟨NNT : 2019SORUS148⟩ |
| Popis: | This work is done in the context of the validation and verification of numerical software for aircraft certification. In this thesis we develop an automatic generator of relaiable numerical test, according to the development rules mandated by the certification process. The tests, composed of stimulations associated with an expected behavior, are thus generated from a specification of the functional behavior of the software. Validation by test of the software means that given the simultations are inputs of the software, we compare the obtained result (binary) with the expected behavior identified using the 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 feasible set by inner boxes (containing only solutions) and outer boxes encompassing the boundary of the feasible region. All tests are then developed using the Mutation Testing on constraints, which evaluates the quality of the current test campaign and adds new tests if needed. Conversions between binary and decimal formats are inevitable and introduce computational errors which can impact the reliability of test 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 vérification de logiciels numériques dans 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 le développement d'arithmétiques fiables (arithmétique d'intervalles décimale multi-précision et arithmétique en bases mixtes binaire/décimale). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|