Home > Research > Publications & Outputs > Efficient model checking of fault-tolerant dist...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Efficient model checking of fault-tolerant distributed protocols

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Efficient model checking of fault-tolerant distributed protocols. / Bokor, P.; Kinder, J.; Serafini, M. et al.
2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE, 2011. p. 73-84.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Bokor, P, Kinder, J, Serafini, M & Suri, N 2011, Efficient model checking of fault-tolerant distributed protocols. in 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE, pp. 73-84. https://doi.org/10.1109/DSN.2011.5958208

APA

Bokor, P., Kinder, J., Serafini, M., & Suri, N. (2011). Efficient model checking of fault-tolerant distributed protocols. In 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN) (pp. 73-84). IEEE. https://doi.org/10.1109/DSN.2011.5958208

Vancouver

Bokor P, Kinder J, Serafini M, Suri N. Efficient model checking of fault-tolerant distributed protocols. In 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE. 2011. p. 73-84 doi: 10.1109/DSN.2011.5958208

Author

Bokor, P. ; Kinder, J. ; Serafini, M. et al. / Efficient model checking of fault-tolerant distributed protocols. 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN). IEEE, 2011. pp. 73-84

Bibtex

@inproceedings{d9d4a50a3e1c479d9b50e5fef85b34cc,
title = "Efficient model checking of fault-tolerant distributed protocols",
abstract = "To aid the formal verification of fault-tolerant distributed protocols, we propose an approach that significantly reduces the costs of their model checking. These protocols often specify atomic, process-local events that consume a set of messages, change the state of a process, and send zero or more messages. We call such events quorum transitions and leverage them to optimize state exploration in two ways. First, we generate fewer states compared to models where quorum transitions are expressed by single-message transitions. Second, we refine transitions into a set of equivalent, finer-grained transitions that allow partial-order algorithms to achieve better reduction. We implement the MP-Basset model checker, which supports refined quorum transitions. We model check protocols representing core primitives of deployed reliable distributed systems, namely: Paxos consensus, regular storage, and Byzantine-tolerant multicast. We achieve up to 92% memory and 85% time reduction compared to model checking with standard unrefined single-message transitions. {\textcopyright} 2011 IEEE.",
keywords = "Distributed protocols, Fault-tolerant, Formal verifications, Model check, Model checker, Multicasts, Partial-order algorithms, Reliable distributed systems, State exploration, Time reduction, Fault tolerant computer systems, Refining, Model checking",
author = "P. Bokor and J. Kinder and M. Serafini and Neeraj Suri",
year = "2011",
month = jun,
day = "27",
doi = "10.1109/DSN.2011.5958208",
language = "English",
isbn = "9781424492329",
pages = "73--84",
booktitle = "2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN)",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Efficient model checking of fault-tolerant distributed protocols

AU - Bokor, P.

AU - Kinder, J.

AU - Serafini, M.

AU - Suri, Neeraj

PY - 2011/6/27

Y1 - 2011/6/27

N2 - To aid the formal verification of fault-tolerant distributed protocols, we propose an approach that significantly reduces the costs of their model checking. These protocols often specify atomic, process-local events that consume a set of messages, change the state of a process, and send zero or more messages. We call such events quorum transitions and leverage them to optimize state exploration in two ways. First, we generate fewer states compared to models where quorum transitions are expressed by single-message transitions. Second, we refine transitions into a set of equivalent, finer-grained transitions that allow partial-order algorithms to achieve better reduction. We implement the MP-Basset model checker, which supports refined quorum transitions. We model check protocols representing core primitives of deployed reliable distributed systems, namely: Paxos consensus, regular storage, and Byzantine-tolerant multicast. We achieve up to 92% memory and 85% time reduction compared to model checking with standard unrefined single-message transitions. © 2011 IEEE.

AB - To aid the formal verification of fault-tolerant distributed protocols, we propose an approach that significantly reduces the costs of their model checking. These protocols often specify atomic, process-local events that consume a set of messages, change the state of a process, and send zero or more messages. We call such events quorum transitions and leverage them to optimize state exploration in two ways. First, we generate fewer states compared to models where quorum transitions are expressed by single-message transitions. Second, we refine transitions into a set of equivalent, finer-grained transitions that allow partial-order algorithms to achieve better reduction. We implement the MP-Basset model checker, which supports refined quorum transitions. We model check protocols representing core primitives of deployed reliable distributed systems, namely: Paxos consensus, regular storage, and Byzantine-tolerant multicast. We achieve up to 92% memory and 85% time reduction compared to model checking with standard unrefined single-message transitions. © 2011 IEEE.

KW - Distributed protocols

KW - Fault-tolerant

KW - Formal verifications

KW - Model check

KW - Model checker

KW - Multicasts

KW - Partial-order algorithms

KW - Reliable distributed systems

KW - State exploration

KW - Time reduction

KW - Fault tolerant computer systems

KW - Refining

KW - Model checking

U2 - 10.1109/DSN.2011.5958208

DO - 10.1109/DSN.2011.5958208

M3 - Conference contribution/Paper

SN - 9781424492329

SP - 73

EP - 84

BT - 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN)

PB - IEEE

ER -