Using alloy to formally model and reason about an OpenFlow network switch
Date
2013-07-10
DOI
Authors
Mirzaei, Saber
Bahargam, Sanaz
Skowyra, Richard
Kfoury, Assaf
Bestavros, Azer
Version
OA Version
Citation
Mirzaei, Saber; Bahargam, Sanaz; Skowyra, Richard; Kfoury, Assaf; Bestavros, Azer. "Using Alloy to Formally Model and Reason About an OpenFlow Network Switch", Technical Report BUCS-TR-2013-007, Computer Science Department, Boston University, July 10, 2013. [Available from: http://hdl.handle.net/2144/11416]
Abstract
Openflow provides a standard interface for separating a network into a data plane and a programmatic control plane. This enables easy network reconfiguration, but introduces the potential for programming bugs to cause network effects. To study OpenFlow switch behavior, we used Alloy to create a software abstraction describing the internal state of a network and its OpenFlow switches. This work is an attempt to model the static and dynamic behaviour a network built using OpenFlow switches.