Softwar Design Laboratory at  MichiganTech

A Framework for Automated Design of Self-Stabilizing Network Protocols

Objectives

The research objective of this project is to exploit verification, synthesis, and fault tolerance techniques to achieve algorithmic addition of convergence to non-stabilizing protocols. Specifically, Instead of designing and verifying problem-specific self-stabilizing protocols, the proposed work will provide a reusable repository of synthesis methods for the addition of convergence to non-stabilizing protocols. Such a repository of synthesis techniques will enable a lightweight formal method where we will synthesize convergence functionalities for small instances of protocols to facilitate the design of larger instances. The synthesized SS protocols will be correct by construction, thereby potentially decreasing development costs. Furthermore, this project will provide three techniques that will enable designers to generalize small instances of the synthesized SS protocols, namely synthesized convergence stairs, cutoff theorems and structural induction. To evaluate the proposed research, we will investigate the automated design of convergence for real-world protocols and classic distributed computing problems (e.g., mutual exclusion and leader election) under different topologies and distinct fairness assumptions. As we devise new synthesis methods, we will implement them in an extensible software framework that we will publicize for the entire research community for evaluation. To measure the effectiveness of synthesis methods, we will identify complexity criteria and will compile them in a public benchmark.