This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

(Please note that Real-Time Maude also has a user manual, and that other unpublished papers are available under the different case studies pages, all accessible from the main page. This is a partial list of publications on Real-Time Maude. Some other papers are available from my list of publications.)

Papers on the tool and its theoretical foundations, etc.:

1. The paper on Real-Time Maude and its semantics:
   Semantics and Pragmatics of Real-Time Maude.
   By Peter C. Ölveczky and José Meseguer.
   In volume 20 of Higher-Order and Symbolic Computation, 2007.
   (pdf; official site of paper at Springer; bibtex entry)

2. A paper which gives some (usually easily checkable) criteria for completeness of "maximal time sampling" analysis in Real-Time Maude. This gives us completeness of Real-Time Maude analyses for dense time for a large class of systems beyond those that can be captured by timed automata, including our wireless sensor network case study:
   Abstraction and Completeness for Real-Time Maude.
   By Peter C. Ölveczky and José Meseguer.
   In Proc. 6th International Workshop on Rewriting Logic and its Applications (WRLA 2006), volume 176 of Electronic Notes in Theoretical Computer Science.
   (paper in pdf; bibtex entry)
   (extended and revised report)

3. A very brief high-level overview of the tool (this paper is becoming somewhat dated, and should be replaced by something more up-to-date):
   Specification and Analysis of Real-Time Systems Using Real-Time Maude.
   By Peter C. Ölveczky and José Meseguer.
   In Proc. Fundamental Approaches to Software Engineering (FASE), 2004. Volume 2984 of Lecture Notes in Computer Science, Springer, 2004.
   (ps, pdf; bibtex entry)

4. The theoretical foundations of the computational model (real-time rewrite theories):
   Specification of real-time and hybrid systems in rewriting logic.
   By Peter C. Ölveczky and José Meseguer.
   In Theoretical Computer Science, number 285, 2002.
   (ps, dvi, gzipped ps, gzipped dvi; bibtex entry)

Papers on applications of Real-Time Maude:

1. The following paper is a somewhat extended version of a conference paper presented at FMOODS 2007 that summarizes the OGDC wireless sensor network case study.
   Formal Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude.
   By Peter C. Ölveczky and Stian Thorvaldsen.
   In Proc. 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 07), volume 4468 of Springer's Lecture Notes in Computer Science, 2007.
   (pdf of extended paper; official site of paper at Springer; bibtex entry)

2. A conference paper on the CASH scheduling protocol case study:
   Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real-Time Maude.
   By Peter C. Ölveczky and Marco Caccamo.
   In L. Baresi and R. Heckel (Eds.), Fundamental Approaches to Software Engineering 2006 (FASE '06), volume 3922 of Springer Lecture Notes in Computer Science, pp. 357-372, 2006.
   (pdf; bibtex entry)

3. A 40+ page journal paper on the use of Real-Time Maude 2.1 to specify and analyze the AER/NCA active network protocol suite:
   Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude.
   By P. C. Ölveczky, J. Meseguer, and C. Talcott.
   In volume 29(3) of Formal Methods in System Design, 2006.
   (pdf; bibtex entry)
   • An even more detailed report on this case study is avaliable as technical report no. UIUCDCS-R-2004-2467, Department of Computer Science, University of Illinois at Urbana-Champaign.
     (pdf)
   • A high-level overview of the large AER/NCA case study illustrates the use of version 1 of the tool (and is therefore somewhat obsolete):
     Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude.
     By P. C. Ölveczky, M. Keaton, J. Meseguer, C. Talcott, and S. Zabele.
     In Proc. FASE 2001, LNCS 2029.
     (ps, dvi, gzipped ps, gzipped dvi)

4. A paper on the application to time-sensitive cryptographic protocols, exemplified by the use on the semi-benchmark wide-mouthed frog protocol:
   Formal Analysis of Time-Dependent Cryptographic Protocols in Real-Time Maude.
   By Peter C. Ölveczky and M. Grimeland.
   In Proceedings of IPDPS 2007, IEEE Computer Society Press, 2007. (The paper was presented at the Workshop on Parallel and Distributed Real-Time Systems at IPDPS.)
   (pdf; bibtex entry)

5. Real-Time Maude, again version 1, has been used to develop an execution environment for a real-time extension of the Actor model:
   Automated verification of the dependability of object-oriented real-time systems.
   By H. Ding, C. Zheng, G. Agha, and L. Sha.
   In Proc. 9th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS'2003). IEEE Computer Society Press, 2003.

6. Different descriptions of the obsolete first version of the tool have occurred in my Dr.Scient. thesis, 2000, in the proceedings of the Third International Workshop on Rewriting Logic and its Applications, 2000, and in the Workshop on Real-Time Tools, Aarhus, 2001.
   Peter Ölveczky