  Software Defined Networking (SDN) brings flexibility in the construction and
managment of distributed applications by reducing the constraints imposed by
physical networks and by moving the control of networks closer to the
applications. However mastering SDN still poses numerous challenges among which
the design of correct SDN components (more specifically controller and
switches). In this work we use a formal stepwise approach to model and reason
on SDN. Although formal approaches have already been used in this area, this
contribution is the first state-based approach; it is based on the Event-B
formal method, and it enables a correct-by-construction of SDN components. We
provide the steps to build, using several refinements, a global formal model of
a SDN system; correct SDN components are then systematically built from the
global formal model satisfying the desired properties. Event-B is used to
experiment the approach.
