As part of the design of a space mission, an important part is the design of so-called flight rules. Flight rules express constraints on various parts and processes of the mission, that if followed, will reduce the risk of failure. One such set of flight rules constrain the format of command sequences regularly (e.g. daily) sent to the spacecraft to con- trol its next near term behavior. We present a high-level view of the automated flight rule checker Frc for checking command sequences sent to NASA’s LADEE Lunar mission spacecraft, used throughout its entire mission. A command sequence is in this case essentially a program (a sequence of commands) with no loops or conditionals, and it can there- fore be verified with a trace analysis tool. Frc is implemented using the TraceContract runtime verification tool, an internal Scala DSL for checking event sequences against “formal specifications”. The paper illustrates this untraditional use of runtime verification in a real con- text, with strong demands on the expressiveness and flexibility of the specification language, illustrating the advantages of an internal DSL.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    A Flight Rule Checker for the LADEE Lunar Spacecraft


    Contributors:

    Publication date :

    2020-11-30


    Type of media :

    Preprint


    Type of material :

    No indication


    Language :

    English



    Flight Rule Checker for the LADEE Lunar Spacecraft

    E. Kurklu / K. Havelund | NTIS | 2020


    A Flight Rule Checker for the LADEE Lunar Spacecraft

    Elif Kurklu / Klaus Havelund | NTRS | 2020


    Lunar Meteoroid Impact Monitoring for LADEE

    R. Suggs / D. Moser | NTIS | 2013


    Lunar Meteoroid Impact Monitoring for LADEE

    Suggs, Rob / Moser, Danielle | NTRS | 2013


    LADEE Flight Software: Verification Techniques

    Gundy-Burlet, Karen | NTRS | 2014