DyNetKAT : An Algebra of Dynamic Networks

Lade...
Vorschaubild
Dateien
Zu diesem Dokument gibt es keine Dateien.
Datum
2022
Autor:innen
Hojjat, Hossein
Mousavi, Mohammad Reza
Tunç, Hünkar Can
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Gold
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen 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_10
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)
004 Informatik
Schlagwörter
Software Defined Networks, Dynamic Updates, Dynamic Network Reconfiguration, NetKAT, Process Algebra, Equational Reasoning
Konferenz
25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, 2. Apr. 2022 - 7. Apr. 2022, Munich, Germany
Rezension
undefined / . - undefined, undefined
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Datensätze
Zitieren
ISO 690CALTAIS, 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_10
BibTex
@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>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Ja
Diese Publikation teilen