TY - GEN
T1 - Towards an industrial use of FLUCTUAT on safety-critical avionics software
AU - Delmas, David
AU - Goubault, Eric
AU - Putot, Sylvie
AU - Souyris, Jean
AU - Tekkal, Karim
AU - Védrine, Franck
PY - 2009/12/2
Y1 - 2009/12/2
N2 - Most modern safety-critical control programs, such as those embedded in fly-by-wire control systems, perform a lot of floating-point computations. The well-known pitfalls of IEEE 754 arithmetic make stability and accuracy analyses a requirement for this type of software. This need is traditionally addressed through a combination of testing and sophisticated intellectual analyses, but such a process is both costly and error-prone. FLUCTUAT is a static analyzer developed by CEA-LIST for studying the propagation of rounding errors in C programs. After a long time research collaboration with CEA-LIST on this tool, Airbus is now willing to use FLUCTUAT industrially, in order to automate part of the accuracy analyses of some control programs. In this paper, we present the IEEE 754 standard, the FLUCTUAT tool, the types of codes to be analyzed and the analysis methodology, together with code examples and analysis results.
AB - Most modern safety-critical control programs, such as those embedded in fly-by-wire control systems, perform a lot of floating-point computations. The well-known pitfalls of IEEE 754 arithmetic make stability and accuracy analyses a requirement for this type of software. This need is traditionally addressed through a combination of testing and sophisticated intellectual analyses, but such a process is both costly and error-prone. FLUCTUAT is a static analyzer developed by CEA-LIST for studying the propagation of rounding errors in C programs. After a long time research collaboration with CEA-LIST on this tool, Airbus is now willing to use FLUCTUAT industrially, in order to automate part of the accuracy analyses of some control programs. In this paper, we present the IEEE 754 standard, the FLUCTUAT tool, the types of codes to be analyzed and the analysis methodology, together with code examples and analysis results.
UR - https://www.scopus.com/pages/publications/70649100057
U2 - 10.1007/978-3-642-04570-7_6
DO - 10.1007/978-3-642-04570-7_6
M3 - Conference contribution
AN - SCOPUS:70649100057
SN - 3642045693
SN - 9783642045691
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 53
EP - 69
BT - Formal Methods for Industrial Critical Systems - 14th International Workshop, FMICS 2009, Proceedings
T2 - 14th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2009
Y2 - 2 November 2009 through 3 November 2009
ER -