Formal Verification and Testing of Data Plane in Software-Defined Networks: A Survey

Software-defined network (SDN) separates the control plane and the data plane, which provides the programmability of the network and is widely deployed in data center networks. As the foundation of SDN, the data plane needs to be fully verified and tested to ensure its correctness and reliability. At present, formal verification and testing methods have been applied to SDN networks. The goals of verification and testing are to find the design defects and the implementation errors of the data plane, respectively. In this paper, we conduct a survey of the state-of-art methods and tools of formal verification and formal testing for SDN data plane. According to support for online verification, the related works of formal verification for the data plane fall into static verification and real-time verification. According to the requirement of source code, the existing works of formal testing for the data plane fall into white-box testing and black-box testing. Based on the state-of-art approaches of verification and testing, we also discuss the research trends of verification and testing for SDN data plane, such as artificial intelligence (AI)-based model construct and property definition, and scalable support for the stateful data plane.