PDNet: A Programming Language for Software-Defined Networks with VLAN

Shuangqing Xiang*, Marcello Bonsangue, Huibiao Zhu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

Abstract

Software-Defined Networking (SDN) is an emerging networking paradigm, which separates the network’s control logic from the underlying routers and switches, providing the ability to program network, simplifying network management and creating an environment for network evolution. NetKAT is a domain-specific language for specifying and verifying packet-processing functions in software-defined networks (SDNs). This paper proposes a more powerful programming language, PDNet, extending NetKAT to specify the behaviors of SDNs that support virtual local area network (VLAN) tags. We present the operational semantics of PDNet in terms of automata and a syntactic derivatives. When comparing PDNet and NetKAT we show that PDNet is strictly more expressive than NetKAT. As expected, we also show that PDNet is as expressive as NetKAT when describing SDNs without VLAN.

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
EditorsYamine Ait-Ameur, Shengchao Qin
PublisherSpringer
Pages203-218
Number of pages16
ISBN (Print)9783030324087
DOIs
StatePublished - 2019
Event21st International Conference on Formal Engineering Methods, ICFEM 2019 - Shenzhen, China
Duration: 5 Nov 20199 Nov 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11852 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Formal Engineering Methods, ICFEM 2019
Country/TerritoryChina
CityShenzhen
Period5/11/199/11/19

Keywords

  • NetKAT
  • Pushdown systems
  • Software Defined Networks
  • VLAN

Fingerprint

Dive into the research topics of 'PDNet: A Programming Language for Software-Defined Networks with VLAN'. Together they form a unique fingerprint.

Cite this