Speed The Real-Time Maude Tool All kinds of timed systems can be modeled

The Real-Time Maude tool (version 2.3)

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 object-oriented real-time systems. The tool offers a wide range of analysis techniques, including timed rewriting for simulation purposes, search, time-bounded and unbounded linear temporal logic model checking, and timed CTL (TCTL) model checking. It has been used to model and analyze sophisticated communication protocols and scheduling algorithms, and as semantic framework and formal analysis tool for a number of modeling languages for embedded systems, including Ptolemy II discrete-event models, subsets of AADL, Timed Rebeca, handset languages developed in industry, and so on.

Real-Time Maude can be seen as complementing on the one hand timed/hybrid automaton-based tools such as Uppaal, HyTech, and Kronos, as well as e.g. timed Petri nets, by providing a much more expressible specification language with good support for real-time object-oriented specification, and on the other hand as complementing traditional testbeds and simulation tools by providing a wide range of formal analysis techniques and a more abstract specification formalism in which different forms of communication can be easily modeled.

Real-Time Maude is implemented in Maude as an extension of Full Maude 2.3. The current version of the tool runs on versions 2.3, 2.4, and 2.6 of Maude.

There are very few Real-Time Maude-specific differences between version 2.2 and version 2.3 of the tool, so that most likely you will not have to change your specifications and analysis commands. (Changelog)

Downloading and Running Real-Time Maude

  1. Downloading and running Real-Time Maude
Real-Time Maude Documentation, Related Papers, and Examples
  1. Real-Time Maude manual in pdf-format.
  2. Papers related to Real-Time Maude
  3. Executable example specifications
Latest News
General Information
  1. Real-Time Maude team with email address for requests, comments, etc.
Older Versions of Real-Time Maude
  1. Version 2.2 of the tool: file real-time-maude.maude. This can be executed on version 2.2 of Maude.
  2. Version 2.1 of the tool: file real-time-maude.maude. This can be executed on version 2.1 of Maude.
  3. Version 2.0 of the tool: file real-time-maude.maude and my modified prelude.maude files for Real-Time Maude 2.0, which can be executed on version 2.0 of the Maude system.
  4. Change log
Larger Case Studies

Each case study page below provides:

Case studies:
  1. (October 14, 2005) CASH scheduling algorithm: maximizing processor utilization through capacity sharing mechanisms
  2. (June 23, 2005; updated March 15, 2007) OGDC algorithm: achieving coverage and longevity in wireless sensor networks
  3. AER/NCA protocol suite: Reliable, scalable, and TCP-friendly multicast in active networks
  4. NORM IETF multicast protocol standard (By Elisabeth Lien)
Peter Ölveczky