Method to Detect Floating-Point Absorption and Cancellation Phenomena in Software-Critical Design Models

摘要

Airborne critical systems that use real numbers in their algorithms can be considerably affected by the floating-point discretized representation. This limitation in the representation is the cause of many problems already known while running software with floating-point variables such as loss of precision in arithmetic operations. This work presents a method for detecting floating-point absorption and cancellation phenomena using static analysis in software design models. Our method uses a range analysis tool that operates over SCADE model to propagate the range of the internal variables and, then, each addition and subtraction operation in the model is analyzed to check the occurrence of the floating-point absorption and cancellation phenomena. The results are presented in an HTML report containing absorption alerts and cancellations charts providing the number of canceled bits for each sub-range in order to permit better assessment of the impact of each detected cancellation. In order to validate the proposed method, we compare the results of our proposed method with the results obtained by an alternative validation method developed using the source code as input and the Frama-C EVA to propagate internal ranges. The method can be used as an early design analysis enabling the cheaper detection and treatment of floating-point anomalies.