Parameterized model checking of fault-tolerant distributed algorithms by abstraction

A John, I Konnov, U Schmid, H Veith… - 2013 Formal Methods …, 2013 - ieeexplore.ieee.org
2013 Formal Methods in Computer-Aided Design, 2013ieeexplore.ieee.org
We introduce an automated parameterized verification method for fault-tolerant distributed
algorithms (FTDA). FTDAs are parameterized by both the number of processes and the
assumed maximum number of faults. At the center of our technique is a parametric interval
abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters.
Using PIA for both data abstraction and a new form of counter abstraction, we reduce the
parameterized problem to finite-state model checking. We demonstrate the practical …
We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of faults. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking. We demonstrate the practical feasibility of our method by verifying safety and liveness of several fault-tolerant broadcasting algorithms, and finding counter examples in the case where there are more faults than the FTDA was designed for.
ieeexplore.ieee.org