Geodesic
A Formal Model and Verification Problems for Software Defined Networks
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 36-51.

Voir la notice de l'article provenant de la source Math-Net.Ru

Software-defined networking (SDN) is an approach to building computer networks that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and flow-table updating was defined in the form of a protocol known as OpenFlow. In this paper we describe an abstract formal model of SDN, introduce a tentative language for specification of SDN forwarding policies, and set up formally model-checking problems for SDN.
Keywords: software defined network, switch, controller, forwarding rule, packet, formal model, specification, model checking. 
@article{MAIS_2013_20_6_a2,
     author = {V. A. Zakharov and R. L. Smelyansky and E. V. Chemeritsky},
     title = {A {Formal} {Model} and {Verification} {Problems} for {Software} {Defined} {Networks}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {36--51},
     publisher = {mathdoc},
     volume = {20},
     number = {6},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a2/}
}
TY  - JOUR
AU  - V. A. Zakharov
AU  - R. L. Smelyansky
AU  - E. V. Chemeritsky
TI  - A Formal Model and Verification Problems for Software Defined Networks
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 36
EP  - 51
VL  - 20
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a2/
LA  - ru
ID  - MAIS_2013_20_6_a2
ER  - 
%0 Journal Article
%A V. A. Zakharov
%A R. L. Smelyansky
%A E. V. Chemeritsky
%T A Formal Model and Verification Problems for Software Defined Networks
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 36-51
%V 20
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a2/
%G ru
%F MAIS_2013_20_6_a2
V. A. Zakharov; R. L. Smelyansky; E. V. Chemeritsky. A Formal Model and Verification Problems for Software Defined Networks. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 36-51. http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a2/

[1] August 5, 2013 www.opennetworking.org

[2] H. Kim, N. Feamster, “Improving network management with software defined networking”, IEEE Communications Magazine, 2013, 114–119 | DOI

[3] E. Al-Shaer, W. Marrero, A. El-Atawy, K. El Badawi, “Network Configuration in a Box: Toward End-to-End Verification of Network Reachability and Security”, 17th IEEE International Conference on Network Protocols, ICNP'09, Princeton, New Jersey, USA, 2009, 123–132

[4] H. Mai, A. Khurshid, R. Agarwal, M. Caesar, R. B. Godfrey, S. T. King, “Debugging of the Data Plane with Anteater”, Proceedings of the ACM SIGCOMM conference, 2011, 290–301

[5] P. Kazemian, G. Varghese, N. McKeown, “Header space analysis: Static checking for networks”, Proceedings of 9-th USENIX Symposium on Networked Systems Design and Implementation, 2012

[6] A. Khurshid, W. Zhou, M. Caesar, P. B. Godfrey, “VeriFlow: Verifying Network-Wide Invariants in Real Time”, Proceedings of International Conference “Hot Topics in Software Defined Networking” (HotSDN), 2012, 49–54

[7] S. Gutz, A. Story, C. Schlesinger, N. Foster, “Splendid isolation: A Slice Abstraction for Software Defined Networks”, Proceedings of International Conference “Hot Topics in Software Defined Networking” (HotSDN), 2012, 79–84

[8] M. Reitblatt, N. Foster, J. Rexford, D. Walker, Consistent updates for software-defined networks: change you can believe in!, HotNets, v. 7, 2011

[9] M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, D. Walker, “Abstractions for Network Update”, Proceedings of ACM SIGCOMM conference, 2012, 323–334

[10] M. Canini, D. Venzano, P. Peresini, D. Kostic, J. Rexford, “A NICE way to Test OpenFlow Applications”, Proceedings of Networked Systems Design and Implementation (April, 2012)

[11] N. Immerman, “Languages that capture complexity classes”, SIAM Journal of Computing, 16:4 (1987), 760–778 | DOI | MR | Zbl

[12] N. Immerman, M. Vardi, “Model checking and transitive closure logic”, Lecture Notes in Computer Science, 1997, 291–302 | DOI

[13] N. Alechina, N. Immerman, “Reachability logic: efficient fragment of transitive closure logic”, Logic Journal of IGPL, 8:3 (2000), 325–337 | MR | Zbl

[14] Z. Galil, “Hierarchies of Complete Problems”, Acta Informatica, 1976, no. 6, 77–88 | MR | Zbl