UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Actor-based model checking for Software-Defined Networks

Albert, E; Gómez-Zamalloa, M; Isabel, M; Rubio, A; Sammartino, M; Silva, A; (2021) Actor-based model checking for Software-Defined Networks. Journal of Logical and Algebraic Methods in Programming , 118 , Article 100617. 10.1016/j.jlamp.2020.100617.

[img] Text
2001.10022.pdf - Accepted version
Access restricted to UCL open access staff until 13 October 2021.

Download (756kB)

Abstract

Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behaviour of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and 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 SDNs, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDNs is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks.

Type: Article
Title: Actor-based model checking for Software-Defined Networks
DOI: 10.1016/j.jlamp.2020.100617
Publisher version: https://doi.org/10.1016/j.jlamp.2020.100617
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: Software-Defined Networks, Verification, Concurrency, Actor-based modelling, Model checking
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10117568
Downloads since deposit
1Download
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item