Formal modeling and verification of software‐defined networks: A survey

Unlike traditional networking devices, control and management plane are decoupled from data plane in software‐defined networks (SDN). The logically centralized control and management plane facilitate dynamic orchestration of network resources, services, and policies by writing software programs. This provides much needed flexibility and programmability where networking rules and policies can be modified dynamically depending upon the application context. As the operation of network services entirely depends on a program, a small fault may induce several issues which can adversely affect the expected behavior of the network. Formal modeling and verification help in catching inconsistencies and existence of errors prior to the deployment of the programs that control the behavior of a network. In this paper, we provide a comprehensive survey of tools and techniques available in the literature for formal modeling and verification of SDN. These tools and techniques are classified based on their types, the components of SDN where they can be applied, and the design and development phase when they are utilized. In particular, their respective benefits and limitations are discussed in terms of ease of use, interfaces, and the ability to capture and verify intended network properties.