Invisible safety of distributed protocols

Abstract

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, at 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. 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. © Springer-Verlag Berlin Heidelberg 2006.