Efficient verification of distributed protocols using stateful model checking

Habib Saissi, Peter Bokor, Can Arda Muftuoglu, Neeraj Suri, Marco Serafini

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings of the IEEE Symposium on Reliable Distributed Systems
Pages133-142
Number of pages10
DOIs
Publication statusPublished - 1 Dec 2013
Event2013 IEEE 32nd International Symposium on Reliable Distributed Systems, SRDS 2013 - Braga, Portugal
Duration: 1 Oct 20133 Oct 2013

Other

Other2013 IEEE 32nd International Symposium on Reliable Distributed Systems, SRDS 2013
CountryPortugal
CityBraga
Period1/10/133/10/13

Fingerprint

Distributed Protocol
Model checking
Model Checking
Message passing
Message Passing
Network protocols
Order Reduction
Partial Order
Fault-tolerant
Java
Acoustic waves
Decomposition
Data storage equipment
Decompose
Software
Optimization
Evaluation
Strategy
Model

ASJC Scopus subject areas

  • Hardware and Architecture
  • Computer Networks and Communications
  • Software
  • Theoretical Computer Science

Cite this

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

Efficient verification of distributed protocols using stateful model checking. / Saissi, Habib; Bokor, Peter; Muftuoglu, Can Arda; Suri, Neeraj; Serafini, Marco.

Proceedings of the IEEE Symposium on Reliable Distributed Systems. 2013. p. 133-142 6656269.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Saissi, H, Bokor, P, Muftuoglu, CA, Suri, N & Serafini, M 2013, Efficient verification of distributed protocols using stateful model checking. in Proceedings of the IEEE Symposium on Reliable Distributed Systems., 6656269, pp. 133-142, 2013 IEEE 32nd International Symposium on Reliable Distributed Systems, SRDS 2013, Braga, Portugal, 1/10/13. https://doi.org/10.1109/SRDS.2013.22
Saissi H, Bokor P, Muftuoglu CA, Suri N, Serafini M. Efficient verification of distributed protocols using stateful model checking. In Proceedings of the IEEE Symposium on Reliable Distributed Systems. 2013. p. 133-142. 6656269 https://doi.org/10.1109/SRDS.2013.22
Saissi, Habib ; Bokor, Peter ; Muftuoglu, Can Arda ; Suri, Neeraj ; Serafini, Marco. / Efficient verification of distributed protocols using stateful model checking. Proceedings of the IEEE Symposium on Reliable Distributed Systems. 2013. pp. 133-142
@inproceedings{7be3907d359b43ad8f80891cfff72723,
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.",
author = "Habib Saissi and Peter Bokor and Muftuoglu, {Can Arda} and Neeraj Suri and Marco Serafini",
year = "2013",
month = "12",
day = "1",
doi = "10.1109/SRDS.2013.22",
language = "English",
isbn = "9780769551159",
pages = "133--142",
booktitle = "Proceedings of the IEEE Symposium on Reliable Distributed Systems",

}

TY - GEN

T1 - Efficient verification of distributed protocols using stateful model checking

AU - Saissi, Habib

AU - Bokor, Peter

AU - Muftuoglu, Can Arda

AU - Suri, Neeraj

AU - Serafini, Marco

PY - 2013/12/1

Y1 - 2013/12/1

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.

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.

UR - http://www.scopus.com/inward/record.url?scp=84891545808&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84891545808&partnerID=8YFLogxK

U2 - 10.1109/SRDS.2013.22

DO - 10.1109/SRDS.2013.22

M3 - Conference contribution

AN - SCOPUS:84891545808

SN - 9780769551159

SP - 133

EP - 142

BT - Proceedings of the IEEE Symposium on Reliable Distributed Systems

ER -