A Survey on Network Verification and Testing With Formal Methods: Approaches and Challenges

被引:33
作者
Li, Yahui [1 ]
Yin, Xia [1 ]
Wang, Zhiliang [2 ]
Yao, Jiangyuan [3 ]
Shi, Xingang [2 ]
Wu, Jianping [1 ]
Zhang, Han [4 ]
Wang, Qing [1 ]
机构
[1] Tsinghua Univ, Tsinghua Natl Lab Informat Sci & Technol, Dept Comp Sci & Technol, Beijing 100084, Peoples R China
[2] Tsinghua Univ, Tsinghua Natl Lab Informat Sci & Technol, Inst Network Sci & Cyberspace, Beijing 100084, Peoples R China
[3] Hainan Univ, Coll Informat Sci & Technol, Haikou 570228, Hainan, Peoples R China
[4] Beihang Univ, Sch Cyber Sci & Technol, Beijing 100191, Peoples R China
基金
中国国家自然科学基金; 国家高技术研究发展计划(863计划);
关键词
Network verification; network testing; formal methods; network reliability; software-defined network; SOFTWARE-DEFINED NETWORKING; SYMBOLIC MODEL CHECKING; TEMPORAL LOGIC; SATISFIABILITY; EXECUTION; PROGRAM; SYSTEM; BOX;
D O I
10.1109/COMST.2018.2868050
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Networks have grown increasingly complicated. Violations of intended policies can compromise network availability and network reliability. Network operators need to ensure that their policies are correctly implemented. This has inspired a research field, network verification and testing, that enables users to automatically detect bugs and systematically reason their network. Furthermore, techniques ranging from formal modeling to verification and testing have been applied to help operators build reliable systems in electronic design automation and software. Inspired by its success, network verification has recently seen increased attention in the academic and industrial communities. As an area of current interest, it is an interdisciplinary subject (with fields including formal methods, mathematical logic, programming languages, and networks), making it daunting for a nonprofessional. We perform a comprehensive survey on well-developed methodologies and tools for data plane verification, control plane verification, data plane testing and control plane testing. This survey also provides lessons gained from existing solutions and a perspective of future research developments.
引用
收藏
页码:940 / 969
页数:30
相关论文
共 177 条
[1]  
Al-Shaer E., 2010, P 3 ACM WORKSHOP ASS, P37, DOI DOI 10.1145/1866898.1866905
[2]   Network Configuration in A Box: Towards End-to-End Verification of Network Reachability and Security [J].
Al-Shaer, Ehab ;
Marrero, Will ;
El-Atawy, Adel ;
ElBadawi, Khalid .
2009 17TH IEEE INTERNATIONAL CONFERENCE ON NETWORK PROTOCOLS (ICNP 2009), 2009, :123-+
[3]  
Al-Shaer ES, 2004, IEEE INFOCOM SER, P2605
[4]   A Survey of Securing Networks Using Software Defined Networking [J].
Ali, Syed Taha ;
Sivaraman, Vijay ;
Radford, Adam ;
Jha, Sanjay .
IEEE TRANSACTIONS ON RELIABILITY, 2015, 64 (03) :1086-1097
[5]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[6]   NetKAT: Semantic Foundations for Networks [J].
Anderson, Carolyn Jane ;
Foster, Nate ;
Guha, Arjun ;
Jeannin, Jean-Baptiste ;
Kozen, Dexter ;
Schlesinger, Cole ;
Walker, David .
ACM SIGPLAN NOTICES, 2014, 49 (01) :113-126
[7]  
[Anonymous], SATISFIABILITY MODUL
[8]  
[Anonymous], 2014, IEEE IFIP NETW OPER
[9]  
[Anonymous], 1654 RFC INT ENG TAS
[10]  
[Anonymous], OPENFLOW SWITCH SPEC