The Constellation project at NASA calls for designing a Crew Exploration Vehicle (Orion, also called CEV) and Cargo Launch Vehicle (Ares, also called CLV). Both projects will rely on newly designed flight control software. The verification of these C++ flight codes is critical, especially for Orion, since human life will be at stake. There exist some commercial tools for the verification of C++ code. However, none of the commercially available tools does a good job a finding bugs dealing with concurrency. Yet both software for Orion and Ares are expected to be multi-threaded. With this work we are proposing to address the issue by developing a suite of tools that can be used to verify C++ code. Our tools will range from a static analyzer (based on abstract interpretation like C Global Surveyor) to a model checker (MCP, which we present in this paper) including a symbolic execution engine for test case generation (TPGEN). This paper focuses on MCP and its application to Aerospace software.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Verification of C++ Flight Software with the MCP Model Checker


    Beteiligte:
    Thompson, S. (Autor:in) / Brat, G. (Autor:in)


    Erscheinungsdatum :

    2008-03-01


    Format / Umfang :

    306000 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    A Model-Based Approach to Verification of Spacecraft Software Using the SPIN Model Checker

    Horvath, G. / Jones, G. / Joshi, R. et al. | British Library Conference Proceedings | 2009


    A Model-Based Approach to Verification of Spacecraft Software Using the SPIN Model Checker

    Horvath, Gregory / Jones, Grailing / Joshi, Rajeev | AIAA | 2009


    Software Library Usage Pattern Extraction Using a Software Model Checker

    Liu, C. / Ye, E. / Richardson, D.J. | British Library Online Contents | 2009



    CHECKER

    YOSHINO MITSUNORI / KITANO TETSUJI | Europäisches Patentamt | 2019

    Freier Zugriff