Reo is a compositional coordination language for component connectors with a formal semantics based on automata. In this paper, we propose a formal model of software defined networks (SDNs) based on Reo where declarative constructs comprising of basic Reo primitives compose to specify descriptive models of both data and control planes of SDNs. We first describe the model of an SDN switch which can be compactly represented as a single state constraint automaton with a memory storing its flow table. A full network can then be compositionally constructed by composing the switches with basic communication channels. The reactive and proactive behaviour of the controllers in the control plane of an SDN can also be modelled by Reo connectors, which can compose the connectors representing data plane. The resulting model is suitable for testing, simulation, visualization, verification, and ultimately compilation into SDN switch code using the standard tools already available for Reo.

, , , , ,
doi.org/10.1007/978-3-030-32409-4_5
Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence
International Conference on Formal Engineering Methods
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Feng, H., Arbab, F., & Bonsangue, M. (2019). A Reo model of Software Defined Networks. In Formal Methods and Software Engineering (pp. 69–85). doi:10.1007/978-3-030-32409-4_5