Abstract
We present an automated what-if analysis tool AalWiNes for MPLS networks which allows us to verify both logical properties (e.g., related to the policy compliance) as well as quantitative properties (e.g., concerning the latency) under multiple link failures. Our tool relies on weighted pushdown automata, a quantitative extension of classic automata theory, and takes into account the actual dataplane configuration, rendering it especially useful for debugging. In particular, our tool collects the different router forwarding tables and then builds a pushdown system, on which quantitative reachability is performed based on an expressive query language. Our experiments show that our tool outperforms state-of-the-art approaches (which until now have been restricted to logical properties) by several orders of magnitude; furthermore, our quantitative extension only entails a moderate overhead in terms of runtime. The tool comes with a platform-independent user interface and is publicly available as open-source, together with all other experimental artefacts.
Original language | English |
---|---|
Title of host publication | CoNEXT '20 : Proceedings of the 16th International Conference on emerging Networking EXperiments and Technologies |
Number of pages | 8 |
Publisher | Association for Computing Machinery |
Publication date | 23 Nov 2020 |
Pages | 474-481 |
ISBN (Print) | 9781450379489 |
DOIs | |
Publication status | Published - 23 Nov 2020 |
Event | 16th ACM Conference on Emerging Networking Experiment and Technologies, CoNEXT 2020 - Barcelona, Spain Duration: 1 Dec 2020 → 4 Dec 2020 |
Conference
Conference | 16th ACM Conference on Emerging Networking Experiment and Technologies, CoNEXT 2020 |
---|---|
Country/Territory | Spain |
City | Barcelona |
Period | 01/12/2020 → 04/12/2020 |
Sponsor | ACM SigComm |
Keywords
- network performance
- network verification
- tools