UC Irvine

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.