Synchronous set relations in rewriting logic

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.

• Autores: Muñoz, César; Rocha Niño, Hernán Camilo
• Tipo de recurso: Article of journal
• Fecha de publicación: 2014
• Institución: Escuela Colombiana de Ingeniería Julio Garavito
• Repositorio: Repositorio Institucional ECI
• Idioma: eng
• OAI Identifier: oai:repositorio.escuelaing.edu.co:001/1864
• Acceso en línea: https://repositorio.escuelaing.edu.co/handle/001/1864
• Palabra clave: Relaciones de conjuntos sincrónicos; semántica síncrona; Reescritura de lógica; Simulación formal y verificación; Maude; Synchronous set relations; Synchronous semantics; Rewriting logic; Formal simulation and verification; PLEXIL
• Rights: openAccess
• License: © 2013 Elsevier B.V. Published by Elsevier B.V. All rights reserved.