Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B

Ad hoc routing protocols are responsible for searching a route from the source to the destination under the dynamic network topology. Hybrid routing protocols combine the features of proactive and reactive approaches. So, the formal specification of a hybrid routing protocol in the dynamic network environment is a challenge. In this paper, we formally analyze the Zone Routing Protocol (ZRP), a hybrid routing framework, using Event-B. We develop the formal specification by the refinement mechanism. It allows us to gradually model the network environment, the construction of routing zones, route discovery based on bordercasting service and routing update. We prove the stabilization property in the inactive environment. In addition, we demonstrate that discovered routes hold the loop freedom and validity in each reachable system state. To present that the formalization is consistent with the informally expressed requirements, we adopt an animator, ProB, to validate our model. Our work provides reference to analyze extensions of the ZRP and other hybrid routing protocols.