Specification and Analysis of Real-Time Systems Using Real-Time Maude

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 objectoriented 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. Tools based on timed and linear hybrid automata, such as Uppaal [1], HyTech [2], and Kronos [3], have been successful in modeling and analyzing an impressive collection of real-time systems. While their restrictive specification formalism ensures that interesting properties are decidable, such finite-control automata do not support well the...

• Type: Conference
• Year: 2004
• Where: FASE
• Authors: Peter Csaba Ölveczky, José Meseguer
• Keywords: FASE 2004, Real-Time Maude, Real-time Systems, Software Engineering, Specification Formalism