Is your OpenFlow application correct?

OpenFlow enables third-party programs to dynamically reconfigure the network by installing, modifying and deleting packet processing rules as well as collecting statistics from individual switches. But how can we know if such programs are correct? While the abstraction of a logically-centralized network controller can ease their development, this abstraction does not remove the complexity of the underlying distributed system. For instance, small differences in packet header fields or packet orderings can "tickle" subtle bugs [1]. We argue for the need of thorough, automatic testing of OpenFlow applications. In this paper, we describe our preliminary experiences with taking two state-of-the-art model checkers (SPIN and Java PathFinder) and applying them "as is" for checking an example of OpenFlow program: a MAC-learning switch application. Overall, the preliminary results we report suggest that these tools taken out-of-the-box have difficulties to cope with the state-space explosion that arises in model checking OpenFlow networks.