July 16, 2pm
Title: Automated Design of Self-Stabilization
Abstract
Nowadays, we witness an increasing impact of software system failures due to the
growing abundance and steady proliferation of software into our daily activities.
Self-stabilization is a property of a distributed system such that, regardless of the
legitimacy of its current behavior, the system behavior shall eventually become legitimate and shall remain so thereafter. Despite its elegance, self-stabilization is very difficult to
design and verify manually. We pursue two approaches towards the automated design of
self-stabilization. The first approach explores the global state space of distributed
protocols, through a set of heuristics, to automatically add self-stabilization to these
protocols. Towards this end, we develop software tools that implement our heuristics and
obtain existing and new self-stabilizing protocols on various network topologies. The
second approach investigates the global behavior of a distributed protocol by reasoning
about the local state space of just one of its components/processes. In particular, we
provide necessary and sufficient conditions — verifiable in the local state space of every
process — for global deadlock and livelock-freedom of protocols on ring topologies. Local
reasoning potentially circumvents state explosion and partial information in distributed
systems, thereby enabling our assertions about global deadlocks and livelocks to hold for
rings of arbitrary size.
Watch the defense: