Supervision : Stef GRAILLAT
Co-supervision : LAUTER Christoph, LARRIBE Fabrice
Automatic Test Generation for Numerical Software in the Context of Aircraft Certification
This work has been done in the context of the validation and verification of numerical software for aircraft certification. In this thesis we develop an automatic generator of reliable 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, with the simultations given as 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).
Defence : 05/21/2019 - 14h - Campus Pierre et Marie Curie, salle Jacques Pitrat (25-26/105)
Jury members :
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
- S. Graillat, Y. Ibrahimy, C. Jeangoudoux, Ch. Lauter : “A parallel compensated Horner scheme for SIMD architecture”, (2023)
- C. Jeangoudoux : “Automatic Test Generation for Numerical Software in the Context of Aircraft Certification”, thesis, defence 05/21/2019, supervision Graillat, Stef, co-supervision : Lauter, Christoph, Larribe, Fabrice (2019)
- C. Jeangoudoux, Ch. Lauter : “A Correctly Rounded Mixed-Radix Fused-Multiply-Add”, 2018 IEEE 25th 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”, 18th international symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2018), 18th international symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2018), Book of Abstracts, Tokyo, Japan, pp. 54-55 (2018)
- 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)
- S. Graillat, C. Jeangoudoux, Ch. Lauter : “A Decimal Multiple-Precision Interval Arithmetic Library”, book of abstracts : 17th International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics., Uppsala, Sweden (2016)