The paper documents an application of the finite state model checker SPIN to formally analyze a multithreaded plan execution module. The plan execution module is one component of NASA's New Millennium Remote Agent, an artificial intelligence-based spacecraft control system architecture which launched in October of 1998 as part of the DEEP SPACE 1 mission. The bottom layer of the plan execution module architecture is a domain specific language, named ESL (Executive Support Language), implemented as an extension to multithreaded COMMON LISP. ESL supports the construction of reactive control mechanisms for autonomous robots and spacecraft. For the case study, we translated the ESL services for managing interacting parallel goal-and-event driven processes into the PROMELA input language of SPIN. A total of five previously undiscovered concurrency errors were identified within the implementation of ESL. According to the Remote Agent programming team, the effort has had a major impact, locating errors that would not have been located otherwise and, in one case, identifying a major design flaw. In fact, in a different part of the system, a concurrency bug identical to one discovered by this study escaped testing and caused a deadlock during an in-flight experiment, 96 million kilometers from Earth. The work additionally motivated the introduction of procedural abstraction in terms of inline procedures into SPIN.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal analysis of a space-craft controller using SPIN


    Beteiligte:
    Havelund, K. (Autor:in) / Lowry, m. (Autor:in) / Penix, J. (Autor:in)

    Erschienen in:

    Erscheinungsdatum :

    2001


    Format / Umfang :

    17 Seiten, 12 Quellen




    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Print


    Sprache :

    Englisch




    Formal Safety Assessment and High Speed Craft

    Peachey, J. / Royal Institute of Naval Architects | British Library Conference Proceedings | 1997


    Craft and method for assembling craft with controlled spin

    BABINSKY HOLGER / MCINTOSH SIMON / WHITCHER LEE et al. | Europäisches Patentamt | 2015

    Freier Zugriff

    CRAFT AND METHOD FOR ASSEMBLING CRAFT WITH CONTROLLED SPIN

    WHITCHER LEE / POTTER STEVE / BABINSKY HOLGER et al. | Europäisches Patentamt | 2018

    Freier Zugriff

    MULTIFUNCTIONAL SPACE CRAFT

    POLUYAN ALEKSANDR PETROVICH / KUZNETSOV VLADIMIR ALEKSANDROVICH | Europäisches Patentamt | 2017

    Freier Zugriff

    Spacesuit: space craft

    Pitts, Bradley McGilvary, 1978- | DSpace@MIT | 2003

    Freier Zugriff