Static Analysis Numerical Algorithms
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 2016
- Accession Number
- AD1008340
Entities
People
- Anca Browne
- David Oglesby
- Devesh Bhatt
- Douglas Smith
- Eric Bush
- Matthew C. Barry
- Steve Hickman