Recent Advances in Real-Time Maude

Peter Csaba Ölveczky, José Meseguer

Research output: Contribution to journalArticlepeer-review


This paper gives an overview of recent advances in Real-Time Maude. Real-Time Maude extends the Maude rewriting logic tool to support formal specification and analysis of object-based real-time systems. It emphasizes ease and generality of specification and supports a spectrum of analysis methods, including symbolic simulation, unbounded and time-bounded reachability analysis, and LTL model checking. Real-Time Maude can be used to specify and analyze many systems that, due to their unbounded features, such as unbounded data structures or dynamic object and message creation, cannot be modeled by current timed/hybrid automaton-based tools. We illustrate this expressiveness and generality by summarizing two case studies: (i) an advanced scheduling algorithm with unbounded queues; and (ii) a state-of-the-art wireless sensor network algorithm. Finally, we give some (often easily checkable) conditions that ensure that Real-Time Maude's analysis methods are complete, also for dense time, for object-based real-time systems. In practice, our result implies that Real-Time Maude's time-bounded search and model checking of LTL time-bounded formulas are complete decision procedures for a large and useful class of non-Zeno real-time systems that fall outside the scope of systems that can be modeled in decidable fragments of hybrid automata, including the sensor network case study discussed in this paper.

Original languageEnglish (US)
Pages (from-to)65-81
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Issue number1
StatePublished - Apr 24 2007


  • Maude
  • completeness
  • formal analysis
  • object-oriented specification
  • real-time systems
  • rewriting logic
  • wireless sensor networks

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Recent Advances in Real-Time Maude'. Together they form a unique fingerprint.

Cite this