Recent Advances in Real-Time Maude

9 years 8 months ago
Recent Advances in Real-Time Maude
This paper gives an overview of recent advances in Real-Time Maude. Real-Time Maude extends the Maude rewriting logic tool to support formal specification and analysis of object-based real-time systems. It emphasizes ease and generality of specification and supports a spectrum of analysis methods, including symbolic simulation, unbounded and time-bounded reachability analysis, and LTL model checking. RealTime Maude can be used to specify and analyze many systems that, due to their unbounded features, such as unbounded data structures or dynamic object and message creation, cannot be modeled by current timed/hybrid automaton-based tools. We illustrate this expressiveness and generality by summarizing two case studies: (i) an advanced scheduling algorithm with unbounded queues; and (ii) a state-of-the-art wireless sensor network algorithm. Finally, we give some (often easily checkable) conditions that ensure that Real-Time Maude’s analysis methods are complete, also for dense time, ...
Peter Csaba Ölveczky, José Meseguer
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Peter Csaba Ölveczky, José Meseguer
Comments (0)