Fluctuat
 | This article may be too technical for most readers to understand. (January 2013) |
| Developer(s) | Commissariat à l'Énergie Atomique |
|---|---|
| Written in | C |
| Operating system | |
| Available in | English |
| Type | Formal verification, Static code analysis |
| License | Commercial |
| Website | www |
Fluctuat has been developed by Commissariat à l'Énergie Atomique et aux Énergies Alternatives since 2001. Fluctuat enables the static analysis of C and Ada programs, with a special focus on floating-point operations.
Theoretical background
[edit]Fluctuat is a static analyser, based on abstract interpretation. Compared to similar tools like Polyspace or Astrée, it relies on zonotopes as an abstract domain. It means that the value of each program variable is abstracted by a linear expression over noise symbols (internal variables that range in [-1,1]).
Let us now consider the following program:
x=[0,1]; y = 2*x 1; z = x * y;
The first line means that the value of x can be anything in [0,1]. It can be written as x= 0.5 0.5*ε, where ε is a noise symbol. The second line implies that y= 2 ε; since x and y share the same noise symbol, this abstract domain is relational. When there are non-linear operations, like in the third line, new noise symbols are introduced. The accurate symbolic expression would be z=1 1.5*ε 0.5*ε*ε, but we abstract it as z=1.25 1.5ε 0.25η.
Features
[edit]Fluctuat's features include:
- static analysis of C and Ada programs.[1]
- sensitivity analysis of program variables.[2]
- worst-case generation.
- interactive analysis.
- analysis of hybrid systems[3]
See also
[edit]References
[edit]- ^ David Delmas; et al. "Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software". Proceedings of 14th International Workshop on Formal Methods for Industrial Critical Systems FMICS'09. LNCS. Vol. 5825. pp. 53–69.
- ^ Eric Goubault and Sylvie Putot. "Static Analysis of Numerical Algorithms". Proceedings of Static Analysis Symposium SAS'06, Seoul. LNCS. Vol. 4134. pp. 18–34.
- ^ Olivier Bouissou; et al. "HybridFluctuat: a static analyzer of numerical programs within a continuous environment". Proceedings of Computer Aided Verification CAV'09, Grenoble, France. LNCS. Vol. 5649. pp. 620–626. CiteSeerX 10.1.1.216.8351.