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

Author

Rocha, Camilo ; Munoz, Cesar ; Cadavid, Héctor

Author_Institution

Dept. of Comput. Sci., Univ. of Illinois at Urbana-Champaign, Urbana, IL, USA

fYear

2009

fDate

19-23 July 2009

Firstpage

201

Lastpage

207

Abstract

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.

Keywords

high level languages; program verification; rewriting systems; user interfaces; PLEXIL; formal interacting visual environment; formal operational semantics; graphical environment; semantic validation; synchronous plan execution language; user-friendly interface; Computer science; Concurrent computing; Information technology; Java; Logic; NASA; Space missions; Space vehicles; System testing; USA Councils; Formal Semantics; PLEXIL; Rewriting Logic; Visual Validation Environment;

fLanguage

English

Publisher

ieee

Conference_Titel

Space Mission Challenges for Information Technology, 2009. SMC-IT 2009. Third IEEE International Conference on

Conference_Location

Pasadena, CA

Print_ISBN

978-0-7695-3637-8

Type

conf

DOI

10.1109/SMC-IT.2009.31

Filename

5226831