Formal Specification of Trusted Neighbor Information Base of OLSR Routing Protocol of Adhoc Network Using Z Language

Nodes in an ad-hoc network lack the protection offered by firewalls in infrastructure-based networks. Trust based system aids to improvise this situation. A few works exists that handle the formal description of ad hoc networks. But describing correct specifications, reusing specifications, and constructing specifications repository are significant issues on software development to product safety and high quality software systems. In order to deal with such issues, we propose a formal specification of the Trusted Neighbor Information Base of OLSR routing protocol of ad hoc network using “Z” language. Z is a state-oriented formal specification language based on set theory and predicate logic. Specification languages are situated between natural and program languages. These types of languages enable to eliminate internal ambiguity, which is characteristic for natural languages. The Z notation is used to for formal specification of this part of the protocol. Finally, the formal specifications is verified and proved using Z Eves tool.