On Verifying Fault Tolerance of Distributed Protocols
=====================================================


Distributed systems are composed of processes connected in some
network. Distributed systems may suffer from faults: processes may
stop, may be interrupted, and may be maliciously attacked.
Fault-tolerant protocols are designed to be resistant to faults.
Proving the resistance of protocols to faults is a very challenging
problem, as it combines the parameterized setting that distributed
systems are based-on, with the need to consider a hostile environment
that produces the faults.  Considering all the possible fault
scenarios for a protocol is very difficult.  Thus, reasoning about
fault-tolerance protocols utterly needs formal methods.

In this paper we describe a framework for verifying the fault
tolerance of (synchronous or asynchronous) distributed protocols. In
addition to the description of the protocol and the desired behavior,
the user provides the fault type (e.g., fail-stop, Byzantine,...) and
its distribution (e.g., a strict minority of the processes are faulty,
...). Our framework is based on augmenting the description of the
configurations of the system by a mask describing which processes are
faulty. We focus on regular model checking and show how it is possible
to compile the input for the model-checking problem to one that takes
the faults and their distribution into an account, and perform regular
model-checking on the compiled input. We demonstrate the effectiveness
of our framework and argue for its generality.