Home > Research > Publications & Outputs > Brief Announcement

Links

Text available via DOI:

View graph of relations

Brief Announcement: Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction

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

Published
Close
Publication date2009
Host publicationDistributed Computing: 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings
PublisherSpringer
Pages289-290
Number of pages2
ISBN (electronic)9783642043550
ISBN (print)9783642043543
<mark>Original language</mark>English

Abstract

Motivation. Fault-tolerant (FT) distributed protocols represent fundamental building blocks behind many practical systems. A rigorous design of these protocols is desired given the complexity of manual proofs. The application of model checking (MC) [2] for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalability is limited by the number of different system states. Although FT distributed protocols usually display a 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 [6] and improve on existing applications of it. Our secondary contribution is to define a high-level description language (called FTDP) to ease the symmetry-aware specification of FT distributed protocols.