NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • Formal Semantics of PLEXIL

    The Plan Execution Interchange Language* (PLEXIL) is an open source synchronous language developed by NASA to support autonomous spacecraft operations. The formal methods group at NASA Langley, in collaboration with the PLEXIL group at NASA Ames, has developed a formal small-step operational semantics of PLEXIL.

    Formalizations

    Publications

    The tag [*] identifies links that are outside the NASA domain