PLEXIL-V

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 develops a PLEXIL Verification Interactive Formal Environment (PLEXIl-V) based on a formal small-step operational semantics of PLEXIL. PLEXIL-V is available under NASA's Open Source Agreement at GitHub.

Formalizations

• Small-step formal semantics of PLEXIL in PVS and Maude: PVS files, Maude files.
• Synchronous Set Relations in Maude.
• PVS library of set relations.
• Serialization procedure in Maude.
• A simple cruise control model written in PLEXIL (plan, script).

Publications

• Camilo Rocha, Héctor Cadavid, César Muñoz, and Radu Siminiceanu, A Formal Interactive Verification Environment for the Plan Execution Interchange Language, Proceedings of 9th International Conference on Integrated Formal Methods (iFM 2012), Lecture Notes in Computer Science, Volume 7321, pp. 343-357, June 2012. BibTeX Reference.
• Gilles Dowek, César Muñoz, and Camilo Rocha, Rewriting Logic Semantics of a Plan Execution Language, Electronic Proceedings in Theoretical Computer Science, Volume 18, 2010. BibTeX Reference.
  A preliminary version appears as Technical Memorandum, NASA/TM-2009-215770, June 2009. BibTeX Reference.
• Camilo Rocha, César Muñoz, and Héctor Cadavid, A Graphical Environment for the Semantic Validation of a Plan Execution Language, Third IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2009), 2009. BibTeX Reference.
• Gilles Dowek, César Muñoz, and Corina Pasareanu, A Small-Step Semantics of PLEXIL, NIA Technical Report, Number 2008-11, 2008. BibTeX Reference.
• Gilles Dowek, César Muñoz, and Corina Pasareanu, A Formal Analysis Framework for PLEXIL, 3rd Workshop on Planning and Plan Execution for Real-World Systems, 2007. BibTeX Reference.

The tag identifies links that are outside the NASA domain