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

Francesco Alberti, Silvio Ghilardi, Andrea Orsini, Elena Pagani

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish
Pages (from-to)102-117
Number of pages16
JournalUnknown Journal
Volume1645
Publication statusPublished - 2016
Externally publishedYes

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Counter abstractions in model checking of distributed broadcast algorithms: Some case studies'. Together they form a unique fingerprint.

Cite this