Sciweavers

Share
FASE
2004
Springer

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

9 years 6 days ago
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...
Peter Csaba Ölveczky, José Meseguer
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where FASE
Authors Peter Csaba Ölveczky, José Meseguer
Comments (0)
books