SASA: A SimulAtor of Self-stabilizing Algorithms

In this paper, we present SASA, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. SASA is implemented as a faithful representation of the atomic-state model. This model is the most commonly used in the self-stabilizing area to prove both the correct operation and complexity bounds of self-stabilizing algorithms. SASA encompasses all features necessary to debug, test, and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Algorithm's properties can be checked using formal test oracles. The design of SASA relies as much as possible on existing tools: OCAML, DOT, and tools developed in the Synchrone Group of the VERIMAG laboratory.