Self-stabilizing Java: Tool Support for Building Robust Software

Name: Yong hun EomDate: April 15, 2015
Time: 10:00am
Location: EH 2430
Committee Chair: Professor Demsky
Committee members: Prof. Pai Chou and Prof. Rainer Doemer

Title: Self-stabilizing Java: Tool Support for Building Robust Software

Abstract:
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.