Papers Related To Real-Time Maude
|
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.:
- 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)
- 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)
- 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)
- 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:
- 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)
- 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)
- 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)
- 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)
- 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.
- 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