Sponsored by:

National Science Foundation

(Contract  #CCF-1116546)

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the PI and his colleagues and do not necessarily reflect the views of the National Science Foundation.

Project Goal

The goal of this project is to advance our understanding of the challenges of designing self-stabilizing network protocols. Self-Stabilizing (SS) network protocols have increasingly become important as today's complex systems are subject to different kinds of transient faults (e.g., soft errors, bad initialization). A SS protocol converges (i.e., recovers) from any network configuration to a set of legitimate configurations when transient faults occur. For example, maintaining a spanning tree of the network nodes is central to many applications (e.g., broadcast, network reset). Temporary node/link failures may result in an illegitimate configuration (e.g., partitioned network) that may include non-tree components (e.g., rings). A SS protocol ensures convergence to a spanning tree from any illegitimate configuration. However, the design and verification of SS protocols are difficult tasks for several reasons. First, a SS protocol must converge to a set of legitimate configurations from any configuration. Second, the global convergence often should be achieved by the coordination of multiple processes while each process is aware of only its locality -- where locality of a process P includes a set of processes whose state is readable by P. Third, any functionality designed for convergence should not interfere with normal functionalities in the absence of transient faults (and vice versa). Most existing methods for the design of SS protocols are manual and require an extensive effort for proving the correctness of manual designs. Moreover, they mainly focus on protocols whose global configuration can be corrected if the local configurations of all processes are corrected, called the locally-correctable protocols.

Softwar Design Laboratory at MichiganTech

A Framework for Automated Design of Self-Stabilizing Network Protocols