Synchronous set relations in rewriting logic

Abstract

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 set relations. The infrastructure, which is written in the Maude system, enables the synchronous execution of a set relation provided by the user. By using the infrastructure, algorithm verification techniques such as reachability analysis and model checking, already available in Maude for traditional asynchronous rewriting, are automatically available to synchronous set rewriting. In this way, set-based synchronous languages and systems such as those built from agents, components, or objects can be naturally specified and simulated, and are also amenable to formal verification in the Maude system. The use of the infrastructure and some of its Maude-based verification capabilities are illustrated with an executable operational semantics of the Plan Execution Interchange Language (PLEXIL), a synchronous language developed by NASA to support autonomous spacecraft operations.

Este artículo presenta una base matemática y una infraestructura lógica de reescritura para la ejecución y verificación de propiedades de relaciones de conjuntos sincrónicos. El fundamento matemático se da en el lenguaje de las relaciones abstractas de conjuntos. La infraestructura, que está escrita en el sistema Maude, permite la ejecución sincrónica de una relación establecida proporcionada por el usuario. Mediante el uso de la infraestructura, las técnicas de verificación de algoritmos, como el análisis de accesibilidad y la verificación de modelos, ya disponibles en Maude para la reescritura asincrónica tradicional, están disponibles automáticamente para la reescritura sincrónica de conjuntos. De esta manera, los lenguajes y sistemas sincrónicos basados ​​en conjuntos, como los construidos a partir de agentes, componentes u objetos, pueden especificarse y simularse de forma natural, y también son susceptibles de verificación formal en el sistema Maude. El uso de la infraestructura y algunas de sus capacidades de verificación basadas en Maude se ilustran con una semántica operativa ejecutable del lenguaje de intercambio de ejecución del plan (PLEXIL), un lenguaje síncrono desarrollado por la NASA para respaldar las operaciones de naves espaciales autónomas.