Result

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

Routing Loop-Free Counter Example

Advertisements
This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s