Role-based symmetry reduction of fault-tolerant distributed protocols with language support

Péter Bokor, Marco Serafini, Neeraj Suri, Helmut Veith

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

4 Citations (Scopus)

Abstract

Fault-tolerant (FT) distributed protocols (such as group membership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT distributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their automated verification often disregard this symmetry. Therefore, we propose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our secondary contribution is to define a high-level description language called FTDP to ease the symmetry aware specification of FT distributed protocols. FTDP supports synchronous as well as asynchronous protocols, a variety of fault types, and the specification of safety and liveness properties. Specifications written in FTDP can directly be analyzed by tools supporting symmetry reduction. We demonstrate the benefit of our approach using the example of well-known and complex distributed FT protocols, specifically Paxos and the Byzantine Generals.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages147-166
Number of pages20
Volume5885 LNCS
DOIs
Publication statusPublished - 1 Dec 2009
Externally publishedYes
Event11th International Conference on Formal Engineering Methods, ICFEM 2009 - Rio de Janeiro, Brazil
Duration: 9 Dec 200912 Dec 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5885 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other11th International Conference on Formal Engineering Methods, ICFEM 2009
CountryBrazil
CityRio de Janeiro
Period9/12/0912/12/09

Fingerprint

Distributed Protocol
Symmetry Reduction
Fault-tolerant
Symmetry
Network protocols
Specification
Model Checking
Protocol Verification
Model checking
Liveness
File System
Specifications
Leverage
Building Blocks
Process Model
Automation
Fault
Safety
Language
Demonstrate

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bokor, P., Serafini, M., Suri, N., & Veith, H. (2009). Role-based symmetry reduction of fault-tolerant distributed protocols with language support. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5885 LNCS, pp. 147-166). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5885 LNCS). https://doi.org/10.1007/978-3-642-10373-5_8

Role-based symmetry reduction of fault-tolerant distributed protocols with language support. / Bokor, Péter; Serafini, Marco; Suri, Neeraj; Veith, Helmut.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5885 LNCS 2009. p. 147-166 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5885 LNCS).

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

Bokor, P, Serafini, M, Suri, N & Veith, H 2009, Role-based symmetry reduction of fault-tolerant distributed protocols with language support. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5885 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5885 LNCS, pp. 147-166, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, 9/12/09. https://doi.org/10.1007/978-3-642-10373-5_8
Bokor P, Serafini M, Suri N, Veith H. Role-based symmetry reduction of fault-tolerant distributed protocols with language support. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5885 LNCS. 2009. p. 147-166. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-10373-5_8
Bokor, Péter ; Serafini, Marco ; Suri, Neeraj ; Veith, Helmut. / Role-based symmetry reduction of fault-tolerant distributed protocols with language support. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5885 LNCS 2009. pp. 147-166 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{007d5a43ca8643569cceb752bf2f691b,
title = "Role-based symmetry reduction of fault-tolerant distributed protocols with language support",
abstract = "Fault-tolerant (FT) distributed protocols (such as group membership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT distributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their automated verification often disregard this symmetry. Therefore, we propose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our secondary contribution is to define a high-level description language called FTDP to ease the symmetry aware specification of FT distributed protocols. FTDP supports synchronous as well as asynchronous protocols, a variety of fault types, and the specification of safety and liveness properties. Specifications written in FTDP can directly be analyzed by tools supporting symmetry reduction. We demonstrate the benefit of our approach using the example of well-known and complex distributed FT protocols, specifically Paxos and the Byzantine Generals.",
author = "P{\'e}ter Bokor and Marco Serafini and Neeraj Suri and Helmut Veith",
year = "2009",
month = "12",
day = "1",
doi = "10.1007/978-3-642-10373-5_8",
language = "English",
isbn = "3642103723",
volume = "5885 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "147--166",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Role-based symmetry reduction of fault-tolerant distributed protocols with language support

AU - Bokor, Péter

AU - Serafini, Marco

AU - Suri, Neeraj

AU - Veith, Helmut

PY - 2009/12/1

Y1 - 2009/12/1

N2 - Fault-tolerant (FT) distributed protocols (such as group membership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT distributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their automated verification often disregard this symmetry. Therefore, we propose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our secondary contribution is to define a high-level description language called FTDP to ease the symmetry aware specification of FT distributed protocols. FTDP supports synchronous as well as asynchronous protocols, a variety of fault types, and the specification of safety and liveness properties. Specifications written in FTDP can directly be analyzed by tools supporting symmetry reduction. We demonstrate the benefit of our approach using the example of well-known and complex distributed FT protocols, specifically Paxos and the Byzantine Generals.

AB - Fault-tolerant (FT) distributed protocols (such as group membership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT distributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their automated verification often disregard this symmetry. Therefore, we propose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our secondary contribution is to define a high-level description language called FTDP to ease the symmetry aware specification of FT distributed protocols. FTDP supports synchronous as well as asynchronous protocols, a variety of fault types, and the specification of safety and liveness properties. Specifications written in FTDP can directly be analyzed by tools supporting symmetry reduction. We demonstrate the benefit of our approach using the example of well-known and complex distributed FT protocols, specifically Paxos and the Byzantine Generals.

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

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

U2 - 10.1007/978-3-642-10373-5_8

DO - 10.1007/978-3-642-10373-5_8

M3 - Conference contribution

SN - 3642103723

SN - 9783642103728

VL - 5885 LNCS

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

SP - 147

EP - 166

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

ER -