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

• 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