Static Analysis of Numerical Algorithms
The objective of the SANA project was to combine model-based development of complex avionics control software with static analysis of the generated code to achieve assurance levels not available from either technique practiced separately. This was a joint effort by Kestrel Technology and Honeywell Aerospace Advanced Technology. We concentrated on two classes of numerical algorithms, linear digital filters (LDFs) and integrating accumulators, modifying existing versions of Honeywell’s HiLiTE model-based development system and Kestrel Technology’s CodeHawk abstract interpretation system to share domain specific information about implementations of these algorithms. This allowed CodeHawk to exploit model-level specifications and theoretical input bounds from HiLiTE concerning the generated C code, producing a much more precise over-approximation of the output bounds and accumulated floating-point error bounds than would be possible with generic abstract interpretation techniques. The integration then returned these static analysis results to HiLiTE to be further exploited in the formal verification of the generated code.
We made some unexpected discoveries during the first year analysis of LDFs concerning analytic solutions to output and error bounds for filters that changed the architecture of our first year approach, and redefined our focus for the second year effort. In particular, Anca Browne’s discovery of an analytic technique for computing filter bounds obviated the need for the iterative symbolic evaluation of classical abstract interpretation, making the time to analyze a filter negligible. This contrasts with comparable filter analyses performed for Airbus that take on the order of 20 hours to achieve less precise results (please inquire for references). Extending this technique to floating point error analysis, she discovered how to generate a closed-form solution for the error as a function of the number of iterations of the recurrence that are performed. This resulted in CodeHawk’s “error bounds” for filters being reported back to HiLiTE not as an instance-specific numeric interval, as was originally envisioned, but as parameters to a generalized error function, allowing HiLiTE to analyze multiple scenarios with different durations from a single analysis result. When these techniques were generalized to integrating accumulators, our static analyzer was able to report both output and error ranges as parameters to a generalized function.
We built specialized versions of both HiLiTE and CodeHawk to exploit the shared model-level information and exchange their results. We were able to precisely analyze a wide range of first-order and second-order LDF’s for both their range and error bounds. Integrating accumulators are a class of numerical algorithm that arise in avionic digital control. One such integrating accumulator was eventually implicated as the source of a floating-point error design flaw in the Patriot Missile avionics software that failed to track an incoming Iraqi Scud missile, allowing it hit the American barracks in Al Khobar near Dhahran, Saudi Arabia, in 1991 (killing 28 Americans). Using design models and source code we demonstrated that our combined analysis tools would have discovered the error at design and implementation time, precluding its deployment into operations.