Title: Invisible Safety of Distributed Protocols


Authors: Ittai Balaban, Amir Pnueli, and Lenore Zuck

The method of ``Invisible Invariants'' has been applied successfully
to protocols that assume a ``symmetric'' underlying topology, be it
cliques, stars, or rings.  In this paper we show how the method can
be applied to proving safety properties of distributed protocols
running under arbitrary topologies.  Many safety properties of such
protocols have reachability predicates, which, on first glance, are
beyond the scope of the Invisible Invariants method.  To overcome
this difficulty, we present a technique, called ``coloring,'' that
allows, in many instances, to replace the second order reachability
predicates by first order predicates, resulting in properties that
are amenable to Invisible Invariants, where ``reachable'' is
replaced by ``colored.''  We demonstrate our techniques on several
distributed protocols, including a variant on Luby's Maximal
Independent Set protocol, the Leader Election protocol used in the
IEEE 1394 (Firewire) distributed bus protocol, and various distributed
spanning tree algorithms. All examples have been tested using the
symbolic model checker TLV.