Is your OpenFlow application correct?

Peter Perešíni*, Marco Canini

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM CoNEXT Student Workshop, CoNEXT 2011
StatePublished - 2011
Externally publishedYes
Event2011 ACM CoNext Student Workshop, CoNEXT 2011 - Tokyo, Japan
Duration: Dec 6 2011Dec 6 2011

Publication series

NameProceedings of the ACM CoNEXT Student Workshop, CoNEXT 2011


Other2011 ACM CoNext Student Workshop, CoNEXT 2011

ASJC Scopus subject areas

  • Computer Networks and Communications


Dive into the research topics of 'Is your OpenFlow application correct?'. Together they form a unique fingerprint.

Cite this