With the increasing scale of communication networks, failures (e.g. link failures) are becoming the norm rather than the exception. Given the critical role such networks play for our digital society, it is important to ensure a reliable and efficient operation of such networks, even in the presence of one or multiple failures.
While several interesting automated approaches to verify and operate networks are emerging, providing an attractive alternative to today’s pragmatic and manual “fix it when it breaks” approach, existing solutions often only provide a limited and inefficient support for reasoning about failure scenarios. In particular, many of these solutions essentially require to test each possible failure scenario one-by-one.
The resulting runtime is exponential in the number of failures, k, which makes this approach not very well-suited for testing large-scale communication networks.
We have developed a tool called P-Rex (CoNEXT) in Python, that has been recently reimplemented in C++ and integrated into the AalWiNes network verification suit developed jointly by researchers at Aalborg University and the University of Vienna. Our tool is currently tailored towards MPLS and Segment Routing (SR) networks, exploiting that their routing and failover behavior is based on stacks of labels.
The tool allows to verify a wide range of important network properties in polynomial time,
parameterized by the maximum number of assumed link failures.