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).
Difesa : 05/21/2019 - 14h - Campus Jussieu 25-26/105 Membri della commissione : 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
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 : “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)