On efficient models for model checking message-passing distributed protocols

Péter Bokor, Marco Serafini, Neeraj Suri

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

7 Citations (Scopus)

Abstract

The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add "unnecessary" complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique. We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13th that of existing equivalent MP models.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages216-223
Number of pages8
Volume6117 LNCS
DOIs
Publication statusPublished - 21 Jul 2010
Externally publishedYes
EventJoint 12th IFIP WG 6.1 International Conference, FMOODS 2010 - Amsterdam, Netherlands
Duration: 7 Jun 20109 Jun 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6117 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

OtherJoint 12th IFIP WG 6.1 International Conference, FMOODS 2010
CountryNetherlands
CityAmsterdam
Period7/6/109/6/10

Fingerprint

Distributed Protocol
Message passing
Model checking
Message Passing
Model Checking
Network protocols
Distributed Algorithms
Parallel algorithms
Model
Formal Methods
State Machine
Formal Model
Formal methods
Fault Tolerance
Replication
Fault tolerance
Correctness
Traffic
Semantics

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bokor, P., Serafini, M., & Suri, N. (2010). On efficient models for model checking message-passing distributed protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6117 LNCS, pp. 216-223). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6117 LNCS). https://doi.org/10.1007/978-3-642-13464-7_17

On efficient models for model checking message-passing distributed protocols. / Bokor, Péter; Serafini, Marco; Suri, Neeraj.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6117 LNCS 2010. p. 216-223 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6117 LNCS).

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

Bokor, P, Serafini, M & Suri, N 2010, On efficient models for model checking message-passing distributed protocols. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 6117 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6117 LNCS, pp. 216-223, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010, Amsterdam, Netherlands, 7/6/10. https://doi.org/10.1007/978-3-642-13464-7_17
Bokor P, Serafini M, Suri N. On efficient models for model checking message-passing distributed protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6117 LNCS. 2010. p. 216-223. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-13464-7_17
Bokor, Péter ; Serafini, Marco ; Suri, Neeraj. / On efficient models for model checking message-passing distributed protocols. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6117 LNCS 2010. pp. 216-223 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{92275db7f18948758b80bbfcebc32c92,
title = "On efficient models for model checking message-passing distributed protocols",
abstract = "The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add {"}unnecessary{"} complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique. We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13th that of existing equivalent MP models.",
author = "P{\'e}ter Bokor and Marco Serafini and Neeraj Suri",
year = "2010",
month = "7",
day = "21",
doi = "10.1007/978-3-642-13464-7_17",
language = "English",
isbn = "3642134637",
volume = "6117 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "216--223",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - On efficient models for model checking message-passing distributed protocols

AU - Bokor, Péter

AU - Serafini, Marco

AU - Suri, Neeraj

PY - 2010/7/21

Y1 - 2010/7/21

N2 - The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add "unnecessary" complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique. We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13th that of existing equivalent MP models.

AB - The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add "unnecessary" complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique. We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13th that of existing equivalent MP models.

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

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

U2 - 10.1007/978-3-642-13464-7_17

DO - 10.1007/978-3-642-13464-7_17

M3 - Conference contribution

AN - SCOPUS:77954639792

SN - 3642134637

SN - 9783642134630

VL - 6117 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 216

EP - 223

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -