Home > Research > Publications & Outputs > Role-based symmetry reduction of fault-tolerant...

Links

Text available via DOI:

View graph of relations

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

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter

Published

Standard

Role-based symmetry reduction of fault-tolerant distributed protocols with language support. / Bokor, P.; Serafini, M.; Suri, Neeraj; Veith, H.

Formal Methods and Software Engineering: 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings. Vol. 5885 LNCS Springer, 2009. p. 147-166.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter

Harvard

Bokor, P, Serafini, M, Suri, N & Veith, H 2009, Role-based symmetry reduction of fault-tolerant distributed protocols with language support. in Formal Methods and Software Engineering: 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings. vol. 5885 LNCS, Springer, pp. 147-166. https://doi.org/10.1007/978-3-642-10373-5_8

APA

Bokor, P., Serafini, M., Suri, N., & Veith, H. (2009). Role-based symmetry reduction of fault-tolerant distributed protocols with language support. In Formal Methods and Software Engineering: 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings (Vol. 5885 LNCS, pp. 147-166). Springer. https://doi.org/10.1007/978-3-642-10373-5_8

Vancouver

Bokor P, Serafini M, Suri N, Veith H. Role-based symmetry reduction of fault-tolerant distributed protocols with language support. In Formal Methods and Software Engineering: 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings. Vol. 5885 LNCS. Springer. 2009. p. 147-166 https://doi.org/10.1007/978-3-642-10373-5_8

Author

Bokor, P. ; Serafini, M. ; Suri, Neeraj ; Veith, H. / Role-based symmetry reduction of fault-tolerant distributed protocols with language support. Formal Methods and Software Engineering: 11th International Conference on Formal Engineering Methods ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings. Vol. 5885 LNCS Springer, 2009. pp. 147-166

Bibtex

@inbook{b2979f236ead466581395ae57ab89352,
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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2009.",
keywords = "Asynchronous protocols, Automated verification, Degree of symmetry, Different process, Distributed protocols, Exploration methods, Fault types, Fault-tolerant, Fundamental building blocks, Google file systems, Group memberships, High level description, Liveness properties, Practical systems, Protocol design, Protocol verification, Role-based, Symmetry reduction, System state, Fault tolerant computer systems, Formal methods, High level languages, Specifications, Model checking",
author = "P. Bokor and M. Serafini and Neeraj Suri and H. Veith",
year = "2009",
doi = "10.1007/978-3-642-10373-5_8",
language = "English",
isbn = "3642103723",
volume = "5885 LNCS",
pages = "147--166",
booktitle = "Formal Methods and Software Engineering",
publisher = "Springer",

}

RIS

TY - CHAP

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

AU - Bokor, P.

AU - Serafini, M.

AU - Suri, Neeraj

AU - Veith, H.

PY - 2009

Y1 - 2009

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. © Springer-Verlag Berlin Heidelberg 2009.

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. © Springer-Verlag Berlin Heidelberg 2009.

KW - Asynchronous protocols

KW - Automated verification

KW - Degree of symmetry

KW - Different process

KW - Distributed protocols

KW - Exploration methods

KW - Fault types

KW - Fault-tolerant

KW - Fundamental building blocks

KW - Google file systems

KW - Group memberships

KW - High level description

KW - Liveness properties

KW - Practical systems

KW - Protocol design

KW - Protocol verification

KW - Role-based

KW - Symmetry reduction

KW - System state

KW - Fault tolerant computer systems

KW - Formal methods

KW - High level languages

KW - Specifications

KW - Model checking

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

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

M3 - Chapter

SN - 3642103723

SN - 9783642103728

VL - 5885 LNCS

SP - 147

EP - 166

BT - Formal Methods and Software Engineering

PB - Springer

ER -