We provide our example Promela source code and template here allowing others to further test the B.A.T.M.A.N. protocol.To run the SPIN model checker, please first install the appropriate software from SPIN’s official website (http://spinroot.com/spin/Man/README.html)
Next, due to upload file type, please download the following files and convert it to the correct file type.
These three files should be type .pml : Batman_Violation Batman_Template batmain.doc
This file should be type .py: RunBatman
The there are three options to run the source codes
- Run it with Batman.pml, our example code. Use the command
$ python RunBatman.py Batman.pml
to run the example source code which contains a network of nine nodes. The result will be written into the file Batman OUTPUT.txt Continue reading
Given that only one of the property among the five does not hold, we also inserted violations of all properties to check the algorithm we implemented correctly identifies those violations. The violations we inserted for each property is described below,
1. Violation 1: We only remove nodes from the network when t > 20. In this way, we are simu- lating the case where packets are injected into the network but are not recovered. Therefore, the assertion that the number of packets sent into the network is the same as the number of packets coming out of the network is false.
To test our implementation of the B.A.T.M.A.N routing protocol, we run the program using the SPIN model checker. The results of the simulations show that at least one property among the five does not hold. During the simulation, the assertion for the fourth property fails. Recall that the fourth property specifies that there are no routing loops in the network.
Although we do not know the exact series of events that caused the SPIN model checker to catch the flag the assertion as false, we can illustrate a counter-example to show that the protocol does not guarantee loop freedom. In the figure below, consider the case where node A tries to send an Originator message to the network. Let the number on each link represent the strength of the link, where 1 is the weakest and 5 is the strongest. When the OGM has been broadcasted to B from A, B re-broadcasts it to C and A with a decremented time-to-live (TTL = 4). However, the re-broadcasted OGM from B to A is dropped due to a weak link. Then, the same OGM is re-broadcasted back and forth between B and C until TTL = 0. At each opportunity for B to broadcast to A, the send fails. This would lead to a situation where C’s best route to A is through B (its only choice), but B thinks its best route to A is through C. This is because B has only received one OGM from A, but has received multiple OGMs from C via re-broadcasting. In other words, since it is the same OGM routing through each node, the sequence number will not be incremented, and the routing loop situation will not be recognizable by the receive() function.
Routing Loop-Free Counter Example
Now that we have described the model, the algorithm, and the properties that we wish to verify, we can describe how we implemented the algorithm in Promela and used assertion statements to verify the given properties.
BATMAN Data Structures
The type Neighbors contains the following fields,
· int neighs[N]:alistofidentifiersofthisnode’sdirectneighbors.
· int numNeighs:thenumberofdirect-linkneighbors.
· int initSeqNum:arandomly-assignedinitialsequencenumberintherange[0,…,216− 1].
· int lastSeqNum: the last sequence number that this noe has injected into the network via an Originator message.
· bit seqWraparound: a boolean containing whether the latest sequence number caused a wraparound.
· int sendingInitSeq: a boolean containing whether the node has yet to send the initial sequence number. The field lastSeqNum is not valid until this is set to 0.
· bit alive: a flag to indicate whether this node is active or inactive; used for blocking sending and receiving processes.
The following is a list of the five properties from the B.A.T.M.A.N. routing algorithm that we implement and analyze in our model.
The protocol specifies exactly what must happen to every Originator message that is injected into the network: “OGMs are flooded until every node has received it at least once, or until they get lost due to packet loss of communication links, or until their TTL (time to live) value has expired.”
We interpret this as asserting that all packets which are injected into the network must eventually leave the network. This property is based on the following assumptions:
(a) The TTL value is decremented with each hop in the network
(b) All nodes broadcast an OGM at some point
(c) All nodes re-broadcast an OGM upon receipt if the re-broading rules are satisfied
(d) With some probability packets are lost during the sending of routing messages
We gave a brief introduction about BATMAN in the earlier post, now we expand it more and explain how its algorithm works.
B.A.T.M.A.N., is a proactive routing protocol for mobile ad-hoc networking. Nodes within the network maintain fresh lists of destinations, called Originators, and properties about those Origina- tors. The basic strategy of B.A.T.M.A.N. is to find the best next-hop to the destination Originator given the source’s direct-link neighbors. The protocol is not concerned with the full forwarding path; it only chooses the best next-hop for a packet as a function of its intended destination.
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