Robustness Analysis of Finite Precision Implementations

Abstract. A desirable property of control systems is to be robust to in-puts, that is small perturbations of the inputs of a system will cause only small perturbations on its outputs. But it is not clear whether this prop-erty is maintained at the implementation level, when two close inputs can lead to very different execution paths. The problem becomes particularly crucial when considering finite precision implementations, where any el-ementary computation can be affected by a small error. In this context, almost every test is potentially unstable, that is, for a given input, the computed (finite precision) path may differ from the ideal (same com-putation in real numbers) path. Still, state-of-the-art error analyses do not consider this possibility and rely on the stable test hypothesis, that control flows are identical. If there is a discontinuity between the treat-ments in the two branches, that is the conditional block is not robust to uncertainties, the error bounds can be unsound. We propose here a new abstract-interpretation based error analysis of fi-nite precision implementations, relying on the analysis of [16] for round-ing error propagation in a given path, but which is now made sound in presence of unstable tests. It automatically bounds the discontinuity error coming from the difference between the float and real values when there is a path divergence, and introduces a new error term labeled by the test that introduced this potential discontinuity. This gives a tractable er-ror analysis, implemented in our static analyzer FLUCTUAT: we present results on representative extracts of control programs.