Research Directions in Formal Verification of Network Configurations Toward Verification of Mobile Networks

被引：0

作者：

Sakurada, Hideki ^{[1
,2
]}

Sakurai, Kouichi ^{[2
,3
]}

机构：

[1] NTT Corp, Tokyo, Japan

[2] Kyushu Univ, Fukuoka, Japan

[3] Adv Telecommun Res Inst Int, Kyoto, Japan

来源：

MOBILE INTERNET SECURITY, MOBISEC 2023 | 2024年 / 2095卷

关键词：

formal verification; network configuration; software-defined networking;

D O I：

10.1007/978-981-97-4465-7_18

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper reviews current research trends in the formal verification of computer network configurations, specifically focusing on formal verification for software-defined networking (SDN). We explore the challenges encountered when applying formal verification, comparing its application to pre-SDN network verification efforts. Additionally, we discuss the potential application of formal verification in mobile networks. We first provide an overview of research on the formal verification of virtual LAN (VLAN) configurations, which predates the emergence of SDN. We next illustrate SDN and existing research applying formal verification to SDN. Finally, we briefly examine potential scenarios for applying formal verification to mobile networks.

引用

页码：248 / 259

页数：12

共 50 条

[31] The Research on Formal Verification of CPU Structure Based on Theorem Proving [J].

Yang, Hongwei ;

Ma, Dianfu .

PROCEEDINGS OF 2019 IEEE 10TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2019), 2019, :139-143

[32] Research on Formal Modeling and Verification of on-board ATP System [J].

Chen, Caiyun ;

Luo, Qing ;

Zhang, Fang ;

Wang, Daqing ;

Xue, Xiaoping .

PROCEEDINGS OF 2013 INTERNATIONAL CONFERENCE ON INFORMATION SCIENCE AND COMPUTER APPLICATIONS (ICSA 2013), 2013, 92 :27-32

[33] Formal Verification of Cloud and Fog Systems: A Review and Research Challenges [J].

Fakhfakh, Fairouz ;

Kallel, Slim ;

Cheikhrouhou, Saoussen .

JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2021, 27 (04) :341-363

[34] Towards Formal Verification of Neural Networks: A Temporal Logic Based Framework [J].

Wang, Xiaobing ;

Yang, Kun ;

Wang, Yanmei ;

Zhao, Liang ;

Shu, Xinfeng .

STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD (SOFL+MSVL 2019), 2020, 12028 :73-87

[35] Formal Verification of Neural Networks: A "Step Zero" Approach for Vehicle Detection [J].

Guidotti, Dario ;

Pandolfo, Laura ;

Pulina, Luca .

ADVANCES AND TRENDS IN ARTIFICIAL INTELLIGENCE: THEORY AND APPLICATIONS, IEA-AIE 2024, 2024, 14748 :297-309

[36] Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study [J].

Webster, Matt ;

Dixon, Clare ;

Fisher, Michael ;

Salem, Maha ;

Saunders, Joe ;

Koay, Kheng Lee ;

Dautenhahn, Kerstin ;

Saez-Pons, Joan .

IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS, 2016, 46 (02) :186-196

[37] Toward Formal Data Set Verification for Building Effective Machine Learning Models [J].

Lopez, Jorge ;

Labonne, Maxime ;

Poletti, Claude .

PROCEEDINGS OF THE 13TH INTERNATIONAL JOINT CONFERENCE ON KNOWLEDGE DISCOVERY, KNOWLEDGE ENGINEERING AND KNOWLEDGE MANAGEMENT (KDIR), VOL 1:, 2021, :249-256

[38] FORMAL CO-VERIFICATION OF LOCAL INTERCONNECT NETWORK MASTER NODE [J].

Nguyen Duc Minh .

2013 INTERNATIONAL CONFERENCE ON ADVANCED TECHNOLOGIES FOR COMMUNICATIONS (ATC), 2013, :355-359

[39] Formal Verification of Neural Network Controllers for Collision-Free Flight [J].

Genin, Daniel ;

Papusha, Ivan ;

Brule, Joshua ;

Young, Tyler ;

Mullins, Galen ;

Kouskoulas, Yanni ;

Wu, Rosa ;

Schmidt, Aurora .

SOFTWARE VERIFICATION, 2022, 13124 :147-164

[40] Linking Simulation with Formal Verification and Modeling of Wireless Sensor Network in TLA [J].

Martyna, Jerzy .

COMPUTER NETWORKS, 2010, 79 :131-140

← 1 2 3 4 5 →