Home > Research > Publications & Outputs > Brief Announcement

Research

Associated organisational units

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/ISSN › Chapter

Published

Standard

Brief Announcement: Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction. / Bokor, Péter; Serafini, Marco; Suri, Neeraj et al.
Distributed Computing: 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings. Springer, 2009. p. 289-290.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter

Harvard

Bokor, P, Serafini, M, Suri, N & Veith, H 2009, Brief Announcement: Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction. in Distributed Computing: 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings. Springer, pp. 289-290. https://doi.org/10.1007/978-3-642-04355-0_29

APA

Bokor, P., Serafini, M., Suri, N., & Veith, H. (2009). Brief Announcement: Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction. In Distributed Computing: 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings (pp. 289-290). Springer. https://doi.org/10.1007/978-3-642-04355-0_29

Vancouver

Bokor P, Serafini M, Suri N, Veith H. Brief Announcement: Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction. In Distributed Computing: 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings. Springer. 2009. p. 289-290 doi: 10.1007/978-3-642-04355-0_29

Author

Bokor, Péter ; Serafini, Marco ; Suri, Neeraj et al. / Brief Announcement : Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction. Distributed Computing: 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings. Springer, 2009. pp. 289-290

Bibtex

@inbook{288f093e1e7a49079cf29e74e33c3a9a,
title = "Brief Announcement: Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction",
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.",
author = "P{\'e}ter Bokor and Marco Serafini and Neeraj Suri and Helmut Veith",
year = "2009",
doi = "10.1007/978-3-642-04355-0_29",
language = "English",
isbn = "9783642043543",
pages = "289--290",
booktitle = "Distributed Computing",
publisher = "Springer",

}

RIS

TY - CHAP

T1 - Brief Announcement

T2 - Efficient Model Checking of Fault-Tolerant Distributed Protocols Using Symmetry Reduction

AU - Bokor, Péter

AU - Serafini, Marco

AU - Suri, Neeraj

AU - Veith, Helmut

PY - 2009

Y1 - 2009

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

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

U2 - 10.1007/978-3-642-04355-0_29

DO - 10.1007/978-3-642-04355-0_29

M3 - Chapter

SN - 9783642043543

SP - 289

EP - 290

BT - Distributed Computing

PB - Springer

ER -