FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
SDN-Actors: Modeling and Verification of SDN Programs

Authors: Elvira Albert, Miguel Gomez-Zamalloa, Albert Rubio, Matteo Sammartino and Alexandra Silva

Paper Information

Title:SDN-Actors: Modeling and Verification of SDN Programs
Authors:Elvira Albert, Miguel Gomez-Zamalloa, Albert Rubio, Matteo Sammartino and Alexandra Silva
Proceedings:FM FMComplete
Editors: Jan Peleska, Klaus Havelund and Bill Roscoe
Keywords:actors, distributed concurrent systems, software-defined networks, model checking, OpenFlow, partial order reduction
Abstract:

ABSTRACT. Software-Defined Networking (SDN) is a recent networking paradigm that has become increasingly popular in the last decade. It gives unprecedented control over the global behavior of the network and provides a new opportunity for formal methods. Much work has appeared in the last few years on providing bridges between SDN and verification. This paper advances this research line and provides a link between SDN and traditional work on formal methods for verification of distributed software---actor-based modelling. We show how SDN programs can be seamlessly modelled using actors, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops.

Pages:18
Talk:Jul 17 17:00 (Session 122B)
Paper: