Maude as a formal meta-tool

M. Clavel, F. Durán, S. Eker, J. Meseguer, M. O. Stehr

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Given the different perspectives from which a complex software system has to be analyzed, the multiplicity of formalisms is unavoidable. This poses two important technical challenges: how to rigorously meet the need to interrelate formalisms, and how to reduce the duplication of effort in tool and specification building across formalisms. These challenges could be answered by adequate formal meta-tools that, when given the specification of a formal inference system, generate an efficient inference engine, and when given a specification of two formalisms and a translation, generate an actual translator between them. Similarly, module composition operations that are logic-independent, but that at present require costly implementation efforts for each formalism, could be provided for logics in general by module algebra generator meta-tools. The foundations of meta-tools of this kind can be based on a metatheory of general logics. Their actual design and implementation can be based on appropriate logical frameworks having efficient implementations. This paper explains how the reflective logical framework of rewriting logic can be used, in conjunction with an efficient reflective implementation such as the Maude language, to design formal meta-tools such as those described above. The feasibility of these ideas and techniques has been demonstrated by a number of substantial experiments in which new formal tools and new translations between formalisms, efficient enough to be used in practice, have been generated.

Original languageEnglish (US)
Title of host publicationFM 1999 - Formal Methods - World Congress on Formal Methods in the Development of Computing Systems, Proceedings
EditorsJeannette M. Wing, Jim Woodcock, Jim Davies
PublisherSpringer-Verlag Berlin Heidelberg
Pages1684-1703
Number of pages20
ISBN (Print)3540665889, 9783540665885
DOIs
StatePublished - Jan 1 1999
Externally publishedYes
Event1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999 - Toulouse, France
Duration: Aug 20 1999Aug 24 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1709
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st World Congress on Formal Methods in the Development of Computing Systems, FM 1999
CountryFrance
CityToulouse
Period8/20/998/24/99

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Maude as a formal meta-tool'. Together they form a unique fingerprint.

Cite this