Simulation and Verification of Synchronous Set Relations in Rewriting Logic
Documento de Conferencia
2011
NASA Langley Research Center
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 consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables
the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm verification techniques already
available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with
an executable operational semantics of a simple synchronous language
and the verification of temporal properties of a synchronous system. 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 consiste en una teoría de reescritura ordenada en Maude, un sistema lógico de reescritura, que 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 existentes ya disponibles en Maude para la reescritura asincrónica tradicional, como el análisis de accesibilidad y la verificación de modelos, están disponibles automáticamente para la reescritura sincrónica de conjuntos. El uso de la infraestructura se ilustra con una semántica operativa ejecutable de un lenguaje síncrono simple y la verificación de las propiedades temporales de un sistema síncrono.
Descripción:
Artículo principal.
Título: Simulation and Verification of Synchronous Set.pdf
Tamaño: 253.2Kb
PDF
Título: Simulation and Verification of Synchronous Set.pdf
Tamaño: 253.2Kb