The automated, formal verification of distributed algorithms is a crucial, although challenging, task. In this paper, we study the properties of distributed algorithms solving the reliable broadcast problem in various failure models. We investigate the suitability of a direct Satisfiability Modulo Theories (SMT) approach to model these algorithms in order to validate safety properties. In a previous work, we modeled distributed algorithms using the declarative framework of array-based systems. In this work, we try also a simulation of array-based systems via counter systems. In fact, this simulation does not indeed introduce spurious runs violating the safety properties we want to formally verify in a significant class of problems. We report the related performance evaluations of some SMT-based modelcheckers (essentially, our tool MCMT and tools like μZ, nuXmv). The experimental results are interesting because they show on one hand that state-of- The- Art SMT-based technology can handle problems arising in fault- Tolerant environments, and on the other hand that different heuristics and search strategies (e.g. acceleration versus abstraction) can have practical impact.

Counter abstractions in model checking of distributed broadcast algorithms: some case studies / F. Alberti, S. Ghilardi, A. Orsini, E. Pagani (CEUR WORKSHOP PROCEEDINGS). - In: Italian Conference on Computational Logic : Proceedings / [a cura di] C. Fiorentini, A. Momigliano. - Prima edizione. - [s.l] : CEUR, 2016 Jun. - pp. 102-117 (( Intervento presentato al 31. convegno CILC tenutosi a Milano nel 2016.

Counter abstractions in model checking of distributed broadcast algorithms: some case studies

S. Ghilardi;E. Pagani
2016

Abstract

The automated, formal verification of distributed algorithms is a crucial, although challenging, task. In this paper, we study the properties of distributed algorithms solving the reliable broadcast problem in various failure models. We investigate the suitability of a direct Satisfiability Modulo Theories (SMT) approach to model these algorithms in order to validate safety properties. In a previous work, we modeled distributed algorithms using the declarative framework of array-based systems. In this work, we try also a simulation of array-based systems via counter systems. In fact, this simulation does not indeed introduce spurious runs violating the safety properties we want to formally verify in a significant class of problems. We report the related performance evaluations of some SMT-based modelcheckers (essentially, our tool MCMT and tools like μZ, nuXmv). The experimental results are interesting because they show on one hand that state-of- The- Art SMT-based technology can handle problems arising in fault- Tolerant environments, and on the other hand that different heuristics and search strategies (e.g. acceleration versus abstraction) can have practical impact.
Satisfiability modulo theories; model checking; distributed algorithms
Settore INF/01 - Informatica
giu-2016
http://ceur-ws.org/Vol-1645/
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
CILC_2016.pdf

accesso riservato

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 421.89 kB
Formato Adobe PDF
421.89 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
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/456416
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact