To begin formalizing BATMAN routing protocol, we need a network model! The following explains how we built our network model with Promela,

The B.A.T.M.A.N. routing protocol is intended to be deployed in mobile ad-hoc networks. These networks are characteristically prone to packet-loss, asymmetric links between nodes, and frequently- changing membership as nodes may enter, leave, or move in the network at any time. Furthermore, the algorithm specifies the sending of packets at regular intervals; therefore, an abstraction for time is necessary in the model. Although Promela provides a high-level abstraction for sending messages, queueing, and receiving messages in the form of channels, to meet the challenges of modeling a mobile network several data structures are necessary:

**Network Data Structure**

**int t**

We use a monotonically-increasing counter t, which is incremented by the process time(), to represent a notion of time in the model. It is used to control periodic flooding mechanism in the B.A.T.M.A.N algorithm and also the termination of the simulation. Note that the scale of t is arbitrary; in the time() process a loop counter is incremented to a certain threshold for each tick of t. Albeit arbitrary, this threshold is appropriate in conjunction with the other parameters of the model.

**chan chans[]**

The channel abstraction provides a receiving buffer for each node to receive packets from all other nodes. Inside each buffer, only packets passing the receiving rules and in the format above are accepted. The fields of each packet are specified later, in other post.

**ChannelStrength strengthFrom[N]**

The ChannelStrength data structure is used to implement the notion of packet loss and asymmetry in the network. It is a two-dimensional array of channel strengths from every node a to every node b in the network. For every element of this two-dimensional array, (a, b), we have (a,b) ∈ {0,1,2,3,4,5}. The interpretation of this number is that the probability of a successful send from node a to node b is 20 · (a, b)%. These discrete probabilities are used because there is no convenient way to generate random numbers (uniformly at random, especially in a large range) in Promela.

**FailedNodes Failed**

The global data structure contains an array of currently inactive nodes and a counter of the number of currently inactive nodes (which must not be more than MAX FAILED NODES. For example, if the field numfailedNodes == 1, then the only valid element in the node array is node[0], which holds the identifier of the inactive node.

**Network Process**

**proctype time()**

time() increments the network’s time counter t until it is equal to SIMULATION END TIME. It also calls the function alterNetwork() for every CHANGE INTERVAL units of time to change the topology of the network.

**inline setNeighbors()**

In this inline function, each node is assigned an initial set of neighbors, according to the network topology shown in figure below

. Therefore, each corner node has two neighbors, the middle node has four neighbors, and every other node has three neighbors initially.

**inline setChannelLossiness()**

The strength of each channel between neighboring nodes is initialized in this function, and given a random probability of successful delivery in the range {20%, 40%, 60%, 80%, 100%}.

**inline selectNodeToFail()**

This function selects a random valid node to deactivate. All nodes except those already in the FailedNodes data structure are valid to choose. This function will only be called if numFailedNodes < MAX FAILED NODES.

**inline selectNodeToActivate()**

selectNodeToActivate() randomly selects a node inside the failed node array failed and then activates it. The function only activates one node at a time.

**inline pickNewNeighs()**

In order to construct a dynamic network, when a node is reactivated (after having been deac- tivated by the alterNetwork() function), it chooses a new set of neighboring nodes. The selection of these neighbors tries to preserve locality by first randomly picking a node in the network to be its first neighbor. Then, with some probability, it become neighbors with the neighbor of the first-selected node. However, if none of these neighbors are chosen, the func- tion randomly selects another node in the network to be its neighbor. This guarantees that the node will have at least two neighbors in the network, and with a high probability these nodes will likely already be closely connected.

**inline alterNetwork()**

This function flips a coin, and with probability 50% chooses an inactive node to activate. Af- ter selecting a node, it instantiates pickNewNeighs() to set up its neighbors and assigns channel strengths to each neighbor. Also, independently from the previous action, the process deactivates an active node with a 50% probability.

**inline removeFailedNodes()**

This function loops through the direct-link neighbors of a given node and removes them from its list of neighbors if the host has not received a message from this neighbor in at least REM T time units. However, if a node loses all of its neighbors from this function, a new set of neighbors will be created.