Concurrent NetKAT with Ports

ACM/SIGAPP Symposium on Applied Computing (SAC), pp. 1722–1730

Abstract

NetKAT is a powerful model extending Kleene algebra with tests (KAT) to programming networks. It supports the specification and reasoning about software-defined networks via automata-based operational semantics. This paper extends the NetKAT automata model to support concurrency using shared ports for communication and synchronization. We first extend the language of NetKAT protocols with communication actions and a parallel operator and give a closed and an open semantics using NetKAT automata. We show that NetKAT automata with an open semantics can be used as a model of the coordination language Reo via symbolic constraint automata.

Authors 2

1. Hui Feng Aachen Leiden Institute of Advanced Computer Science

   Leiden University

   Affiliation as printed

   Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands

2. Marcello Bonsangue Aachen Leiden Institute of Advanced Computer Science

   Leiden University

   Affiliation as printed

   Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands