Virual Oral Presentation Slide by Slide

IEEE/ICACT20220362 Slide.13        [Big Slide]       [YouTube]	Oral Presentation
	We express that some state satisfying P should be reachable using the path formula E<>P. The following formulae verify that a packet reaches the same destination for two different topologies: ˇ°E<> sw1.match && sw2.match && sw3.match ˇ° First Figure show that verification results is ˇ°Property is satisfied.ˇ± In the other words, a packet P on a path reaches match locations of Switch 1, 2 and 3 on each topology in order to match the rule on flow table. Next Figure is also verification results for ˇ°Property is satisfied.ˇ± It means that a packet P on a path reaches send location of Host1 and match location of Switch 4 on each topology. This shows that whether the packet sent from Host 1 matches Switch 4.

[Go to Next Slide]

Select Voice: Virtual Oral Presentation!!