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
The algorithm dictates that no sequence number may be duplicated from an Originator node. Note that at any time a node may receive two OGMs from the same source; however, these must be re- broadcasts of the original OGM and must not have come from the source of the packets.
The assumptions present for this property are as follows:
(a) With every OGM, the Sequence Number is incremented
The third property we choose to examine is the correctness of the routing algorithm. If a destination is reachable from a given source, then the B.A.T.M.A.N. protocol should choose the correct first-hop link to that destination.
Note that we do not define correctness as choosing the link which leads to the highest probabilty of successful delivery to the destination. Our simulation includes probabilities for sending success for every link, and it is therefore possible to determine a most “correct” link in this way. However, this is information is outside of the knowledge of any node. Therefore, we define correctness to be the selection of the link with the highest number of recently received packets, as this is all of the information that a node has in order to make its routing decision.
This property is based on the following assumptions:
(a) Each node has a routing table showing the first-hop neighbors for every destination.
(b) UponreceiptofanOGM,thenodewillupdateitsB.A.T.M.A.N.datastructurestocountthenode where appropriate and will then re-calculate the best first-hop links.
The fourth property that we test is the absence of routing loops in the network: “B.A.T.M.A.N. chooses the most reliable route upon the next-hop routing decision of individual
nodes. This approach has shown in practise that it is reliable and loop-free.” We have the following assumptions for this property:
(a) Upon receipt of an OGM, the node only further processes it if the originator address is above or in the sliding window of sequence numbers.
(b) Upon receipt of an OGM above or in the sliding window, the best first-hop link will be re- calculated.
Finally, the last property that we verify is that there are no unidirectional links in a route: “The protocol ensures that a route consists of bidirectional links only.” This property is based on the following assumptions:
(a) Upon receipt of an OGM, the node drops the message if the uni-directional flag is set to one.
(b) Upon receipt of an OGM, if the uni-directional flag is set to 1 and if the last sequence number does not differ by more than a certain threshold from the last bi-directional sequence number, then the link is marked as unidirectional