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.
Type de document :
Communication dans un congrès
John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.216-223, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_17〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01055152
Contributeur : Hal Ifip <>
Soumis le : lundi 11 août 2014 - 16:27:49
Dernière modification le : vendredi 11 août 2017 - 16:16:34
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:16:26

Fichier

61170213.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Péter Bokor, Marco Serafini, Neeraj Suri. On Efficient Models for Model Checking Message-Passing Distributed Protocols. John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.216-223, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_17〉. 〈hal-01055152〉

Partager

Métriques

Consultations de la notice

232

Téléchargements de fichiers

179