DyNetKAT: An Algebra of Dynamic Networks

Georgiana Caltais*, Hossein Hojjat, Mohammad Reza Mousavi, Hünkar Can Tunç

*Corresponding author for this work

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

9 Downloads (Pure)

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 and provide an efficient method for reasoning about safety properties. 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 tool prototype.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
EditorsPatricia Bouyer, Lutz Schröder
Number of pages21
PublisherSpringer
Publication date2022
Pages184-204
ISBN (Print)9783030992521
DOIs
Publication statusPublished - 2022
Event25th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 - Munich, Germany
Duration: 4 Apr 20226 Apr 2022

Conference

Conference25th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022
Country/TerritoryGermany
CityMunich
Period04/04/202206/04/2022
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13242 LNCS
ISSN0302-9743

Keywords

  • Dynamic Network Reconfiguration
  • Dynamic Updates
  • Equational Reasoning
  • NetKAT
  • Process Algebra
  • Software Defined Networks

Fingerprint

Dive into the research topics of 'DyNetKAT: An Algebra of Dynamic Networks'. Together they form a unique fingerprint.

Cite this