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 条
  • [11] A Sketch-based Network Traffic Analysis Implementation on Commodity OpenFlow Switches
    Liou, Zong-Cheng
    Cheng, Chung-Hsiang
    Wellem, Theophilus
    Shih, Ku-Yeh
    Lai, Yu-Kuen
    2018 ASIA-PACIFIC SIGNAL AND INFORMATION PROCESSING ASSOCIATION ANNUAL SUMMIT AND CONFERENCE (APSIPA ASC), 2018, : 459 - 465
  • [12] Tutorial: Practical Verification of Network Programs
    Foster, Nate
    Guha, Arjun
    Reitblatt, Mark
    Schlesinger, Cole
    2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2013, : 9 - +
  • [13] Energy-efficient operation of a network of OpenFlow switches featuring hardware acceleration and frequency scaling
    Ghiasian, Ali
    Liu, Pengcheng
    Wang, Xiaojun
    Collier, Martin
    TRANSACTIONS ON EMERGING TELECOMMUNICATIONS TECHNOLOGIES, 2019, 30 (06)
  • [14] On Retrieval Order of Statistics Information from OpenFlow Switches to Locate Lossy Links by Network Tomographic Refinement
    Nakamura, Takemi
    Shibata, Masahiro
    Tsuru, Masato
    ADVANCES IN INTELLIGENT NETWORKING AND COLLABORATIVE SYSTEMS, INCOS - 2019, 2020, 1035 : 342 - 351
  • [15] Heuristics for ring network design when several types of switches are available
    Chamberland, S
    Sanso, B
    Marcotte, O
    ICC'97: 1997 IEEE INTERNATIONAL CONFERENCE ON COMMUNICATIONS - TOWARDS THE KNOWLEDGE MILLENNIUM, CONFERENCE RECORD - VOLS 1-3, 1997, : 570 - 574
  • [16] ON THE COMPUTATIONAL-COMPLEXITY OF OPTIMAL SORTING NETWORK VERIFICATION
    PARBERRY, I
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 505 : 252 - 269
  • [17] Fault-Tolerant OpenFlow-based Software Switch Architecture with LINC Switches for a Reliable Network Data Exchange
    Velusamy, Gandhimathi
    Gurkan, Deniz
    Narayan, Sandhya
    Bailey, Stuart
    2014 THIRD GENI RESEARCH AND EDUCATIONAL EXPERIMENT WORKSHOP (GREE), 2014, : 43 - 48
  • [18] Verification Systems and Programs in Regional Television Stations That Are Members of the CIRCOM Network
    Ruas-Araujo, Jose
    Rodriguez-Martelo, Talia
    Maiz-Bar, Carmen
    JOURNALISM AND MEDIA, 2022, 3 (01): : 1 - 12
  • [19] Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic
    Chlipala, Adam
    ACM SIGPLAN NOTICES, 2011, 46 (06) : 234 - 245
  • [20] Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic
    Chlipala, Adam
    PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2011, : 234 - 245
1234