Automated analysis of fault-tolerance in distributed systems

A method for automated analysis of fault-tolerance of distributed systems is presented. It is based on a stream (or data-flow) model of distributed computation. Temporal (ordering) relationships between messages received by a component on different channels are not captured by this model. This makes the analysis more efficient and forces the use of conservative approximations in analysis of systems whose behavior depends on such inter-channel orderings. To further support efficient analysis, our framework includes abstractions for the contents, number, and ordering of messages sent on each channel. Analysis of a reliable broadcast protocol illustrates the method.