Buscar
Mostrando ítems 1-7 de 7
A Formal Interactive Verification Environment for the Plan Execution Interchange Language
(Springer Nature, 2012)
The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive ...
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
(Springer, 2010)
Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite ...
Simulation and Verification of Synchronous Set Relations in Rewriting Logic
(NASA Langley Research Center, 2011)
This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of
synchronous set relations. The mathematical foundation is given in the
language of abstract ...
A formal library of set relations and its application to synchronous languages
(Elsevier B.V., 2011)
Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and ...
Tool Interoperability in the Maude Formal Environment
(Springer, 2011)
We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the ...
Rewriting Logic Semantics of a Plan Execution Language
(2010)
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 ...
A Graphical Environment for the Semantic Validation of a Plan Execution Language
(© Copyright 2021 IEEE, 2009)
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 ...