Publication:
A Graphical Environment for the Semantic Validation of a Plan Execution Language

Thumbnail Image
Files

Files

A Graphical Environment for the Semantic Validation of a Plan Execution Language.pdf (693.71 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Rocha, Camilo
Muñoz, Cesar
Cadavid, Hector
Abstract (Spanish)
Este documento presenta PLEXIL5, el entorno visual interactivo formal de PLEXIL, un entorno gráfico que proporciona una interfaz fácil de usar para la semántica operativa formal de PLEXIL. PLEXIL es un lenguaje de ejecución de planes sincrónicos desarrollado por la NASA para respaldar las operaciones espaciales autónomas. PLEXIL5 sirve como banco de pruebas para diseñadores, desarrolladores y usuarios del sistema ejecutivo de PLEXIL para validar, mantener y depurar la implementación del sistema contra la semántica formal del lenguaje. La semántica formal ejecutable de PLEXIL es una teoría lógica de reescritura ejecutable en el lenguaje de Maude.
Abstract (English)
This paper presents PLEXIL5, PLEXIL's formal interacting visual environment, a graphical environment providing an user-friendly interface to the formal operational semantics of PLEXIL. PLEXIL is a synchronous plan execution language developed by NASA to support autonomous space operations. PLEXIL5 serves as a testbed for designers, developers and users of PLEXIL's executive system to validate, maintain, and debug the implementation of the system against the formal semantics of the language. The executable formal semantics of PLEXIL is an executable rewriting logic theory in Maude's language.
Extent
7 páginas.
Rights

© Copyright 2021 IEEE

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

Collections

AD - CTG – Informática
References

V. Verma A. Jonsson C. S. Pasareanu and M. Iatauro "Universal executive and PLEXIL: Engine and language for robust spacecraft control and operations" American Institute of Aeronautics and Astronautics Space 2006 Conference 2006.

G. Berry "The foundations of Esterel" Proof Language and Interaction: Essays in Honour of Robin Milner 2000.

P. Caspi D. Pilaud N. Halbwachs and J. Plaice "Lustre: A declarative language for programming synchronous systems" Proceedings of the 14th Symposium on Principles of Programming Languages (POPL) 1987.

P. L. Guernic T. Gautier M. L. Borgne and C. L. M. e. "Programming real-time applications with SIGNAL" Proceedings of the IEEE vol. 79 no. 9 pp. 1321-1336 1991.

G. Dowek C. Munoz and C. Pasareanu A small-step semantics of PLEXIL 2008.

G. Dowek C. Munoz and C. Pasareanu "A formal analysis framework for PLEXIL" Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems September 2007.

S. Owre J. Rushby and N. Shankar "PVS: A prototype verification system" 11th International Conference on Automated Deduction (CADE) ser. Lecture Notes in Artificial Intelligence vol. 607 pp. 748-752 Jun. 1992.

"All About Maude - A High-Performance Logical Framework How to Specify Program and Verify Systems in Rewriting Logic" in Lecture Notes in Computer Science Springer vol. 4350 2007.

J. Meseguer "Conditional rewriting logic as a unified model of concurrency" Theoretical Computer Science vol. 96 no. 1 pp. 73-155 1992.

T.-F. Serbanuta G. Rosu and J. Meseguer "A rewriting logic approach to operational semantics" Inf Comput. vol. 207 no. 2 pp. 305-340 2009.

F. Buschmann R. Meunier H. Rohnert P. Sornmerlad and M. Stal Pattern-Oriented Software Architecture Wiley vol. 1 1996.

M. Fowler Patterns of Enterprise Application Architecture Reading Massachusetts:Addison Wesley Nov. 2002.

A. K. Bhattacharjee S. D. Dhodapkar S. A. Seshia and R. K. Shyama-sundar "A graphical environment for the specification and verification of reactive systems" in SAFECOMP ser. Lecture Notes in Computer Science Springer vol. 1698 pp. 431-444 1999.

S. Ramesh and P. Sampath SCADE: Synchronous Design and Validation of Embedded Control Software Springer Netherlands 2007.

G. Berry "Synchronous design and verification of critical embedded systems using scade and esterel" in FMICS ser. Lecture Notes in Computer Science Springer vol. 4916 pp. 2 2007.

J. Meseguer and G. Rosu "The rewriting logic semantics project" Theor. Comput. Sci. vol. 373 no. 3 pp. 213-237 2007.