Towards a Maude Formal Environment

Abstract

Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in the development of formal analysis tools for checking specific properties of Maude specifications. This includes tools for checking termination, confluence, and inductive properties of rewrite theories. Nevertheless, most of these tools have been designed to work in isolation, making it difficult, for instance, to exchange data between them and inconvenient to switch between their environments. This paper presents the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can interact with tools to mechanically verify properties of Maude specifications. One important aspect of this work is that the MFE has been designed to be easily extended with tools having highly heterogeneous designs whilst creating synergy among them. As a proof of concept, we report on the integration of five commonly used formal analysis tools for Maude specifications into MFE and illustrate their interoperability with an example.

Maude es un lenguaje declarativo y reflexivo basado en una lógica de reescritura en la que el cómputo corresponde a una deducción eficiente por reescritura. Debido a sus capacidades reflexivas, Maude ha resultado útil como metaherramienta en el desarrollo de herramientas de análisis formal para verificar propiedades específicas de las especificaciones de Maude. Esto incluye herramientas para verificar la terminación, la confluencia y las propiedades inductivas de las teorías de reescritura. Sin embargo, la mayoría de estas herramientas han sido diseñadas para funcionar de forma aislada, lo que dificulta, por ejemplo, el intercambio de datos entre ellas y dificulta el cambio entre sus entornos. Este documento presenta Maude Formal Environment (MFE), una especificación formal ejecutable en Maude dentro de la cual un usuario puede interactuar con herramientas para verificar mecánicamente las propiedades de las especificaciones de Maude. Un aspecto importante de este trabajo es que el MFE ha sido diseñado para ser ampliado fácilmente con herramientas que tienen diseños muy heterogéneos, creando sinergia entre ellos. Como prueba de concepto, informamos sobre la integración de cinco herramientas de análisis formales de uso común para las especificaciones de Maude en MFE e ilustramos su interoperabilidad con un ejemplo.