Author Archives: bucs512

Test it with Our Model

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, … Continue reading

Posted in Uncategorized | Leave a comment

Discussion and Conclusion

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, … Continue reading

Posted in Uncategorized | Leave a comment

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 … Continue reading

Posted in Uncategorized | Leave a comment

BATMAN Model

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 … Continue reading

Posted in Uncategorized | Leave a comment

Finalize Five Properties & Assumptions

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. Property 1 The protocol specifies exactly what must happen to every Originator message that is injected into the … Continue reading

Posted in Uncategorized | Leave a comment

Inside BATMAN

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 … Continue reading

Posted in Uncategorized | Leave a comment

Our Network Model

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 … Continue reading

Posted in Uncategorized | Leave a comment