Albert, E;
Gómez-Zamalloa, M;
Rubio, A;
Sammartino, M;
Silva, A;
(2018)
SDN-Actors: Modeling and Verification of SDN Programs.
In: Havelund, K and Peleska, J and Roscoe, B and de Vink, E, (eds.)
Proceedings of International Symposium on Formal Methods 2018.
(pp. pp. 550-567).
Springer Nature: Cham, Switzerland.
Preview |
Text
Silva_SDN-Actors. Modeling and verification of SDN programs_AAM.pdf - Accepted Version Download (424kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | SDN-Actors: Modeling and Verification of SDN Programs |
| Event: | International Symposium on Formal Methods |
| Location: | Oxford, UK |
| Dates: | 15th-17th July 2018 |
| ISBN: | 0302-9743 |
| ISBN-13: | 978-3-319-95581-0 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-319-95582-7_33 |
| Publisher version: | http://doi.org/10.1007/978-3-319-95582-7_33 |
| 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: | artificial intelligence, data security, formal logic, formal methods, formal verifications, model checking, program debugging, robots, safety critical systems, satisfiability, security systems, software engineering, software evaluation, specifications, temporal logic, verification |
| UCL classification: | UCL 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/10060372 |
Archive Staff Only
 |
View Item |
