@inproceedings{9cbd00798d974d2db7c78c12fa93683e,
title = "A Model Checking Based Approach for Detecting SDN Races",
abstract = "The paper is devoted to the verification of Software Defined Networking (SDN) components and their compositions. We focus on the interaction between three basic entities, an application, a controller, and a switch. When the application submits a request to the controller, containing a set of rules to configure, these rules are expected to be {\textquoteleft}pushed{\textquoteright} and correctly applied by the switch of interest. However, this is not always the case, and one of the reasons is the presence of races or concurrency issues in SDN components and related interfaces. We propose a model checking based approach for deriving test sequences that can identify SDN races. The test generation strategy is based on model checking, and related formal verification is performed with the use of extended automata specifying the behavior of the components of interest; Linear Temporal Logic (LTL) formulas are utilized to express the properties to check. We generalize the races of interest and propose an approach for deriving the corresponding LTL formulas that are later used for verifiation. The Spin model checker is used for that purpose and thus, Promela specifications for interacting components are also provided; those are: the ONOS REST API, the ONOS controller and an OpenFlow Switch. An experimental evaluation with the aforementioned components showcases the existence of race conditions in their compositions.",
keywords = "Controller, Races, Software Defined Networking (SDN), Switch, Testing, Verification",
author = "Evgenii Vinarskii and Jorge L{\'o}pez and Natalia Kushik and Nina Yevtushenko and Djamal Zeghlache",
note = "Publisher Copyright: {\textcopyright} 2019, IFIP International Federation for Information Processing.; 31st IFIP International Conference on Testing Software and Systems, ICTSS 2019 ; Conference date: 15-10-2019 Through 17-10-2019",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-31280-0\_12",
language = "English",
isbn = "9783030312794",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "194--211",
editor = "Christophe Gaston and Nikolai Kosmatov and \{Le Gall\}, Pascale",
booktitle = "Testing Software and Systems - 31st IFIP WG 6.1 International Conference, ICTSS 2019, Proceedings",
}