@gnouf @nlejeune
###### tags: `TAS`

# Résumé article "Interval Slopes as Numerical Abstract Domain for Floating-Point Variables"

https://hal.archives-ouvertes.fr/hal-00469007v4/document

NARDIN Théo
LEJEUNE Nicolas

## Cadre de recherche
$\hspace{0.5cm}$Le développement de systèmes embarqués nescessitent l'utilisation du concept de *Model-Based design*, c'est à dire le fait de répliquer le comportement réel d'un modèle. Pour répéter la réalité au plus proche, le système a besoin d'une précision chirurgicale, chose qui ne lui est pas apportée par le fonctionnement classique des nombres flottants.

La représentation en binaire des nombres à virgules est effectuée en suivant la norme IEEE-754-2008 qui est la plus répandue. Elle définit ces derniers comme suit:
$f = s.m.2^e$ avec $s$ représentant le signe, $m$ la mantisse et $e$ l'exposant de la virgule du nombre $f$ appartenant à l'intervalle $[e_{min}, e_{max}]$.

Par exemple en suivant la norme IEEE-754-2008 si l'ont fait le calcul suivant : $0.0007 + (−0.0097) + 0.0738 + (−0.3122) + 0.7102 + (−0.5709) + (−1.0953) + \\ 3.3002 + (−2.9619) + (−0.2353) + 2.4214 + (−1.7331) + 0.4121$
On obtient la valeur $-2.08616257.10^{-6}$ alors que si l'ont le fait à la main on obtient $0$. Cette différence importante s'explique par l'accumulation d'erreurs d'arrondis causées par la réprésentation des nombres flottants.
Les problèmes de précisions peuvent aussi provenir de deux autre biais :
* **L'absorption :** Ce phénomène s'observe lorsqu'on cherche à additionner ou soustraire un nombre relativement petit à un nombre relativement grand.
* **L'annulation :** Ce phénomène s'observe lors de la soustraction de deux nombres flottants très proches et qu'un grand nombre de leurs bits significatifs s'annulent.

Ces erreurs sur les flottants peuvent éivdemment causer d'importants problèmes en rendant les mesures d'un environnement physique fausses ou en donnant des résultats approximatifs voir totalement erronés.

Le problème est que les intervalles de valeurs classiques utilisés par les analyseurs statiques ne détectent pas les erreurs précédement citées sur les nombres flottants du fait que ces intervalles sont souvent trop ressérés.

L'objectif de la méthode décrite dans l'article va être d'utiliser l'analyse statique pour valider le design du matériel embarqué décrit en Mathlab/Simulink.

## Proposition

$\hspace{0.5cm}$Dans l'objectif de réduire la sur-approximation dans les intervalles des nombres flottants, l'auteur de l'article s'appuie sur un élargissement d'intervalle, réalisé à l'origine pour les nombres réels par les chercheurs Krawczyk et Neumaier, en utilisant la notion des pentes arithmétiques.

Soient $\vec{X}$ un vecteur d'intervalles et $f: \mathbb{R}^n \to \mathbb{R}$ une fonction non-linéaire composée seulement d'additions, soustractions, multiplications, divisions et racines carrées.
La méthode d'élargissement réduit l'approximation de $f'$ et est définie comme suit (inspiré du *Mean Value Theorem*):
$$
f(\vec{X}) \subseteq f(\vec{z}) + [F^{\vec{z}}](\vec{X})(\vec{X} - \vec{z}) \forall \vec{z} \in \vec{X}
$$
avec
$$
F^{\vec{z}}(\vec{X}) =
\Bigg\{ \frac{f(\vec{x}) - f(\vec{z})}{\vec{x} - \vec{z}}: \vec{x} \in \vec{X} \wedge \vec{z} \neq \vec{x} \Bigg\}
$$

L'utilisation de cette forme permet donc, en réduisant l'approximation de la dérivée, d'obtenir un intervalle d'approximation plus précis.

Néanmoins pour utiliser cet intervalle, il est nescessaire de prendre en compte les fonctions d'arrondis et surtout les erreurs d'arrondis pour imiter au mieux le comportement de l'arithmétique sur les nombres flottants, pour cela l'auteur est obligé de l'adapter.

Au travers de sa *proposition n°1* l'auteur va prouver que le résultat d'une opération sur des nombres à virgules flottantes peut être sur-approximée en effectuant la même opération sur l'intervalle des pentes arithmétiques et en faisant varier un peu ce résultat en fonction de $\mu$ et $\sigma$ qui sont respectivement : l'erreur d'arrondis relative et l'erreur absolue.

L'un des intérêts d'utiliser $\mu$ et $\sigma$ est qu'il est possible de faire varier le comportement des nombres à virgules flottantes en fonction des composants physiques de la machine.

Un ensemble de valeurs à virgules flottantes peut, selon cette proposition, être représenté comme suit :
$$
([f](\vec{z})+(1+[-\mu,\mu])+[-\frac{\sigma}{2}, \frac{\sigma}{2}], [F^{\vec{z}}](\vec{X})(1+[-\mu, \mu]))
$$

Le premier ensemble permet de prendre en compte les éventuelles erreurs d'arrondis quant au second il permet de prendre en charge les erreurs relatives.

Toujours dans un soucis de mimétisme l'auteur propose une fonction nommée $\rho$ qui permet d'imiter le comportement d'absorbtion et donc de le prendre en compte lors de l'analyse. Pour ce faire cette fonction va considérer que la pente de la courbe est de 0 et donc empêcher toute influence par les variables sur le calcul des expression arithmétiques, chose qui peut sembler en contradiction car c'est un des principal intêret des pentes arithmétiques. Mais en faisant cela on va en effet reproduire fidélement le comportement de l'absorbtion de l'arithmétique à virgule flottante.

Cette fonction $\rho$ n'est qu'un exemple parmis les nombreuses autres fonctions participant à définir une sémantique abstraite des opérations arithmétiques permettant d'imiter sur l'intervalle des pentes arithmétiques les opérations de l'arithmétique sur les nombres flottants.

## Conclusion
L'auteur a présenté un nouveau domaine dédié aux variables à virgules flottantes qui va imiter le comportement de l'arithmétique des nombres à virgules flottantes. Ce domaine permet donc, en utilisant les pentes arithmétiques, de vérifier la véracité des simulations calculées par Matlab/Simulink.