Formal Specification and Analysis of Real-Time Systems in Real-Time Maude

Real-Time Maude is a tool that 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 temporal logic model checking. Our tool is particularly suitable to specify 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 Real-Time Maude for both simulation and model checking, has been demonstrated in advanced state-of-the-art applications, including scheduling and wireless sensor network algorithms, communication and cryptographic protocols, and in finding several bugs in embedded car software that were not found by standard model checking tools employed in industry.

This talk gives a high-level overview of Real-Time Maude and some of its applications, and briefly discusses completeness of analysis for dense-time systems.