Skip to main content

Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement

Author(s): Giannarakis, Nick; Beckett, Ryan; Mahajan, Ratul; Walker, David

To refer to this page use:
Abstract: We show how to verify that large data center networks satisfy key properties such as all-pairs reachability under a bounded number of faults. To scale the analysis, we develop algorithms that identify network symmetries and compute small abstract networks from large concrete ones. Using counter-example guided abstraction refinement, we successively refine the computed abstractions until the given property may be verified. The soundness of our approach relies on a novel notion of network approximation: routing paths in the concrete network are not precisely simulated by those in the abstract network but are guaranteed to be “at least as good.” We implement our algorithms in a tool called Origami and use them to verify reachability under faults for standard data center topologies. We find that Origami computes abstract networks with 1–3 orders of magnitude fewer edges, which makes it possible to verify large networks that are out of reach of existing techniques.
Publication Date: 2019
Citation: Giannarakis, Nick, Ryan Beckett, Ratul Mahajan, and David Walker. "Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement." In International Conference on Computer Aided Verification (2019): pp. 305-323. doi:10.1007/978-3-030-25543-5_18
DOI: 10.1007/978-3-030-25543-5_18
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 305 - 323
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Computer Aided Verification
Version: Final published version. This is an open access article.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.