Semantics and pragmatics of Real-Time Maude

Peter Csaba Ölveczky, José Meseguer

Research output: Contribution to journalArticlepeer-review


At present, designers of real-time systems face a dilemma between expressiveness and automatic verification: if they can specify some aspects of their system in some automaton-based formalism, then automatic verification is possible; but more complex system components may be hard or impossible to express in such decidable formalisms. These more complex components may still be simulated; but there is then little support for their formal analysis. The main goal of Real-Time Maude is to provide a way out of this dilemma, while complementing both decision procedures and simulation tools. Real-Time Maude emphasizes ease and generality of specification, including support for distributed real-time object-based systems. Because of its generality, falling outside of decidable system classes, the formal analyses supported-including symbolic simulation, breadth-first search for failures of safety properties, and model checking of time-bounded temporal logic properties-are in general incomplete (although they are complete for discrete time). These analysis techniques have been shown useful in finding subtle bugs of complex systems, clearly outside the scope of current decision procedures. This paper describes both the semantics of Real-Time Maude specifications, and of the formal analyses supported by the tool. It also explains the tool's pragmatics, both in the use of its features, and in its application to concrete examples.

Original languageEnglish (US)
Pages (from-to)161-196
Number of pages36
JournalHigher-Order and Symbolic Computation
Issue number1-2
StatePublished - Jun 2007


  • Formal analysis
  • Model checking
  • Object-oriented specification
  • Real-time systems
  • Rewriting logic
  • Simulation

ASJC Scopus subject areas

  • Software
  • Computer Science Applications


Dive into the research topics of 'Semantics and pragmatics of Real-Time Maude'. Together they form a unique fingerprint.

Cite this