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. Acta cybernetica, (24) 1. pp. 61-81. (2019)

[img] Cikk, tanulmány, mű

Download (854kB)


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
Event Title: Conference of PhD students in computer science (11.) (2018) (Szeged)
Journal or Publication Title: Acta cybernetica
Date: 2019
Volume: 24
Number: 1
Page Range: pp. 61-81
ISSN: 0324-721X
Publisher: University of Szeged, Institute of Informatics
Place of Publication: 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