Real-Time Maude and Its Applications

Real-Time Maude extends the rewriting-logic-based Maude system to support the executable formal modeling and analysis of real-time systems. Real-Time Maude is characterized by its general and expressive, yet intuitive, specification formalism, and offers a spectrum of formal analysis methods, including: rewriting for simulation purposes, search for reachability analysis, and both untimed and metric temporal logic model checking. Real-Time Maude is particularly suitable for specifying real-time systems in an object-oriented style, and its flexible formalism makes it easy to model different forms of communication. This modeling flexibility, and the usefulness of both Real-Time Maude simulation and model checking, has been demonstrated in many advanced state-of-the-art applications, including both distributed protocols of different kinds and industrial embedded systems. Furthermore, Real-Time Maude's expressiveness has also been exploited to define the formal semantics of a number of modeling languages for real-time/embedded systems. Real-Time Maude thereby provides formal analysis for these languages for free, and such analysis has been integrated into the tool environment of a number of modeling languages. This paper gives an informal overview of Real-Time Maude and some of its applications.