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

  1. 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.
  2. 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
  3. 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

 
Peter Ölveczky