Interval Slopes as Numerical Abstract Domain for Floating-Point Variables

TL;DR

This paper introduces a new abstract domain based on interval slopes for floating-point variables, enabling precise static analysis of embedded control systems to verify error absence and numerical accuracy.

Contribution

It presents a novel partially relational abstract domain derived from interval slopes, specifically designed for floating-point variables in embedded systems.

Findings

The domain accurately models floating-point behaviors.

It can prove absence of run-time errors.

It aids in analyzing numerical precision.

Abstract

The design of embedded control systems is mainly done with model-based tools such as Matlab/Simulink. Numerical simulation is the central technique of development and verification of such tools. Floating-point arithmetic, that is well-known to only provide approximated results, is omnipresent in this activity. In order to validate the behaviors of numerical simulations using abstract interpretation-based static analysis, we present, theoretically and with experiments, a new partially relational abstract domain dedicated to floating-point variables. It comes from interval expansion of non-linear functions using slopes and it is able to mimic all the behaviors of the floating-point arithmetic. Hence it is adapted to prove the absence of run-time errors or to analyze the numerical precision of embedded control systems.