 |
To verify the networks resilience, we proposed a new formal framework.
The resilience verification process verifies reachability, safety and liveness.
To verify the reachability, we checked that a packet P reaches match locations of Switch 1, 2 and 3.
To describe the safety, we show that a packet P does not reach at drop locations of Switch 1 and 2.
Finally, to confirm the liveness, we verify that a packet does not reach at out_port and drop locations of Switch 1 in order to check if a packet drops in Switch 1, the packet does not forward to next Switch.
Additionally, it verifies that different topologies with the same properties both apply the forwarding rule.
|
IEEE/ICACT20220362 Slide.17
[Big Slide]
[YouTube]