Using Alloy to formally model and reason about an OpenFlow network switch
Files
First author draft
Date
2016
DOI
Authors
Mirzaei, Saber
Bahargam, Sanaz
Skowyra, Richard
Bestavros, Azer
Kfoury, Assaf J.
Version
OA Version
Citation
Saber Mirzaei, Sanaz Bahargam, Richard Skowyra, Assaf J Kfoury, Azer Bestavros. 2016. "Using Alloy to formally model and reason about an OpenFlow network switch.." CoRR, Volume abs/1604.00060
Abstract
Openflow provides a standard interface for partitioning a network into a data plane and a programmatic control plane. While providing easy network reconfiguration, Openflow introduces the potential for programming bugs, causing network deficiency. To study the behavior of OpenFlow switchs, we used Alloy to create a software abstraction, describing the internal state of a network and its OpenFlow switches. Hence, this work is an attempt to model the static and dynamic behaviour of networks configured using OpenFlow switches.