Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude

This paper describes the application of the Real-Time Maude tool and the Maude formal methodology to the specification and analysis of the AER/NCA suite of active network multicast protocol components. Because of the time-sensitive and resource-sensitive behavior, the presence of probabilistic algorithms, and the composability of its components, AER/NCA poses challenging new problems for its formal specification and analysis. Real-Time Maude is a natural extension of the Maude rewriting logic language and tool for the specification and analysis of real-time object-based distributed systems. It supports a wide spectrum of formal methods, including: executable specification; symbolic simulation; breadth-first search for failures of safety properties in infinite-state systems; and linear temporal logic model checking of time-bounded temporal logic formulas. These methods complement those offered by network simulators on the one hand, and timed-automaton-based tools and general-purpose theorem provers on the other. Our experience shows that Real-Time Maude is well-suited to meet the AER/NCA modeling challenges, and that its methods have proved effective in uncovering subtle and important errors in the informal use case specification.

1. It is however possible to use formal methods and tools to support the passage from informal to formal specifications: a fairly large body of work on the formal underpinnings of UML, as well as work on passing from scenarios to system specifications and code [11] are good examples of work in this direction. But it does not follow from this that a full formalization of the entire process is possible: just the simple fact that ethical decisions are often involved in the choice of the relevant properties, particularly for safety-critical systems, seems to us a clear indication that it isn’t.

2. Active networks allow users to inject programs into the nodes of the network.

3. Rewrites cannot take place in a frozen argument position of a function symbol, so that a term \(f(t_1, \ldots, t_i, \ldots, t_n)\) will not rewrite to \(f(t_1, \ldots, u_i, \ldots, t_n)\) when t _i rewrites to u _i if \(i\in \phi(f)\).

4. In general, the condition of such rules may not only contain rewrites \(u_i\longrightarrow v_i\) and equations \(w_j=w'_j\), but also memberships \(t_k:s_k\); however, the specifications in this paper do not use this extra generality.

5. Operationally, a term is reduced to its E-normal form modulo A before any rewrite rule is applied in Maude. Under the coherence assumption [33] this is a complete strategy to achieve the effect of rewriting in \(E\cup A\)-equivalence classes.

6. In Real-Time Maude, being an extension of Full Maude, module declarations and execution commands must be enclosed by a pair of parentheses.

7. If one or more of an object's attributes are of sort Object or Configuration, an object may contain other objects, or even entire configurations, as parts of its state, giving rise to “Russian dolls” distributed object architectures [17].

8. The attributes and rules of a class cannot be redefined by its subclasses, but subclasses may introduce additional attributes and rules.

9. For the purpose of conveniently defining initial states, Real-Time Maude allows the user to introduce operators of sort GlobalSystem, such as RTTstate2 in Section 4.11.2. Each ground term of sort GlobalSystem must reduce to a term of the form { t } using the equations in the specification.

10. Since the temporal logic model checker uses depth-first search techniques, there are cases in which the check command terminates even without a time limit, and where the temporal logic model checker would loop. One such example is shown in Section 4.13.

11. The operators delta and mte should be declared to be frozen operators (see Section 3.1) in their first argument position to avoid ill-timed rewrites or rewrites in the time domain [24, 26].

12. Recall from Section 3.1 that the attributes assoc, comm, and id: none of the operator \(\mathtt{\_\:\_}\) state that \(\mathtt{\_\:\_}\) is associative, commutative, and has identity element none. That is, together with the subsort Oid < OidSet, this operator defines multisets of Oid elements, where the order of the elements does not matter.

13. The list concatenation operator \(\mathtt{\_+\_}\) is declared to be associative (assoc), so that parentheses are not needed and rules can match such lists with associative pattern matching.

14. Maude supports both “Peano” and ordinary decimal representation of natural numbers, so that s N (in rule outOfDownLink) is an equivalent representation of N + 1. Furthermore, s N is an irreducible term which can be used as a pattern in the left-hand side of a rule.

15. Since the total delay of a packet entering the link is larger than the delay of the packets already in the link, the first (leftmost) packet will have the smallest delay, and the last packet will have the largest delay.

16. The output of Real-Time Maude executions will be manually tabulated for readability purposes, and parts of the output omitted in the exposition will be replaced by ‘...'

17. Although the lpe estimates are then considered less reliable, this avoids having long initial computation segments that could cause combinatorial explosion when performing formal analysis. Furthermore, the design errors we found did not depend on the specific value chosen for the size bound.

18. Since there is no repair service intervention for the NAMPackets, we have abstracted from their transmission times. The situation is even worse when there is a non-zero time interval without a nominee receiver. Indeed, even if the new nominee is aware of it being the new nominee before the old nominee becomes aware of the change, the protocol may still miss to acknowledge a data packet which arrives at the new nominee much earlier than at the old nominee.

19. The sender sends an SPM packet when the protocol starts, explaining why the link becomes full after 9 data packets.

We are grateful to Mark Keaton and Steve Zabele for their invaluable cooperation during the specification and analysis of a previous version, in Real-Time Maude 1.0, of the AER/NCA protocol suite. Their explanation of AER/NCA and related issues, their feedback to our specification efforts, and their suggestions of suitable initial states for the analysis parts were essential for the modeling and analysis described in this paper. We also thank the anonymous referees for many helpful comments on a previous version of this paper. Partial support of this research by ONR Grant N00014-02-1-0715, by NSF Grant CCR-0234524, by DARPA through Rome Labs. Contract F30602-97-C-0312, and by The Norwegian Research Council is gratefully acknowledged.

Authors and Affiliations

1. Department of Computer Science, Thomas M. Siebel Center for Computer Science, 201 N Goodwin Ave, Urbana, IL, 61801-2302, USA

   Peter Csaba Ölveczky & José Meseguer

2. Department of Informatics, University of Oslo, P.O. Box 1080 Blindern, 0316, Oslo, Norway

   Peter Csaba Ölveczky

3. Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA, 94025-3493, USA

   Carolyn L. Talcott

Corresponding author

Correspondence to Peter Csaba Ölveczky.

Reprints and permissions