Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
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 -