Code to estimate position and attitude of a spacecraft or aircraft belongs to the most safety-critical parts of flight software. The complex underlying mathematics and abundance of design details make it error-prone and reliable implementations costly. AutoFilter is a program synthesis tool for the automatic generation of state estimation code from compact specifications. It can automatically produce additional safety certificates which formally guarantee that each generated program individually satisfies a set of important safety policies. These safety policies (e.g.. array-bounds, variable initialization) form a core of properties which are essential for high-assurance software. Here we describe the AutoFilter system and its certificate generator and compare our approach to the static analysis tool PolySpace.
Adding Assurance to Automatically Generated Code
High Assurance Systems Engineering 2 ; 2004 ; Tampa, FL, United States
2004-01-01
Preprint
No indication
English
Verifying Code Automatically Generated From an Executable Model
SAE Technical Papers | 2005
|Verifying code automatically generated from an executable model
Automotive engineering | 2005
|Building Heterogeneous Safety Cases for Automatically Generated Code
British Library Conference Proceedings | 2011
|2005-01-1665 Verifying Code Automatically Generated From an Executable Model
British Library Conference Proceedings | 2005
|