Premium
Formal modeling and verification of software‐defined networks: A survey
Author(s) -
Shukla Nitin,
Pandey Mayank,
Srivastava Shashank
Publication year - 2019
Publication title -
international journal of network management
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.373
H-Index - 28
eISSN - 1099-1190
pISSN - 1055-7148
DOI - 10.1002/nem.2082
Subject(s) - computer science , flexibility (engineering) , orchestration , software deployment , forwarding plane , software defined networking , distributed computing , context (archaeology) , software , software engineering , network management , computer network , operating system , art , musical , statistics , paleontology , mathematics , network packet , visual arts , biology
Summary 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.