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.
@article{arxiv.1604.00060,
title = {Using Alloy to Formally Model and Reason About an OpenFlow Network Switch},
author = {Saber Mirzaei and Sanaz Bahargam and Richard Skowyra and Assaf Kfoury and Azer Bestavros},
journal= {arXiv preprint arXiv:1604.00060},
year = {2016}
}