Real-Time Maude Case Study: The
AER/NCA Protocol Suite
The AER/NCA protocol suite
combines several state-of-the-art techniques to achieve
adaptive reliable, scalable, and "TCP-friendly" multicast in
active networks. The protocol suite
consists of a collection of composable protocol components supporting
active error recovery
(AER) and nominee-based congestion avoidance (NCA) features, and makes
use of the possibility of having some processing
capabilities at ``active nodes'' between the sender and the receivers
to achieve scalability and efficiency.
The protocol itself was proposed by researchers at the University of
Massachusetts and at TASC, and was
originally specified informally as a set of use cases.
We have specified the whole protocol in Real-Time Maude 2.1, and have used
object-oriented techniques to be able to analyze each protocol
component separately, as well as to analyze the combined protocol.
Real-Time Maude analysis was able to uncover all errors discovered
independently by the protocol developers, as well as significant
design errors not discovered by the developers during
traditional simulation and testing.
- Specification and Analysis of the
AER/NCA Active Network Protocol
Suite in Real-Time Maude.
By Peter Csaba Ölveczky,
José Meseguer, and Carolyn L. Talcott.
of Computer Science, University of Illinois at Urbana-Champaign, July
This is an extensive report on the Real-Time Maude 2.1
specification and analysis of the AER/NCA protocol suite.
fair reliable multicast using active services.
By S. K. Kasera, S. Bhattacharyya, M. Keaton, D. Kiwior,
J. Kurose, D. Towsley and S. Zabele.
IEEE Network, vol. 14, pp. 48 -57, Jan./Feb. 2000.
Gives an overview of the AER/NCA protocol suite
and Analysis of Real-Time
and Hybrid Systems in Rewriting Logic.
By Peter Csaba Ölveczky.
Doctoral Thesis. University of Bergen, 2000.
Provides an extensive explanation of the Real-Time Maude 1.0
specification of the protocol, as well as the complete informal
use-case specification of AER/NCA in an appendix. This
thesis is slightly obsolete for AER/NCA, in particular in its
of the Real-Time Maude analysis.
The Informal Use Case Specification of AER/NCA
Version 1.0 of the informal use-case
specification of the AER/NCA protocol suite
provided the basis for our Real-Time Maude specification of the
protocol. In addition to using this specification, we
communicated with Mark Keaton on various issues of the protocol to
arrive at our Real-Time Maude specification.
This informal specification was written by Dr. G. Stephen Zabele, Mark
Keaton, and Diane Kiwior at Litton-TASC, Reading, Mass., and Dr. Don
Towsley, Dr. Jim Kurose, Dr. Supratik Bhattacharyya, and Dr. Sneha Kasera at
The University of Massachusetts, Amherst, and is a test
version which probably was not intended to be a
finished product. It is
given here to document the kind of specifications that we used as the
basis for developing our formal
specification. The specification can also be useful to
compare the different specification styles.
round trip time estimation (RTT) component,
nominee receiver selection (NOM) component,
rate control (RC) component, and
repair service (RS) component.
New version 1.1 of informal protocol description, incorporating
results from our specification and analysis effort:
RC component, and
The Executable Real-Time Maude 2.1 Specification of AER/NCA
- The Real-Time Maude files:
I have just re-tested all analysis commands, and everything works perfectly!
(some basic data types, including links and handling of time; starts by
loading ../real-time-maude.maude, please modify this line if
your real-time-maude.maude file is elsewhere in your file system)
(some classes which appear in many components)
(declarations of messages which appear in many components)
- rtt.rtmaude (specifies the RTT
- rttX.rtmaude (extends
rtt.rtmaude with some initial states, and includes all the
analysis commands -- commented away)
(for some attributes which are shared between some objects in
different protocol components)
(data type for sliding window for NOM component to determine lpe values)
- nom.rtmaude (specification of
the NOM component)
- nomX.rtmaude (extends
nom.rtmaude by adding appropriate initial states to test the
NOM component, and contains all analysis commands, commented away)
- ncarc.rtmaude (specification of
the RC component)
- ncarcX.rtmaude (extends
ncarc.rtmaude by adding appropriate initial states to test the
RC component, and contains all analysis commands, commented away)
(error classes for error in RS component)
- rs.rtmaude (specification of
the RS component)
- appLayer.rtmaude (defines
an "application layer" on top of AER/RS to test the RS component, and
the combined protocol)
(adds three initial state patterns to the application layer, and
contains the analysis commands for the RS component)
- comb.rtmaude (the combined
protocol, including suitable initial states and execution commands)
- How to execute/analyze these specifications?
- Copy all the above files with their given filenames.
- Modify, if necessary, the beginning of the file
that it reads real-time-maude.maude using the correct path in
your file system.
- To execute the RTT component specification, you can start Maude
with the file rttX.rtmaude as argument:
maude rttX.rtmaude. The file rttX.rtmaude
includes commands which reads the other necessary files.
The various analysis commands are in
this file, but are commented away; just remove the '***(' and ')'
parts around the commands, or cut-and-paste the desired command onto the Maude
- To execute the NOM, RC, RS components and the combined protocol,
do the same thing with, respectively, the files
appLayerX.rtmaude, and comb.