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.
|Number of pages||16|
|Publication status||Published - 2016|
ASJC Scopus subject areas
- Computer Science(all)