Technical Reports


A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols

Ali Ebnenasir CS-TR-14-02

This paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. The core idea behind the proposed method includes the automated synthesis of self-stabilizing protocols in a limited scope (i.e., fixed number of processes) and the use of theorem proving methods for the generalization of the solutions produced by the synthesizer. Specifically, we use the Prototype Verification System (PVS) to mechanically verify an algorithm for the synthesis of weakly self-stabilizing protocols. Then, we reuse the proof of correctness of the synthesis algorithm to establish the correctness of the generalized versions of synthesized protocols for an arbitrary number of processes. We demonstrate the proposed approach in the context of an agreement and a coloring protocol of the ring topology.

Synthesizing Self-Stabilization Through Superposition and Backtracking

Alex P. Klinkhamer and Ali Ebnenasir CS-TR-14-01

This paper presents a sound and complete method for algorithmic design of self-stabilizing network protocols. While the design of self-stabilization is known to be a hard problem, several sound (but incomplete) heuristics exists for algorithmic design of self-stabilization. The essence of the proposed approach is based on variable superposition and backtracking search. We have validated the proposed method by creating both a sequential and a parallel implementation in the context of a software tool, called Protocon. Moreover, we have used Protocon to automatically design self-stabilizing protocols for problems which all existing heuristics fail to solve.