A Flight Rule Checker for the LADEE Lunar Spacecraft

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.