The Real-Time Maude Tool
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
Kronos, as well
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.
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.
Downloading and Running Real-Time Maude
- Downloading and running Real-Time Maude
Real-Time Maude Documentation, Related Papers, and Examples
- Real-Time Maude manual in pdf-format.
- Papers related to Real-Time Maude
- 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.
- Real-Time Maude team with
email address for requests, comments, etc.
Older Versions of Real-Time Maude
- Version 2.2 of the tool: file
This can be executed on version 2.2 of Maude.
2.1 of the tool: file
real-time-maude.maude. This can be executed on version 2.1 of Maude.
- Version 2.0 of the tool: file
and my modified prelude.maude
files for Real-Time Maude 2.0, which can be executed on version
2.0 of the Maude system.
- Change log
Each case study page below provides:
- overview and purpose of the case study
- executable Real-Time Maude specifications together with useful
- related papers
- (October 14, 2005) CASH scheduling algorithm:
maximizing processor utilization through capacity sharing mechanisms
- (June 23, 2005; updated March 15, 2007)
OGDC algorithm: achieving coverage
and longevity in wireless sensor networks
- AER/NCA protocol suite: Reliable,
scalable, and TCP-friendly multicast in active networks
- NORM IETF multicast protocol standard (By Elisabeth Lien)