License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.OPODIS.2016.18
URN: urn:nbn:de:0030-drops-70870
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7087/
Go to the corresponding LIPIcs Volume Portal

Larsen, Kim G. ; Schmid, Stefan ; Xue, Bingtian

WNetKAT: A Weighted SDN Programming and Verification Language

pdf-format:
LIPIcs-OPODIS-2016-18.pdf (0.6 MB)

Abstract

Programmability and verifiability lie at the heart of the software-defined networking paradigm. While OpenFlow and its match-action concept provide primitive operations to manipulate hardware configurations, over the last years, several more expressive network programming languages have been developed. This paper presents WNetKAT, the first network programming language accounting for the fact that networks are inherently weighted, and communications subject to capacity constraints (e.g., in terms of bandwidth) and costs (e.g., latency or monetary costs). WNetKAT is based on a syntactic and semantic extension of the NetKAT algebra. We demonstrate several relevant applications for WNetKAT, including cost and capacity-aware reachability, as well as quality-of-service and fairness aspects. These applications do not only apply to classic, splittable and unsplittable (s,t)-flows, but also generalize to more complex (and stateful) network functions and service chains. For example, WNetKAT allows to model flows which need to traverse certain waypoint functions, which can change the traffic rate. This paper also shows the relationship between the equivalence problem of WNetKAT and the equivalence problem of the weighted finite automata, which implies undecidability of the former. However, this paper also shows the decidability of whether an expression equals to 0, which is sufficient in many practical scenarios, and we initiate the discussion of decidable subsets of the whole language.

BibTeX - Entry

@InProceedings{larsen_et_al:LIPIcs:2017:7087,
  author =	{Kim G. Larsen and Stefan Schmid and Bingtian Xue},
  title =	{{WNetKAT: A Weighted SDN Programming and Verification Language}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Panagiota Fatourou and Ernesto Jim{\'e}nez and Fernando Pedone},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7087},
  URN =		{urn:nbn:de:0030-drops-70870},
  doi =		{10.4230/LIPIcs.OPODIS.2016.18},
  annote =	{Keywords: Software-Defined Networking, Verification, Reachability, Stateful Processing, Service Chains, Weighted Automata, Decidability, NetKAT}
}

Keywords: Software-Defined Networking, Verification, Reachability, Stateful Processing, Service Chains, Weighted Automata, Decidability, NetKAT
Collection: 20th International Conference on Principles of Distributed Systems (OPODIS 2016)
Issue Date: 2017
Date of publication: 06.04.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI