Specification and Analysis of Real-Time Systems Using Real-Time Maude

Peter Csaba Ölveczky, José Meseguer

Research output: Contribution to journalArticle


Real-Time Maude is a language and tool supporting the formal specification and analysis of real-time and hybrid systems. The specification formalism is based on rewriting logic, emphasizes generality and ease of specification, and is particularly suitable to specify objectoriented real-time systems. The tool offers a wide range of analysis techniques, including timed rewriting for simulation purposes, search, and time-bounded linear temporal logic model checking. It has been used to model and analyze sophisticated communication protocols and scheduling algorithms. Real-Time Maude is an extension of Maude and a major redesign of an earlier prototype.

Original languageEnglish (US)
Pages (from-to)354-358
Number of pages5
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - Dec 1 2004

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Specification and Analysis of Real-Time Systems Using Real-Time Maude'. Together they form a unique fingerprint.

  • Cite this