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 条
  • [1] Computational Verification of Network Programs in Coq
    Stewart, Gordon
    CERTIFIED PROGRAMS AND PROOFS, CPP 2013, 2013, 8307 : 33 - 49
  • [2] Verification of Java programs in Coq
    Department of Computer Science, Royal Holloway University of London, Surrey, United Kingdom
    Comput. Sci. Electron. Eng. Conf., CEEC,
  • [3] A Coq Library for Verification of Concurrent Programs
    Affeldt, Reynald
    Kobayashi, Naoki
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 199 : 17 - 32
  • [4] Modular Verification of Programs with Effects and Effect Handlers in Coq
    Letan, Thomas
    Regis-Gianas, Yann
    Chifflier, Pierre
    Hiet, Guillaume
    FORMAL METHODS, 2018, 10951 : 338 - 354
  • [5] Verification of PCP-Related Computational Reductions in Coq
    Forster, Yannick
    Heiter, Edith
    Smolka, Gert
    INTERACTIVE THEOREM PROVING, ITP 2018, 2018, 10895 : 253 - 269
  • [6] Impact of TCAM size on power efficiency in a network of OpenFlow switches
    Ghiasian, Ali
    IET NETWORKS, 2020, 9 (06) : 367 - 371
  • [7] Verification of computational electromagnetic programs
    Ida, N
    INTERNATIONAL JOURNAL OF NUMERICAL MODELLING-ELECTRONIC NETWORKS DEVICES AND FIELDS, 1996, 9 (1-2) : 159 - 165
  • [8] Analytical Verification of Computational Programs
    Petrenko, Sergey A.
    Stupin, Dmitry D.
    FIFTH INTERNATIONAL CONFERENCE ON ENGINEERING AND TELECOMMUNICATION (ENT-MIPT 2018), 2018, : 172 - 175
  • [9] MapReduce-Based network property verification technique for openFlow network
    Liu Y.
    Lei C.
    Zhang H.
    Yang Y.
    1600, Science Press (53): : 2500 - 2511
  • [10] Virtualizing Packet-Processing Network Functions Over Heterogeneous OpenFlow Switches
    Guimaraes de Oliveira, Joao Victor
    Pereira Bellotti, Pedro Clemente
    de Oliveira, Roberto Massi
    Vieira, Alex Borges
    Chaves, Luciano Jerez
    IEEE TRANSACTIONS ON NETWORK AND SERVICE MANAGEMENT, 2022, 19 (01): : 485 - 496
1234