Real-Time Maude Case Study: The AER/NCA Protocol Suite

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.

Related Papers

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.
Manuscript, Department of Computer Science, University of Illinois at Urbana-Champaign, July 2004.
This is an extensive report on the Real-Time Maude 2.1 specification and analysis of the AER/NCA protocol suite.
Scalable 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
Specification 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 description 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.
Version 1.0: 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:
RTT component, NOM component, RC component, and RS component.

The Executable Real-Time Maude 2.1 Specification of AER/NCA

The Real-Time Maude files:

AER-prelude.rtmaude (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)
AER-commonclasses.rtmaude (some classes which appear in many components)
AER-shared-msgs.rtmaude (declarations of messages which appear in many components)
rtt.rtmaude (specifies the RTT protocol component)
rttX.rtmaude (extends rtt.rtmaude with some initial states, and includes all the analysis commands -- commented away)
AER-shared-atts.rtmaude (for some attributes which are shared between some objects in different protocol components)
EfficientWindow.rtmaude (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)
AER-error-object.rtmaude (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)
appLayerX.rtmaude (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)
I have just re-tested all analysis commands, and everything works perfectly!
How to execute/analyze these specifications?

Copy all the above files with their given filenames.
Modify, if necessary, the beginning of the file AER-prelude.rtmaude so 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 command line.
To execute the NOM, RC, RS components and the combined protocol, do the same thing with, respectively, the files nomX.rtmaude, ncarcX.rtmaude, appLayerX.rtmaude, and comb.

Peter Ölveczky