DyNetKAT: an algebra of dynamic networks

DOI10.1007/978-3-030-99253-8_10MaRDI QIDQ6181928zbMATH OpenOpenAlexFDO

Authors Georgiana Caltais, Hossein Hojjat, Mohammadreza Mousavi, Hünkar Can Tunç

Publication date 23 January 2024

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2102.10035

zbMATH Keywords

dynamic network reconfigurationdynamic updatesequational reasoningNetKATprocess algebrasoftware defined networks

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Abstract: 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.

Recommendations

• Towards an analysis of dynamic gossip in Net\textsc{kat}
• NetKAT -- a formal system for the verification of networks
• Netkat, semantic foundations for networks
• Probabilistic NetKAT
• A coalgebraic decision procedure for NetKAT

Cites work

• A coalgebraic decision procedure for NetKAT
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• scientific article; zbMATH DE number 1407502 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Modular structural operational semantics
• Netkat, semantic foundations for networks
• Notions of bisimulation and congruence formats for SOS with data
• Optimal consistent network updates in polynomial time
• Probabilistic NetKAT
• Process Algebra
• Turning SOS rules into equations

Cited in

(1)

• Concurrent NetKAT. Modeling and analyzing stateful, concurrent networks

This page was built for publication: DyNetKAT: an algebra of dynamic networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6181928)