Automatic verification of MPLS networks

Jiri Srba
SpeakerJiri Srba
TrackTrack 1
DescriptionI shall 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 the theory of 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.

Joint work with: P.G. Jensen, D. Kristiansen, S. Schmid, M.K. Schou, B.C. Schrenk, J. Vanerio and I. van Duijn.

Presentation documents

All talks