Final published version
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter
}
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 -