Model-based design and automated code generation are increasingly used at NASA to produce actual flight code, particularly in the Guidance, Navigation, and Control domain. However, since code generators are typically not qualified, there is no guarantee that their output is correct, and consequently auto-generated code still needs to be fully tested and certified. We have thus developed AutoCert, a generator-independent plug-in that supports the certification of auto-generated code. AutoCert takes a set of mission safety requirements, and formally verifies that the auto-generated code satisfies these requirements. It generates a natural language report that explains why and how the code complies with the specified requirements. The report is hyper-linked to both the program and the verification conditions and thus provides a high-level structured argument containing tracing information for use in code reviews.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Generating Code Review Documentation for Auto-Generated Mission-Critical Software


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


    Erscheinungsdatum :

    2009-07-01


    Format / Umfang :

    1660154 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Standards for mission operations documentation

    Bender, H.J. / Gries, A. | Tema Archiv | 1991