Towards a Maude Formal Environment

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.

• Autores: Durán, Francisco; Rocha, Camilo; Álvarez, José María
• Tipo de recurso: Part of book
• Fecha de publicación: 2011
• Institución: Escuela Colombiana de Ingeniería Julio Garavito
• Repositorio: Repositorio Institucional ECI
• Idioma: eng
• OAI Identifier: oai:repositorio.escuelaing.edu.co:001/1890
• Acceso en línea: https://repositorio.escuelaing.edu.co/handle/001/1890
• Palabra clave: MAUDE; Obligación de prueba; Objeto controlador; Objeto de herramienta; MFE; Critical Pair; Proof Obligation; Tool Object; Active Tool; Controller Object
• Rights: closedAccess
• License: © Springer-Verlag Berlin Heidelberg 2011