Abstract
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 object-oriented 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. Journal on Software Tools for Technology Transfer 1, 134–152 (1997)
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer 1, 110–122 (1997)
Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1, 123–133 (1997)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Ölveczky, P.C., Keaton, M., Meseguer, J., Talcott, C., Zabele, S.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 333–347. Springer, Heidelberg (2001)
Ding, H., Zheng, C., Agha, G., Sha, L.: Automated verification of the dependability of object-oriented real-time systems. In: 9th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS 2003). IEEE Computer Society Press, Los Alamitos (2003)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Ölveczky, P.C., Meseguer, J.: Real-Time Maude: A tool for simulating and analyzing real-time and hybrid systems. In: Third International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 36. Elsevier, Amsterdam (2000), http://www.elsevier.nl/locate/entcs/volume36.html
Ölveczky, P.C., Meseguer, J.: Real-Time Maude 2.0. Submitted for publication (2004), http://heim.ifi.uio.no/~peterol/RealTimeMaude/rtm-papers.html
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Fourth InternationalWorkshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 71. Elsevier, Amsterdam (2002)
Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285, 359–405 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ölveczky, P.C., Meseguer, J. (2004). Specification and Analysis of Real-Time Systems Using Real-Time Maude. In: Wermelinger, M., Margaria-Steffen, T. (eds) Fundamental Approaches to Software Engineering. FASE 2004. Lecture Notes in Computer Science, vol 2984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24721-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-24721-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21305-5
Online ISBN: 978-3-540-24721-0
eBook Packages: Springer Book Archive