Abstract
Real-Time Maude is a language and tool supporting the formal specification and analysis of realtime 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 realtime systems. The tool offers a wide range of analysis techniques, including timed rewriting for simulation purposes, untimed and time-bounded search for states that are reachable from the initial state and match a given search pattern, and time-bounded linear temporal logic model checking. It has been used to model and analyze sophisticated communication protocols, and state-of-the-art wireless sensor network and scheduling algorithms. Real-Time Maude is an extension of Maude. This document describes the version 2.3 of the language and tool Real-Time Maude. Papers describing the versions 2 of the tool include [32, 33, 35]. The references [29, 30, 37] describe the obsolete prototype version 1 of Real-Time Maude.