NTRS - NASA Technical Reports Server

Back to Results
rewriting logic semantics of a plan execution languageThe Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on the finding of two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.
Document ID
Document Type
Technical Memorandum (TM)
Dowek, Gilles
(Ecole Polytechnique France)
Munoz, Cesar A.
(NASA Langley Research Center Hampton, VA, United States)
Rocha, Camilo
(Illinois Univ. Urbana-Champaign, IL, United States)
Date Acquired
August 24, 2013
Publication Date
June 1, 2009
Subject Category
Computer Programming and Software
Report/Patent Number
Funding Number(s)
WBS: WBS 015792.04.01.0423
Distribution Limits
Public Use Permitted.

Available Downloads

NameType 20090025974.pdf STI