Automatic Synthesis of Transiently Correct Network Updates via Petri Games

As software-defined networking (SDN) is growing increasingly common within the networking industry, the lack of accessible and reliable automated methods for updating network configurations becomes more apparent. Any computer network is a complex distributed system and changes to its configuration may result in policy violations during the transient phase when the individual routers update their forwarding tables. We present an approach for automatic synthesis of update sequences that ensures correct network functionality throughout the entire update phase. Our approach is based on a novel translation of the update synthesis problem into a Petri game and it is implemented on top of the open-source model checker TAPAAL. On a large benchmark of synthetic and real-world network topologies, we document the efficiency of our approach and compare its performance with state-of-the-art tool NetSynth. Our experiments show that for several networks with up to thousands of nodes, we are able to outperform NetSynth’s update schedule generation.