TY - GEN
T1 - Towards a maude formal environment
AU - Durán, Francisco
AU - Rocha, Camilo
AU - Álvarez, José María
N1 - Funding Information:
Acknowledgements. The authors would like to thank the anonymous referees for comments that helped to improved the paper. The first author has been partially supported by Spanish Research Projects TIN2008-03107 and P07-TIC-03184. The second author has been partially supported by NSF grants CNS 07-16638 and CCF 09-05584.
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84856591937&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-24933-4_17
DO - 10.1007/978-3-642-24933-4_17
M3 - Conference contribution
AN - SCOPUS:84856591937
SN - 9783642249327
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 329
EP - 351
BT - Formal Modeling
A2 - Agha, Gul
A2 - Meseguer, Jose
A2 - Danvy, Olivier
ER -