Static Analysis Numerical Algorithms
Technical Report,01 Nov 2013,01 Nov 2015
KESTREL TECHNOLOGY, LLC Palo Alto
Pagination or Media Count:
This document reports on a two-year research project by Kestrel Technology and Honeywell Aerospace Advanced Technology 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. We concentrated on two classes of numerical algorithms, linear digital filters and integrating accumulators, modifying existing versions of Honeywells HiLiTE model-based development system and Kestrels 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. These static analysis results were then fed back into HiLiTE to be further exploited in the formal verification of the generated code.