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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Adding Assurance to Automatically Generated Code


    Beteiligte:
    Denney, Ewen (Autor:in) / Fischer, Bernd (Autor:in) / Schumann, Johann (Autor:in)

    Kongress:

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


    Erscheinungsdatum :

    01.01.2004


    Medientyp :

    Preprint


    Format :

    Keine Angabe


    Sprache :

    Englisch


    Schlagwörter :


    Verifying Code Automatically Generated From an Executable Model

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


    Building Heterogeneous Safety Cases for Automatically Generated Code

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


    Verifying code automatically generated from an executable model

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


    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