This paper describes an approach to assuring the reliability of autonomous systems for Astronaut-Rover (ASRO) teams using the formal verification of models in the Brahms multi-agent modelling language. Planetary surface rovers have proven essential to several manned and unmanned missions to the moon and Mars. The first rovers were teleor manually-operated, but autonomous systems are increasingly being used to increase the effectiveness and range of rover operations on missions such as the NASA Mars Science Laboratory. It is anticipated that future manned missions to the moon and Mars will use autonomous rovers to assist astronauts during extravehicular activity (EVA), including science, technical and construction operations. These ASRO teams have the potential to significantly increase the safety and efficiency of surface operations. We describe a new Brahms model in which an autonomous rover may perform several different activities including assisting an astronaut during EVA. These activities compete for the autonomous rover's “attention” and therefore the rover must decide which activity is currently the most important and engage in that activity. The Brahms model also includes an astronaut agent, which models an astronaut's predicted behaviour during an EVA. The rover must also respond to the astronauts activities. We show how this Brahms model can be simulated using the Brahms integrated development environment. The model can then also be formally verified with respect to system requirements using the SPIN model checker, through automatic translation from Brahms to PROMELA (the input language for SPIN). We show that such formal verification can be used to determine that mission- and safety-critical operations are conducted correctly, and therefore increase the reliability of autonomous systems for planetary rovers in ASRO teams.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Astronaut-Rover Teams for Planetary Surface Operations


    Beteiligte:
    Webster, Matt (Autor:in) / Dennis, Louise A. (Autor:in) / Dixon, Clare (Autor:in) / Fisher, Michael (Autor:in) / Stocker, Richard (Autor:in) / Sierhuis, Maarten (Autor:in)


    Erscheinungsdatum :

    2020-03-01


    Format / Umfang :

    1552549 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    First Astronaut- Rover Interaction Field Test

    Kosmo, Joseph J. / Ross, Amy / Cabrol, Nathalie A. | NTRS | 2000


    First Astronaut - Rover Interaction Field Test

    Ross, Amy / Kosmo, Joseph J. / Cabrol, Nathalie A. et al. | SAE Technical Papers | 2000


    Astronaut Operations

    Chamitoff, Gregory E. / Reagan, Marcum / Peterson, Tyler | AIAA | 2021


    Increased autonomy for planetary rover operations

    Hoffman, Brian D., 1975- | DSpace@MIT | 1998

    Freier Zugriff

    Planetary rover

    LIU FEI / HE CHUNQIAO / LIANG PENG et al. | Europäisches Patentamt | 2015

    Freier Zugriff