Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software

Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software
复制标题

FLUCTUAT 在安全关键型航空电子软件上的工业应用

DOI:
--
复制
发表时间:
2009
期刊:
International Workshop on Formal Methods for Industrial Critical Systems
影响因子:
--
通讯作者:
Franck Védrine
Franck Védrine
中科院分区:
--
文献类型:
--
作者:
David Delmas;É. Goubault;S. Putot;J. Souyris;Karim Tekkal;Franck Védrine

文献摘要

被引文献

相似文献

大多数现代的安全关键控制程序,如嵌入在电传操纵系统中的程序,执行大量的浮点计算。IEEE 754算法的众所周知的缺陷使得稳定性和准确性分析成为这类软件的要求。这种需求传统上是通过测试和复杂的智力分析相结合来解决的,但这样的过程既昂贵又容易出错。FLUCTUAT是CEA-LIST开发的静态分析器,用于研究C程序中舍入错误的传播。在与CEA-LIST就该工具进行了长期的研究合作之后,空客现在愿意在工业上使用FLUCTUAT,以自动化某些控制程序的部分精度分析。在本文中,我们提出了IEEE 754标准,FLUCTUAT工具,代码的类型进行分析和分析方法,连同代码的例子和分析结果。
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.