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.
|Titel||CoNEXT '20 : Proceedings of the 16th International Conference on emerging Networking EXperiments and Technologies|
|Forlag||Association for Computing Machinery|
|Publikationsdato||23 nov. 2020|
|Status||Udgivet - 23 nov. 2020|
|Begivenhed||16th ACM Conference on Emerging Networking Experiment and Technologies, CoNEXT 2020 - Barcelona, Spanien|
Varighed: 1 dec. 2020 → 4 dec. 2020
|Konference||16th ACM Conference on Emerging Networking Experiment and Technologies, CoNEXT 2020|
|Periode||01/12/2020 → 04/12/2020|
Bibliografisk noteFunding Information:
Acknowledgements. We thank Henrik T. Jensen from NORDUnet for providing us with configuration data. The research is supported by DFF project QASNET and WWTF project ICT19-045.
© 2020 ACM.
Copyright 2020 Elsevier B.V., All rights reserved.