Self-stabilizing Java: Tool Support for Building Robust Software
Developing robust software systems remains an open research
problem. The current approaches for improving software reliability
mainly focus on minimizing the number of software bugs through
formal verification or extensive testing. Despite such efforts, it is
common that unexpected software bugs corrupt a program's state and
cause systems to fail.
The motivation for this research is to embrace the fact that it is
difficult to guarantee that software is error-free. We present
Self-stabilizing Java (SJava) that instead checks that a program
self-stabilizes. Self-stabilizing programs automatically recover to
the correct state from the corrupted state caused by software bugs and
other sources. A number of applications are inherently
self-stabilizing---such programs typically overwrite all non-constant
data with new input data.
We have developed a type system and static analyses that together
check whether program executions eventually transition from incorrect
states to the correct state. We combine this with a code-generation
strategy that ensures that a program continues executing long enough
to self-stabilize. Furthermore, in order to lower the burden of type
annotations, we present an annotation inference algorithm that
automatically derives an initial set of annotations.
Our experience using SJava indicates that our system successfully
checked that several benchmarks were self-stabilizing and effectively
inferred annotations for our benchmarks.