Génération automatique de tests logiciels dans le contexte de la certification aéronautique
Institution:
Sorbonne universitéDisciplines:
Directors:
Abstract EN:
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).
Abstract FR:
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).