Computational Verification of Network Programs for Several OpenFlow Switches in Coq

被引：0

作者：

Date, Hiroaki ^{[1
]}

Yoshiura, Noriaki ^{[1
]}

机构：

[1] Saitama Univ, Dept Informat & Comp Sci, Sakura Ku, 255 Shimo Ookubo, Saitama, Japan

来源：

COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2016, PT II | 2016年 / 9787卷

关键词：

D O I：

10.1007/978-3-319-42108-7_17

中图分类号：

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

学科分类号：

0812 ;

摘要：

OpenFlow is a network technology that enables to control network equipment centrally, to realize complicated forwarding of packets and to change network topologies flexibly. In OpenFlow networks, network equipment is separated into OpenFlow switches and OpenFlow controllers. OpenFlow switches do not have controllers that usual network equipment has. OpenFlow controllers control OpenFlow switches. OpenFlow controllers are configured by programs. Therefore, network configurations are realized by software. This kind of software can be created by several kinds of programming languages. NetCore is one of them. The verification method of NetCore programs has been introduced. This method uses Coq, which is a formal proof management system. This method, however, deals with only networks that consist of one OpenFlow switch. This paper proposes a methodology that verifies networks that consist of several OpenFlow switches.

引用

页码：223 / 238

页数：16

共 31 条

[21] Effects of initial settings on computational protein-ligand docking accuracies for several docking programs
Oda, Akifumi
Yamaotsu, Noriyuki
Hirono, Shuichi
Watanabe, Yurie
Fukuyoshi, Shuichi
Takahashi, Ohgi
MOLECULAR SIMULATION, 2015, 41 (10-12) : 1027 - 1034
[22] Compatibility among Electrical Network Component Models of Computational Power System Analysis Programs
Varricchio, S.
Campello, T.
IEEE LATIN AMERICA TRANSACTIONS, 2019, 17 (05) : 833 - 842
[23] Hybrid neural-network/computational programs to the analysis of elastic-plastic structures
Waszczyszyn, Z
Pabisek, E
Mucha, G
IUTAM SYMPOSIUM ON DISCRETIZATION METHODS IN STRUCTURAL MECHANICS, 1999, 68 : 189 - 198
[24] A Comparison of Verification Methods for Neural-Network Controllers Using Mixed-Integer Programs
Dubach, Marcel
Ducard, Guillaume J. J.
2022 7TH INTERNATIONAL CONFERENCE ON ROBOTICS AND AUTOMATION ENGINEERING, ICRAE, 2022, : 43 - 48
[25] SINGLE-EXCEPTION SORTING NETWORKS AND THE COMPUTATIONAL-COMPLEXITY OF OPTIMAL SORTING NETWORK VERIFICATION
PARBERRY, I
MATHEMATICAL SYSTEMS THEORY, 1990, 23 (02): : 81 - 93
[26] Verification of path computational performance in functionally distributed transport networking on next-generation network
Ogawa, Entaro
Aoki, Michihiro
Chaki, Shinichiro
2008 7TH ASIA-PACIFIC SYMPOSIUM ON INFORMATION AND TELECOMMUNICATION TECHNOLOGIES, 2008, : 81 - +
[27] Analysis of effective thermal conductivity of pebble bed by artificial neural network and its computational and experimental verification
Sedani, Chirag
Panchal, Maulik
Tanna, Vipul
Chaudhuri, Paritosh
Gupta, Manoj Kumar
CASE STUDIES IN THERMAL ENGINEERING, 2022, 40
[28] Neural transition system abstraction for neural network dynamical system models and its application to Computational Tree Logic verification
Yang, Yejiang
Wang, Tao
Xiang, Weiming
NEURAL NETWORKS, 2025, 186
[29] Exploring the Molecular Mechanism of Niuxi-Mugua Formula in Treating Coronavirus Disease 2019 via Network Pharmacology, Computational Biology, and Surface Plasmon Resonance Verification
Wang, Wei
Cao, Xu
Cao, Yi-nan
Liu, Lian-lian
Zhang, Shu-ling
Qi, Wen-ying
Zhang, Jia-xin
Yang, Xian-zhao
Li, Xiao-ke
Zao, Xiao-bin
Ye, Yong-an
CURRENT COMPUTER-AIDED DRUG DESIGN, 2024, 20 (07) : 1113 - 1129
[30] Computational exploration of cis-regulatory modules in rhythmic expression data using the "Exploration of Distinctive CREs and CRMs" (EDCC) and "CRM Network Generator" (CNG) programs
Bekiaris, Pavlos Stephanos
Tekath, Tobias
Staiger, Dorothee
Danisman, Selahattin
PLOS ONE, 2018, 13 (01):

← 1 2 3 4 →