Efficient verification of network fault tolerance via counterexample-guided refinement

Nick Giannarakis, Ryan Beckett, Ratul Mahajan, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
EditorsIsil Dillig, Serdar Tasiran
PublisherSpringer Verlag
Pages305-323
Number of pages19
ISBN (Print)9783030255428
DOIs
StatePublished - Jan 1 2019
Event31st International Conference on Computer Aided Verification, CAV 2019 - New York City, United States
Duration: Jul 15 2019Jul 18 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11562 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference31st International Conference on Computer Aided Verification, CAV 2019
CountryUnited States
CityNew York City
Period7/15/197/18/19

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Giannarakis, N., Beckett, R., Mahajan, R., & Walker, D. (2019). Efficient verification of network fault tolerance via counterexample-guided refinement. In I. Dillig, & S. Tasiran (Eds.), Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings (pp. 305-323). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11562 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-25543-5_18