 |
The formal framework in Figure consists of controllers, switches, and hosts at UPPAAL modeling. Simulations can be used to confirm that the model operates as intended. In particular, the safety, reachability, and liveness at Properties of the system can be verified. As a result of this verification process, users receive either a Satisfied or Not Satisfied message. In the framework, the model and its properties are modified through feedback, and then verification is run again.
As an application of the framework, the topology is modeled with SDN components, including the hosts, controller, and switches. Furthermore, the network configuration can be changed through the alternation of the topology, depending on various network conditions such as node failure, QoS requirements, and cost reduction. Each SDN is modeled with two different topologies. The forwarding rule must be applied well, even though the network changes to a different topology. The verification properties are examined for each topology in terms of safety, liveness, and reachability. The maintenance of the forwarding rule is confirmed by verifying the same properties in different topologies. The results of ¡°Not Satisfied¡± or ¡°Satisfied¡± are displayed after the properties are input to UPPAAL Verify, the middle part of Figure 2. It can be confirmed that the same forwarding rule is applied if Satisfied is obtained as a result after two SDNs with different topologies are modeled and verified for the same property.
|
IEEE/ICACT20220362 Slide.06
[Big Slide]
[YouTube]