Latte
- 5 March 2021
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGMETRICS Performance Evaluation Review
- Vol. 48 (3), 14-26
- https://doi.org/10.1145/3453953.3453957
Abstract
Emerging software-defined and programmable networking technologies enable more adaptive communication infrastructures. However, leveraging these flexibilities and operating networks more adaptively is challenging, as the underlying infrastructure remains a complex distributed system that is a subject to delays, and as consistency properties need to be preserved transiently, even during network reconfiguration. Motivated by these challenges, we propose Latte, an automated approach to minimize the latency of network update schedules by avoiding unnecessary waiting times and exploiting concurrency, while at the same time provably ensuring a wide range of fundamental consistency properties like waypoint enforcement. To enable automated reasoning about the performance and consistency of software-defined networks during an update, we introduce the model of timed-arc colored Petri nets: an extension of Petri nets which allows us to account for time aspects in asynchronous networks, including characteristic timing behaviors, modeled as timed and colored tokens. This novel formalism may be of independent interest. Latte relies on an efficient translation of specific network update problems into timed-arc colored Petri nets. We show that the constructed nets can be analyzed efficiently via their unfolding into existing timed-arc Petri nets. We integrate Latte into the state-of-the-art model checking tool TAPAAL, and find that in many cases, we are able to reduce the latency of network updates by 90% or more.Keywords
This publication has 21 references indexed in Scilit:
- Network security analyzing and modeling based on Petri net and Attack tree for SDNPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2016
- Network service chaining with optimized network function embedding supporting service decompositionsComputer Networks, 2015
- Efficient synthesis of network updatesPublished by Association for Computing Machinery (ACM) ,2015
- A distributed and robust SDN control plane for transactional network updatesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2015
- zUpdatePublished by Association for Computing Machinery (ACM) ,2013
- Verification of Liveness Properties on Closed Timed-Arc Petri NetsLecture Notes in Computer Science, 2013
- A Forward Reachability Algorithm for Bounded Timed-Arc Petri NetsElectronic Proceedings in Theoretical Computer Science, 2012
- Abstractions for network updateACM SIGCOMM Computer Communication Review, 2012
- TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri NetsLecture Notes in Computer Science, 2012
- Timed Petri nets definitions, properties, and applicationsMicroelectronics Reliability, 1991