TY - GEN
T1 - Static analysis of the accuracy in control systems
T2 - 12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007
AU - Goubault, Eric
AU - Putot, Sylvie
AU - Baufreton, Philippe
AU - Gassino, Jean
PY - 2008/6/9
Y1 - 2008/6/9
N2 - Finite precision computations can severely affect the accuracy of computed solutions. We present a complete survey of a static analysis based on abstract interpretation, and a prototype implementing this analysis for C code, for studying the propagation of rounding errors occurring at every intermediary step in floating-point computations. In the first part of this paper, we briefly present the domains and techniques used in the implemented analyzer, called FLUCTUAT. We describe in the second part, the experiments made on real industrial codes, at Institut de Radioprotection et de Sûreté Nucléaire and at Hispano-Suiza, respectively coming from the nuclear industry and from aeronautics industry. This paper aims at filling in the gaps between some theoretical aspects of the static analysis of floating-point computations that have been described in [13,14,21], and the necessary choices of algorithms and implementation, in accordance with practical motivations drawn from real industrial cases.
AB - Finite precision computations can severely affect the accuracy of computed solutions. We present a complete survey of a static analysis based on abstract interpretation, and a prototype implementing this analysis for C code, for studying the propagation of rounding errors occurring at every intermediary step in floating-point computations. In the first part of this paper, we briefly present the domains and techniques used in the implemented analyzer, called FLUCTUAT. We describe in the second part, the experiments made on real industrial codes, at Institut de Radioprotection et de Sûreté Nucléaire and at Hispano-Suiza, respectively coming from the nuclear industry and from aeronautics industry. This paper aims at filling in the gaps between some theoretical aspects of the static analysis of floating-point computations that have been described in [13,14,21], and the necessary choices of algorithms and implementation, in accordance with practical motivations drawn from real industrial cases.
KW - Control systems
KW - Floating-point computations
KW - Static analysis
U2 - 10.1007/978-3-540-79707-4_3
DO - 10.1007/978-3-540-79707-4_3
M3 - Conference contribution
AN - SCOPUS:44649123787
SN - 3540797068
SN - 9783540797067
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 20
BT - Formal Methods for Industrial Critical Systems - 12th International Workshop, FMICS 2007, Revised Selected Papers
Y2 - 1 July 2007 through 2 July 2007
ER -