Efficient verification of network fault tolerance via counterexample-guided refinement

Nick Giannarakis, Ryan Beckett, Ratul Mahajan, David P. 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

Fault tolerance
Fault Tolerance
Counterexample
Refinement
Concretes
Topology
Data Center
Verify
Reachability
Fault
Large Data
Soundness
Routing
Symmetry
Path
Approximation

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Giannarakis, N., Beckett, R., Mahajan, R., & Walker, D. P. (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
Giannarakis, Nick ; Beckett, Ryan ; Mahajan, Ratul ; Walker, David P. / Efficient verification of network fault tolerance via counterexample-guided refinement. Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. editor / Isil Dillig ; Serdar Tasiran. Springer Verlag, 2019. pp. 305-323 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{867401e52a304ce8a11fe250e3911082,
title = "Efficient verification of network fault tolerance via counterexample-guided refinement",
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.",
author = "Nick Giannarakis and Ryan Beckett and Ratul Mahajan and Walker, {David P.}",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-25543-5_18",
language = "English (US)",
isbn = "9783030255428",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "305--323",
editor = "Isil Dillig and Serdar Tasiran",
booktitle = "Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings",
address = "Germany",

}

Giannarakis, N, Beckett, R, Mahajan, R & Walker, DP 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11562 LNCS, Springer Verlag, pp. 305-323, 31st International Conference on Computer Aided Verification, CAV 2019, New York City, United States, 7/15/19. https://doi.org/10.1007/978-3-030-25543-5_18

Efficient verification of network fault tolerance via counterexample-guided refinement. / Giannarakis, Nick; Beckett, Ryan; Mahajan, Ratul; Walker, David P.

Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. ed. / Isil Dillig; Serdar Tasiran. Springer Verlag, 2019. p. 305-323 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11562 LNCS).

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

TY - GEN

T1 - Efficient verification of network fault tolerance via counterexample-guided refinement

AU - Giannarakis, Nick

AU - Beckett, Ryan

AU - Mahajan, Ratul

AU - Walker, David P.

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85069859946&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85069859946&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-25543-5_18

DO - 10.1007/978-3-030-25543-5_18

M3 - Conference contribution

SN - 9783030255428

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 305

EP - 323

BT - Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings

A2 - Dillig, Isil

A2 - Tasiran, Serdar

PB - Springer Verlag

ER -

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