The validation of distributed algorithms is a crucial, although challenging, task. The processes executing these algorithms communicate to one another, their actions depend on the messages received, and their number is arbitrary. These characteristics are captured by so called reactive parameterized systems. The task of validating or refuting properties of these systems is daunting, due to the difficulty of limiting the possible evolutions, thus having to deal with genuinely infinite-state systems. In this paper, we consider distributed algorithms to solve the reliable broadcast problem in the presence of crash, send-omission, and byzantine failures. We study the properties of these algorithms using Model Checker Modulo Theories (MCMT). MCMT is able to verify safety properties of infinite-state reactive parameterized systems, for any number of processes. It adopts a pure SMT (Satisfiability Modulo Theories) approach, due to its flexibility. It uses some form of abstractions, and involves acceleration mechanisms in order to increase computation efficiency. In this work, we study how to model the algorithms in MCMT according to two paradigms: array-based systems and counter abstraction. The former uses unbounded arrays to represent the states of the processes. The latter exploits a characteristic of the considered algorithms, which consists in determining the behavior of the processes de- pending on the number of messages they receive from other processes (threshold-guarded algorithms). The algorithms are modeled according to both paradigms, or using a hybrid approach mixing arrays with counter abstraction. We discuss the rationale of our modeling choices and show how to use the characteristics of MCMT to perform the validation. We report a performance evaluation of the computation with the different models, and (in the counter abstraction paradigm) compare the results with equivalent modelization in both Z3 and nuXmv, obtained by translating our models.

SMT-based approaches to Model Checking of Distributed Broadcast Algorithms / F. Alberti, S. Ghilardi, A. Orsini, E. Pagani. ((Intervento presentato al convegno Formal Reasoning in Distributed Algorithms tenutosi a Grenoble nel 2015.

SMT-based approaches to Model Checking of Distributed Broadcast Algorithms

S. Ghilardi
Secondo
;
E. Pagani
Ultimo
2015

Abstract

The validation of distributed algorithms is a crucial, although challenging, task. The processes executing these algorithms communicate to one another, their actions depend on the messages received, and their number is arbitrary. These characteristics are captured by so called reactive parameterized systems. The task of validating or refuting properties of these systems is daunting, due to the difficulty of limiting the possible evolutions, thus having to deal with genuinely infinite-state systems. In this paper, we consider distributed algorithms to solve the reliable broadcast problem in the presence of crash, send-omission, and byzantine failures. We study the properties of these algorithms using Model Checker Modulo Theories (MCMT). MCMT is able to verify safety properties of infinite-state reactive parameterized systems, for any number of processes. It adopts a pure SMT (Satisfiability Modulo Theories) approach, due to its flexibility. It uses some form of abstractions, and involves acceleration mechanisms in order to increase computation efficiency. In this work, we study how to model the algorithms in MCMT according to two paradigms: array-based systems and counter abstraction. The former uses unbounded arrays to represent the states of the processes. The latter exploits a characteristic of the considered algorithms, which consists in determining the behavior of the processes de- pending on the number of messages they receive from other processes (threshold-guarded algorithms). The algorithms are modeled according to both paradigms, or using a hybrid approach mixing arrays with counter abstraction. We discuss the rationale of our modeling choices and show how to use the characteristics of MCMT to perform the validation. We report a performance evaluation of the computation with the different models, and (in the counter abstraction paradigm) compare the results with equivalent modelization in both Z3 and nuXmv, obtained by translating our models.
5-giu-2015
reactive parameterized systems; SMT-based model checking; fault-tolerant broadcast algorithms; array-based systems; counter abstraction
Settore INF/01 - Informatica
http://discotec2015.inria.fr/workshops/frida-2015/index.html
SMT-based approaches to Model Checking of Distributed Broadcast Algorithms / F. Alberti, S. Ghilardi, A. Orsini, E. Pagani. ((Intervento presentato al convegno Formal Reasoning in Distributed Algorithms tenutosi a Grenoble nel 2015.
Conference Object
File in questo prodotto:
File Dimensione Formato  
FRIDA2015_abstract.pdf

accesso aperto

Descrizione: Articolo completo
Tipologia: Altro
Dimensione 101.98 kB
Formato Adobe PDF
101.98 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/502069
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact