Specification and Analysis of a Reliable Broadcasting Protocol in Maude - Static Network Topology


 
  The following is a somewhat abbreviated version of the informal specification given by José Garcia-Luna, which describes the proposed protocol for the static topology. A static network is modeled as an undirected connected graph where each node knows its neighbors but does not know anything more about the topology. The objective of the protocol is to broadcast the message from a source node to all the nodes in the network and to give feedback to the source. We only consider one round of the protocol - only one message is to be broadcasted from some source j to all nodes reachable from j. Handling multiple messages from each source can be easily accommodated by means of bit vectors or counters.

Initially, for every node i in the network, si=nil (this value denotes the ``parent'', i.e., the propagator, of nodei ) and SNi=nil (SNi denotes the set of neighbors from which i has received the message). The cycle starts with the source node sending the message to all its neighbors, and terminates when the source node has received an acknowledgment from all its neighbors. Every node i other than the source node reacts in the following way to input events (reception of message or acknowledgment):

  1. If i receives a message for the first time, say from node p, it sets si=p (p is the parent of i), adds the node p to the set SNi (the set of nodes from which it has received the message), and propagates the message to every node in the set Ni-p.
  2. If node i receives a message from a node q when it has already has received the message from some other node, then it simply adds q to the set SNi.
  3. When node i has received an acknowledgment from every node in the set Ni-SNi, it sends an acknowledgment to every node in the set SNi-si.
  4. When node i receives acknowledgment from every neighbor in the set SNi-si, it sends an acknowledgment to its parent node si.

The Maude specification for the static network topologies

Note that we have defined three test configurations, namely, test3, test4, and test6. test4 is declared as follows in the specification: 

eq test4 =
  (to a broadcast m)  
  < a : Node | nbs : b c, parent : noOid, recdMsg : nil, recdAck : nil >
  < b : Node | nbs : a c, parent : noOid, recdMsg : nil, recdAck : nil >
  < c : Node | nbs : b a d, parent : noOid, recdMsg : nil, recdAck : nil >
  < d : Node | nbs : c, parent : noOid, recdMsg : nil, recdAck : nil > .
This configuration models a network with 4 nodes, a, b, c, and d, and where there are links between a and b, between a and c, between b and c, and between c and d. The message (to a broadcast m) initiates a round of the protocol. The initial states can be used to immediately execute the specification. After a round of the protocol, the system should be in a state where all messages have seen the message, and received the various acknowledgments, and there should be no message left in the configuration. Using Maude's default interpreter, we can immediately execute an arbitrary run of the system.

Test runs using Maude's default interpreter.

Sample execution:
1. Store Maude specification as "rbpStatic.maude"
2. Start full-maude
3. "Maude> in rbpStatic.maude"
4. Execute sample runs, e.g., "Maude> (rew test3 .)"

Maude's default interpreter only executes one of the many possible rewrite paths starting with a given initial term. For a deeper analysis, we wrote a strategy which returns all nonrewritable states reachable from the initial state. In the static case, there should only be one such term.

The specification of the strategy

Test runs of this exhaustive search strategy for the static case

Sample execution:
1. Store Maude specification for strategy as "strat.maude"
2. Start full-maude
3. "Maude> in rbpStatic.maude"
4. "Maude> in strat.maude"
5. Execute sample runs, e.g., "Maude> (red irreducibleforms(RBP, {'test3}'Configuration, allstaticrules) .)"

 
[Maude Home Page]