Keeping P4 switches fast and fault-free through automatic verification

Lukács, Dániel and Tejfel, Máté and Pongrácz, Gergely: Keeping P4 switches fast and fault-free through automatic verification. In: Acta cybernetica, (24) 1. pp. 61-81. (2019)

Cikk, tanulmány, mű

Download (854kB) | Preview


The networking dataplane is going through a paradigm shift as softwarization of switches sees an increased pull from the market. Yet, software tooling to support development with these new technologies is still in its infancy. In this work, we introduce a framework for verifying performance requirement conformance of data plane protocols defined in the P4 language . We present a framework that transforms a P4 program in a versatile symbolic formula which can be utilized to answer various performance queries. We represented the system using denotational semantics and it can be easily extended with low-level target-dependent information. We demonstrate the operation of this system on a toy specification.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2019
Volume: 24
Number: 1
ISSN: 0324-721X
Page Range: pp. 61-81
Publisher: University of Szeged, Institute of Informatics
Place of Publication: Szeged
Event Title: Conference of PhD students in computer science (11.) (2018) (Szeged)
Uncontrolled Keywords: Számítástechnika, Informatika
Additional Information: Bibliogr.: p. 80-81. ; összefoglalás angol nyelven
Date Deposited: 2019. Jul. 17. 13:18
Last Modified: 2019. Jul. 17. 13:18

Actions (login required)

View Item View Item