Formal Semantics of PLEXIL
The Plan Execution Interchange Language
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.
- Camilo Rocha, Héctor Cadavid, César Muñoz,
and Radu Siminiceanu,
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
Third IEEE International Conference on Space Mission Challenges
for Information Technology (SMC-IT 2009), 2009.
- Gilles Dowek, César Muñoz, and Corina Pasareanu, A
Semantics of PLEXIL, NIA Technical Report, Number 2008-11, 2008.
- 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.
identifies links that are outside
the NASA domain