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