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.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.