Automated Synthesis of Reactive Controllers for Software-Defined Networks

With the tremendous growth of the Internet and the emerging software-defined networks, there is an increasing need for rigorous and scalable network management methods and tool support. This paper proposes a synthesis approach for managing software-defined networks. We formulate the construction of network control logic as a reactive synthesis problem which is solvable with existing synthesis tools. The key idea is to synthesize a strategy that manages control logic in response to network changes while satisfying some network-wide specification. Finally, we investigate network abstractions for scalability. For large networks, instead of synthesizing control logic directly, we use its abstraction-a smaller network that simulates its behavior-for synthesis, and then implement the synthesized control on the original network while preserving the correctness. By using the so-called simulation relations, we also prove the soundness of this abstraction-based synthesis approach.