Home > Research > Publications & Outputs > Efficient verification of distributed protocols...

Links

Text available via DOI:

View graph of relations

Efficient verification of distributed protocols using stateful model checking

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paper

Published

Standard

Efficient verification of distributed protocols using stateful model checking. / Saissi, H.; Bokor, P.; Muftuoglu, C.A.; Suri, Neeraj; Serafini, M.

2013 IEEE 32nd International Symposium on Reliable Distributed Systems. IEEE, 2013. p. 133-142.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paper

Harvard

Saissi, H, Bokor, P, Muftuoglu, CA, Suri, N & Serafini, M 2013, Efficient verification of distributed protocols using stateful model checking. in 2013 IEEE 32nd International Symposium on Reliable Distributed Systems. IEEE, pp. 133-142. https://doi.org/10.1109/SRDS.2013.22

APA

Saissi, H., Bokor, P., Muftuoglu, C. A., Suri, N., & Serafini, M. (2013). Efficient verification of distributed protocols using stateful model checking. In 2013 IEEE 32nd International Symposium on Reliable Distributed Systems (pp. 133-142). IEEE. https://doi.org/10.1109/SRDS.2013.22

Vancouver

Saissi H, Bokor P, Muftuoglu CA, Suri N, Serafini M. Efficient verification of distributed protocols using stateful model checking. In 2013 IEEE 32nd International Symposium on Reliable Distributed Systems. IEEE. 2013. p. 133-142 https://doi.org/10.1109/SRDS.2013.22

Author

Saissi, H. ; Bokor, P. ; Muftuoglu, C.A. ; Suri, Neeraj ; Serafini, M. / Efficient verification of distributed protocols using stateful model checking. 2013 IEEE 32nd International Symposium on Reliable Distributed Systems. IEEE, 2013. pp. 133-142

Bibtex

@inproceedings{b56b5a651a0c4a618d81575124ed28ca,
title = "Efficient verification of distributed protocols using stateful model checking",
abstract = "This paper presents efficient model checking of distributed software. Key to the achieved efficiency is a novel stateful model checking strategy that is based on the decomposition of states into a relevant and an auxiliary part. We formally show this strategy to be sound, complete, and terminating for general finite-state systems. As a case study, we implement the proposed strategy within Basset/MP-Basset, a model checker for message-passing Java programs. Our evaluation with actual deployed fault-tolerant message-passing protocols shows that the proposed stateful optimization is able to reduce model checking time and memory by up to 69% compared to the naive stateful search, and 39% compared to partial-order reduction. {\textcopyright} 2013 IEEE.",
keywords = "Distributed protocols, Distributed software, Fault-tolerant, Finite state systems, Java program, Model checker, Partial-order reduction, Computer software, Java programming language, Message passing, Model checking",
author = "H. Saissi and P. Bokor and C.A. Muftuoglu and Neeraj Suri and M. Serafini",
year = "2013",
month = sep,
day = "30",
doi = "10.1109/SRDS.2013.22",
language = "English",
pages = "133--142",
booktitle = "2013 IEEE 32nd International Symposium on Reliable Distributed Systems",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Efficient verification of distributed protocols using stateful model checking

AU - Saissi, H.

AU - Bokor, P.

AU - Muftuoglu, C.A.

AU - Suri, Neeraj

AU - Serafini, M.

PY - 2013/9/30

Y1 - 2013/9/30

N2 - This paper presents efficient model checking of distributed software. Key to the achieved efficiency is a novel stateful model checking strategy that is based on the decomposition of states into a relevant and an auxiliary part. We formally show this strategy to be sound, complete, and terminating for general finite-state systems. As a case study, we implement the proposed strategy within Basset/MP-Basset, a model checker for message-passing Java programs. Our evaluation with actual deployed fault-tolerant message-passing protocols shows that the proposed stateful optimization is able to reduce model checking time and memory by up to 69% compared to the naive stateful search, and 39% compared to partial-order reduction. © 2013 IEEE.

AB - This paper presents efficient model checking of distributed software. Key to the achieved efficiency is a novel stateful model checking strategy that is based on the decomposition of states into a relevant and an auxiliary part. We formally show this strategy to be sound, complete, and terminating for general finite-state systems. As a case study, we implement the proposed strategy within Basset/MP-Basset, a model checker for message-passing Java programs. Our evaluation with actual deployed fault-tolerant message-passing protocols shows that the proposed stateful optimization is able to reduce model checking time and memory by up to 69% compared to the naive stateful search, and 39% compared to partial-order reduction. © 2013 IEEE.

KW - Distributed protocols

KW - Distributed software

KW - Fault-tolerant

KW - Finite state systems

KW - Java program

KW - Model checker

KW - Partial-order reduction

KW - Computer software

KW - Java programming language

KW - Message passing

KW - Model checking

U2 - 10.1109/SRDS.2013.22

DO - 10.1109/SRDS.2013.22

M3 - Conference contribution/Paper

SP - 133

EP - 142

BT - 2013 IEEE 32nd International Symposium on Reliable Distributed Systems

PB - IEEE

ER -