DyNetKAT : An Algebra of Dynamic Networks
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Sammlungen
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
CALTAIS, Georgiana, Hossein HOJJAT, Mohammad Reza MOUSAVI, Hünkar Can TUNÇ, 2022. DyNetKAT : An Algebra of Dynamic Networks. 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022. Munich, Germany, 2. Apr. 2022 - 7. Apr. 2022. In: BOUYER, Patricia, ed., Lutz SCHRÖDER, ed.. Foundations 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, Munich, Germany, April 2–7, 2022, Proceedings. Cham: Springer International Publishing, 2022, pp. 184-204. Lecture Notes in Computer Science. 13242. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-99252-1. Available under: doi: 10.1007/978-3-030-99253-8_10BibTex
@inproceedings{Caltais2022DyNet-57472, year={2022}, doi={10.1007/978-3-030-99253-8_10}, title={DyNetKAT : An Algebra of Dynamic Networks}, number={13242}, isbn={978-3-030-99252-1}, issn={0302-9743}, publisher={Springer International Publishing}, address={Cham}, series={Lecture Notes in Computer Science}, booktitle={Foundations 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, Munich, Germany, April 2–7, 2022, Proceedings}, pages={184--204}, editor={Bouyer, Patricia and Schröder, Lutz}, author={Caltais, Georgiana and Hojjat, Hossein and Mousavi, Mohammad Reza and Tunç, Hünkar Can} }
RDF
<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/57472"> <dc:contributor>Mousavi, Mohammad Reza</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/"/> <dc:creator>Caltais, Georgiana</dc:creator> <dc:creator>Hojjat, Hossein</dc:creator> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/57472"/> <dc:rights>Attribution 4.0 International</dc:rights> <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by/4.0/"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2022-05-09T10:32:57Z</dcterms:available> <dcterms:issued>2022</dcterms:issued> <dc:contributor>Hojjat, Hossein</dc:contributor> <dc:contributor>Tunç, Hünkar Can</dc:contributor> <dcterms:title>DyNetKAT : An Algebra of Dynamic Networks</dcterms:title> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2022-05-09T10:32:57Z</dc:date> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>Tunç, Hünkar Can</dc:creator> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dc:creator>Mousavi, Mohammad Reza</dc:creator> <dc:language>eng</dc:language> <dc:contributor>Caltais, Georgiana</dc:contributor> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dcterms:abstract xml:lang="eng">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.</dcterms:abstract> </rdf:Description> </rdf:RDF>