Building Correct SDN-Based Components from a Global Formal Mode
Christian Attiogb\'e

TL;DR
This paper introduces a formal, stepwise method using Event-B to model and systematically build correct SDN components, ensuring they meet specified properties and improving reliability.
Contribution
It presents the first state-based formal approach with Event-B for correct-by-construction SDN components from a global model.
Findings
Successful modeling of SDN system with Event-B
Systematic construction of correct SDN components
Validation of the approach through experiments
Abstract
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.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware-Defined Networks and 5G · Software Testing and Debugging Techniques · Model-Driven Software Engineering Techniques
