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.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Adding Assurance to Automatically Generated Code


    Contributors:

    Conference:

    High Assurance Systems Engineering 2 ; 2004 ; Tampa, FL, United States


    Publication date :

    2004-01-01


    Type of media :

    Preprint


    Type of material :

    No indication


    Language :

    English




    Verifying Code Automatically Generated From an Executable Model

    Williams, Cheryl A. / Kropinski, Michael A. / Steele, Michael A. et al. | SAE Technical Papers | 2005


    Verifying code automatically generated from an executable model

    Williams,C.A. / Kropinski,M.A. / Matthews,O. et al. | Automotive engineering | 2005


    Building Heterogeneous Safety Cases for Automatically Generated Code

    Denney, E. / Basir, N. / Fischer, B. et al. | British Library Conference Proceedings | 2011


    Building Heterogeneous Safety Cases for Automatically Generated Code

    Denney, Ewen / Fischer, Bernd / Basir, Nurlida | AIAA | 2011


    2005-01-1665 Verifying Code Automatically Generated From an Executable Model

    Williams, C. A. / Kropinski, M. A. / Matthews, O. et al. | British Library Conference Proceedings | 2005