Building Correct SDN-Based Components from a Global Formal Mode
This work addresses correctness issues in SDN component design for networking applications, but it is incremental as it applies an existing formal method (Event-B) to a new domain.
The authors tackled the challenge of designing correct SDN components like controllers and switches by using a formal stepwise approach based on Event-B, resulting in a correct-by-construction method that systematically builds components from a global formal model.
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.