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, and time-bounded linear temporal logic model checking. It has been used to model and analyze sophisticated communication protocols and scheduling algorithms. Real-Time Maude is an extension of Maude and a major redesign of an earlier prototype.
Note: Our tool paper at TACAS 2008 is a newer short tool paper which gives an updated overview of Real-Time Maude, including an overview of some case studies and our completeness results. However, the FASE 2004 paper gives more details about the technicalities of the tool.