2021/02/19 by Georgiana Caltais, Caltais, Georgiana, Hossein Hojjat +5
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Networking and Internet Architecture (cs.NI) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2102.10035
openalex publication_date 2021/02/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory to provide an efficient reasoning method about safety properties for dynamic networks. We implement our equational theory in DyNetiKAT -- a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our initial tool prototype.