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

  • typedef Neighbors

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.

  • typedef WindowUnit

The type WindowUnit contains the following fields to keep track of the correct range of sequence numbers that the node has received:

· int seqNum: the sequence number representing this block in the window

· byte numRec: number of times this sequence number has been received.

  • typedef Neighbor

The type Neighbor contains the following fields:

· WindowUnit w[WINDOW SIZE]: a collection of sequence numbers that are within the sliding window.

· int packetCount: count of sequence numbers in the sliding window.

· bit uni: A boolean containing whether the link to this neighbor is unidirectional.

  • typedef Originator

Type Originator contains the following fields,

· int lastTime: the time stamp of when this originator was last updated.

· int bidirSeqNum: the sequence number of the last self-initiated OGM received from a direct link neighbor.

· int curSeqNum: the most current sequence number that has been received.

· int bestLink: the best first-hop gateway to this destination.

· bit curSeqValid: a boolean containing whether the curSeqNum field is valid.

· Neighbor neigh[N]: a list of direct-link neighbors’ information.

BATMAN Processes – Sending

  • inline setInitSeqNums()

Each node is initially set to a integer sequence number in the range of [0, 216 − 1]. A random- number generator in a python preprocessing script is utilized for new random initial sequence numbers every time the simulation is run.

  • inline getJitter()

getJitter() assigns an integer value in the range {−2, −1, 0, 1, 2} to a jitter variable. The jitter value is used to add some randomness to the expire variable after the initial expiration has been reached.

  • inline sendOGM()

sendOGM() sends an OGM with some probability of failure to all its direct-link neighbors. A random integer number in the range {0, 1, 2, 3, 4} is obtained before the process sends the OGM. If the value of random number is greater than the channel’s strength, which is in the range {1, 2, 3, 4, 5}, the send failed. In this way, the simulation exhibits the property of packet loss, which is common in mobile networks.

  • proctype send()

send() function is called during the init of this model. Inside each send() instantiation, when the time counter t equals teh current node’s expire value, it calls sendOGM() for each of its direct-link neighbors. After sending an OGM to each neighbor, it then adjusts its expire value with a random jitter value and ORIGINATOR INTERVAL.

BATMAN Process – Receiving

  • inline bidirectionalLinkCheck()

This inline function checks if the link is bi-directional. It follows the B.A.T.M.A.N. protocol specifications, which dictate that if the sequence number in the received message is within LINK TIMEOUT units of the last recorded bi-directional sequence number, then the check succeeds; this link is then considered bi-directional. If the check does not succeed, then this link is marked as unidirectional.

  • inline moveSlidingWindows()

This inline function moves the sliding windows of all direct-link neighbors so that the most recent block in the window contains the most recently-received sequence number from a given Originator. Along the way, this function also updates the packet counts for each direct-link neighbor.

  • inline updateSeqNumCount()

This inline function updates the sequence number count in each direct-link’s window. The numReceived in each window is therefore incremented by one, and the packetCount field for each link is incremented by one as well.

  • inline calculateBestLink()

This inline function calculate the best first-hop link that should be used in order to forward a packet between a given source and destination. This best link is one of the direct-link neighbors of the source. If there are ties in calculating which link has the highest number of packets received, they are broken arbitrarily.

  • inline rebroadcastOGM()

This inline function rebroadcasts an OGM only when a packet with the unidirectional flag is not set. If the link is bi-directional, the OGM is rebroadcasted to all direct-link neighbors with some probability of failure.

  • proctype receive()

The receive() process will block until it has received a message in its buffer. After re- ceiving a message, the process performs many checks before successfully recording it into its

channel. We categorize into three cases when the message is dropped:

· Case 1: If this node sent this OGM to itself, the OGM is dropped.

· Case 2: If the unidirectional flag is set, the OGM is dropped.

· Case 3: If this node is the source of the OGM, a bi-directional link check is issued and then the OGM is dropped.

· Case 4: If the OGM’s sequence number is below the sliding window range, the OGM is dropped.

If the OGM passes the checks, it rebroadcasts the message to all of its direct-link neighbors.

BATMAN Processes – Generating Data Packets

The B.A.T.M.A.N. algorithm can be run completely with the above implementation. However, in order to test that implementation, we need to generate and handle data packets in the model. There- fore, in this section we shift from the control-plane to the data-plane and explain how data packets are handled in the model.

  • inline generatePacket()

This function is called by the time() process to generate a packet with a random source and destination every GEN PACKET time units.

  • inline handlePacket()

Upon receipt of a data packet, the receive() process instantiates this function to handle packet forwarding. Therefore, all this function must do is select the best first-hop link for a given destination, which has been set up by the B.A.T.M.A.N. routing algorithm. If the node has no direct-link neighbors, then the packet must be dropped.

BATMAN Properties

We now discuss how we implemented the verification of the five chosen properties, as outlined in previous post. All of the properties are implemented using assert statements.

(a) To ensure that all messages which enter the network eventually leave the network, we use two global (and atomic) variables messsagesIn and messagesOut. Every time we write or read these variables, we wrap the execution in the atomic structure provided by Promela. This ensures mutual exclusion and the integrity of the variables across concurrent access.

The messagesIn variable is incremented in sendOGM(), rebOGM, handlePacket(), and generatePacket(). The messagesOut variable is incremented in receive().

At every second, the model then asserts that the number of messages that have entered into the network is equal to the messages that have left the network plus the number of messages that are buffered in queues.

(b) To ensure that there are no redundant OGMs entering the network, we keep a record of the last sequence number that was sent from a given node in the lastSeqNum field of the Neighbors data structure.

If a node ever attempts to send an OGM with a sequence number that is less than or equal to the lastSeqNum field– without having wrapped around– then we flag that as a violation of the property.

(c) Toverifythecorrectnessoftheroutingalgorithm,wegeneratepacketsinournetworkandforward them according to forwarding rules devised by the B.A.T.M.A.N. algorithm. We warm-up the routing infrastructure by only generating and sending these data packets during the second half of the program’s execution.

When a packet is about to be forwarded, the given source node will fetch the best first-hop link as set by the routing protocol. To ensure that this best link is correct, we then loop through all of the available first-hop neighbors and check whether there is a neighbor that has a higher packet count for the given destination than does the supposed best link. Therefore, if there is a better, more “correct” link in terms of the B.A.T.M.A.N. algorithm, an assertion failure will ensue.

(d) As packets are passed through the network we must verify that no routing loops occur, per the fourth property that we are verifying. To do this, each data packet contains a length-N bit-array, where element i will contain a 1 if the packet has visited that node along the path. Upon receipt of a packet, the handlePacket() function will mark this LoopCheck data structure to signal that the packet has been present.

If, in handlePacket(), it is detected that this packet has already reached this node before, it means that a routing loop has occurred. Therefore, a violation of the property will have occurred.

(e) During the execution of the routing algorithm, the receive() performs a bi-directional link check if the receiving node is the same as the Originator of the message. This bi-directional link check will fail if the received sequence number is more than LINK TIMEOUT time steps away from the last bi-directional sequence check number. If the check fails, then the link will be flagged as unidirectional.

Therefore, to check if the algorithm uses unidirectional links, in the handlePacket() function we check that the best first-hop link is bi-directional. If it has been flagged as unidirectional, then the assertion will fail.

This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

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

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

Google+ photo

You are commenting using your Google+ 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 )


Connecting to %s