O'Reilly logo

VRRP: Increasing Reliability and Failover with the Virtual Router Redundance Protocol by Adnan Adam Onart, Ayikudy Srikanth

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

E.5. Protocol Assertions

Ownership and Priority

For the discussions related to ownership, we introduce a unary predicate:

x is the owner of the virtual router v

and we symbolize this predicate as

O(x).

With our definitions and symbolisms for priority, primary IP address, and ownership at hand, we start our study of assertions related to the ownership within VRRP virtual routers.

A-(1) If a VRRP router x is the owner of the virtual router v, then the priority of x in v has the value 255.
∀x (O(x) → prio(x) = 255)
A-(2) If the priority of a VRRP router x has the priority 255 in the virtual router v, then x is the owner of v.
∀x ( prio(x) = 255 → O(x))

From A-(1) and A-(2) using the equivalence (4), we can obtain the following assertion:

A-(3) ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required