Formal Semantics of PLEXIL
The
Plan Execution Interchange Language![*](/images/exlink.gif)
(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
- 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
![[*]](/images/exlink.gif)
identifies links that are outside
the NASA domain