The Real-Time Maude Tool

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

1. Real-Time Maude manual in pdf-format.
2. Papers related to Real-Time Maude
3. Executable example specifications

• July 2014: A version of Real-Time Maude that includes Daniela Lepri's TCTL model checker for Real-Time Maude is available here.
• August 9, 2007: Version 2.3 released; web pages updated.
• March 15, 2007: New results and conference paper on the OGDC wireless sensor network case study added.

1. Real-Time Maude team with email address for requests, comments, etc.

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

Each case study page below provides:

• overview and purpose of the case study
• executable Real-Time Maude specifications together with useful analysis commands
• related papers

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)