Please help transcribe this video using our simple transcription tool. You need to be logged in to do so.


Design and veri?cation of Self-Stabilizing (SS) network protocols are dif?cult tasks in part because of the requirement that a SS protocol must recover to a set of legitimate states from any state in its state space (when perturbed by transient faults). Moreover, distribution issues exacerbate the design complexity of SS protocols as processes should take local actions that result in global recovery/convergence of a network protocol. As such, most existing design techniques focus on protocols that are locally-correctable. To facilitate the design of ?nite-state SS protocols (that may not necessarily be locally-correctable), this paper presents a lightweight formal method supported by a software tool that automatically adds convergence to nonstabilizing protocols. We have used our method/tool to automatically generate several SS protocols with up to 40 processes (and 3 40 states) in a few minutes on a regular PC. Surprisingly, our tool has automatically synthesized both protocols that are the same as their manually-designed versions as well as new solutions for well-known problems in the literature (e.g., Dijkstra’s token ring [?]). Moreover, the proposed method has helped us reveal ?aws in a manually designed SS protocol.

Questions and Answers

You need to be logged in to be able to post here.