Publication:
Rewriting Logic Semantics of a Plan Execution Language

Thumbnail Image
Files

Files

Rewriting Logic Semantics of a Plan Execution Language ∗.pdf (274.11 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Dowek, Gilles
Muñoz, César
Rocha, Camilo
Abstract (Spanish)
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.
Abstract (English)
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.
Extent
15 páginas.
Rights

c G. Dowek & C. Munoz & C. Rocha

URI: https://repositorio.escuelaing.edu.co/handle/001/1902
Collections

Collections

AD - CTG – Informática
References

M. AlTurki & J. Meseguer (2008): Reduction Semantics and Formal Analysis of Orc Programs. Electr. Notes Theor. Comput. Sci. 200(3), pp. 25–41.

G. Berry (2000): The Foundations of Esterel. In: Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge, MA, USA, pp. 425–454.

R. Bruni & J. Meseguer (2006): Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1-3), pp. 386–414. Available at http://dx.doi.org/10.1016/j.tcs.2006.04.012.

P. Caspi, D. Pilaud, N. Halbwachs & J. A. Plaice (1987): LUSTRE: a declarative language for real-time programming. In: POPL ’87: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM, New York, NY, USA, pp. 178–188.

M. Clavel, F. Duran, S. Eker, J. Meseguer, P. Lincoln, N. Mart ´ ´ı-Oliet & C. Talcott (2007): All About Maude - A High-Performance Logical Framework. Springer LNCS Vol. 4350, 1st edition.

N. Dershowitz & J. P. Jouannaud (1990): Rewrite Systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). The MIT Press, pp. 243–320.

G. Dowek, C. Munoz & C. P ˜ as˘ areanu (2007): ˘ A Formal Analysis Framework for PLEXIL. In: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems. pp. 45–51.

G. Dowek, C. Munoz & C. P ˜ as˘ areanu (2008): ˘ A Small-Step Semantics OF PLEXIL. Technical Report 2008- 11, National Institute of Aerospace, Hampton, VA.

T. Estlin, A. Jonsson, C. P ´ as˘ areanu, R. Simmons, K. Tso & V. Verna (2006): ˘ Plan Execution Interchange Language (PLEXIL). Technical Memorandum TM-2006-213483, NASA.

D. Lucanu (2009): Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions. Electr. Notes Theor. Comput. Sci. 237, pp. 107–125.

J. Meseguer (1992): Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96(1), pp. 73–155.

J. Meseguer & G. Rosu (2007): The rewriting logic semantics project. Theor. Comput. Sci. 373(3), pp. 213–237. Available at http://dx.doi.org/10.1016/j.tcs.2006.12.018.

S. Owre, J. Rushby & N. Shankar (1992): PVS: A Prototype Verification System. In: Deepak Kapur, editor: 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence 607. Springer-Verlag, Saratoga, NY, pp. 748–752.

G. D. Plotkin (2004): A structural approach to operational semantics. J. Log. Alg. Prog. 60-61, pp. 17–139.

C. Rocha, C. Munoz & H. Cadavid (2009): ˜ A Graphical Environment for the Semantic Validation of a Plan Execution Language. IEEE International Conference on Space Mission Challenges for Information Technology 0, pp. 201–207.

T. Serbanuta, G. Rosu & J. Meseguer (2009): A rewriting logic approach to operational semantics. Inf. Comput. 207(2), pp. 305–340.

T. Serbanuta, G. Stefanescu & G. Rosu (2008): Defining and Executing P Systems with Structured Data in K. In: David W. Corne, Pierluigi Frisco, Gheorghe Paun, Grzegorz Rozenberg & Arto Salomaa, editors: Workshop on Membrane Computing, Lecture Notes in Computer Science 5391. Springer, pp. 374–393.

O. Tardieu (2007): A deterministic logical semantics for pure Esterel. ACM Trans. Program. Lang. Syst. 29(2), p. 8.

A. Verdejo & N. Mart´ı-Oliet (2006): Executable structural operational semantics in Maude. J. Log. Algebr. Program. 67(1-2), pp. 226–293.

V. Verna, A. Jonsson, C. P ´ as˘ areanu & M. Latauro (2006): ˘ Universal Executive and PLEXIL: Engine and Language for Robust Spacecraft Control and Operations. In: Proceedings of the American Institute of Aeronautics and Astronautics Space Conference.

P. Viry (2002): Equational rules for rewriting logic. Theoretical Computer Science 285, pp. 487–517.