Using Alloy to formally model and reason about an OpenFlow network switch
Kfoury, Assaf J.
MetadataShow full item record
CitationSaber 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
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.