Rewriting Logic Semantics of a Plan Execution Language

Abstract

The 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 two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.

El lenguaje de intercambio de ejecución de planes (PLEXIL) es un lenguaje sincrónico desarrollado por la NASA para respaldar las operaciones de naves espaciales autónomas. En este artículo, proponemos una reescritura de la semántica lógica de PLEXIL en Maude, un motor lógico de alto rendimiento. La semántica de reescritura lógica es por sí misma un intérprete formal del lenguaje y puede ser utilizada como referencia semántica para la implementación de ejecutivos de PLEXIL. La implementación en Maude tiene el beneficio adicional de poner a disposición de los diseñadores y desarrolladores de PLEXIL todas las herramientas formales de análisis y verificación proporcionadas por Maude. La formalización de la semántica de PLEXIL en la reescritura lógica plantea un interesante desafío debido a la naturaleza sincrónica del lenguaje y las reglas priorizadas que definen su semántica. Para superar esta dificultad, proponemos un procedimiento general para simular relaciones de conjuntos síncronos en la reescritura de la lógica que es sólida y, para las relaciones deterministas, completa. También informamos sobre dos problemas a nivel de diseño de la semántica PLEXIL original que se identificaron con la ayuda de la especificación ejecutable en Maude.