Automatic Certification of Kalman Filters for Reliable Code Generation

Author

Denney, Ewen ; Fischer, Bernd ; Schumann, Johann ; Richardson, Julian

Author_Institution

USRA/RIACS, NASA Ames Res. Center, Moffett Field, CA

fYear

2005

fDate

5-12 March 2005

Firstpage

1

Lastpage

10

Abstract

AUTOFILTER is a tool for automatically deriving Kalman filter code from high-level declarative specifications of state estimation problems. It can generate code with a range of algorithmic characteristics and for several target platforms. The tool has been designed with reliability of the generated code in mind and is able to automatically certify that the code it generates is free from various error classes. Since documentation is an important part of software assurance, AUTOFILTER can also automatically generate various human-readable documents, containing both design and safety related information. We discuss how these features address software assurance standards such as DO-17SB

Keywords

Kalman filters; aerospace computing; formal specification; program compilers; software standards; AUTOFILTER; DO-17SB; Kalman filters; automatic certification; code generation; high-level declarative specifications; human-readable documents; software assurance standards; state estimation problems; Application software; Certification; FAA; Gold; Mathematics; NASA; Software safety; Software tools; Space vehicles; State estimation;

fLanguage

English

Publisher

ieee

Conference_Titel

Aerospace Conference, 2005 IEEE

Conference_Location

Big Sky, MT

Print_ISBN

0-7803-8870-4

Type

conf

DOI

10.1109/AERO.2005.1559605

Filename

1559605